Add model checking harnesses for rec_aux_count and rec_destroy #374
Conversation
This removes null state which does not exist in the spec. ``` C1.23 RmmRecState type Name Description REC_READY REC is not currently running. REC_RUNNING REC is currently running. ``` Signed-off-by: Changho Choi <[email protected]>
| for i in 0..rmi::MAX_REC_AUX_GRANULES { | ||
| let rec_aux = rec.aux(i) as usize; | ||
| let mut rec_aux_granule = get_granule_if!(rec_aux, GranuleState::Delegated)?; | ||
| set_granule(&mut rec_aux_granule, GranuleState::RecAux)?; |
There was a problem hiding this comment.
Does Islet actually use Auxiliary Granules? During the setup of a Realm, KVM asks RMM about the number of auxilary granules (rmi::REC_AUX_COUNT) that RMM needs for some data storage. RMM returns MAX_REC_AUX_GRANULES. Basing on that information KVM allocates and passes them while calling REC_CREATE. But they seem not to be used at all in Islet RMM. Why not just to return 0 while calling rmi::REC_AUX_COUNT?
There was a problem hiding this comment.
That's a really good question. I think that returning 0 in rmi::REC_AUX_COUNT would be also a reasonable alternative as a shortcut. I am actually not sure how auxiliary granules would be used eventually with a real world realm image: this is actually in one of my query lists to Arm. However, as long as RecAux Granule is not deprecated in the official arm cca's spec, I think that supporting this functionality would be better than not supporting it. Also, note that RecAux have existed since the earliest beta0 version to the latest alpha8 version in the spec. Thus, I expect that it is less likely to be deprecated in the future as well.
There was a problem hiding this comment.
In TF-RMM they use these auxiliary granules as a heap for cryptographic operations during the attestation process. I don't mean to remove or change the RMI API. TF-RMM uses these extra granules as a storage (heap), where Islet RMM don't use them at all. So returning 0 in REC_AUC_COUNT handler will be still aligned with the RMM specification. rmi::REC_AUX_COUNT is a way for telling KVM how many extra granules we need per a REC. In other words, the RMM, not KVM, decides how many auxiliary granules the REC needs.
There was a problem hiding this comment.
Oh, thank you for the information!
This fixes rec_aux in B4.3.12.3, found by the process of
verification. Rec's aux should be set as the one passed
by the parameters.
```
B4.3.12.3 Success conditions
ID Condition
rec_aux AuxEqual(
Rec(rec).aux, params.aux,
RecAuxCount(rd))
```
Signed-off-by: Changho Choi <[email protected]>
This fixes num_aux in B4.3.12.2, found by the process of
verification. Inequality operator should be used instead
of the previous comparison operator. Note that a smaller
value should not be used for the correct setting.
```
B4.3.12.2 Failure conditions
ID Condition
num_aux pre: params.num_aux != RecAuxCount(rd)
post: ResultEqual(result, RMI_ERROR_INPUT)
```
Signed-off-by: Changho Choi <[email protected]>
This fixes rec_aux_state in B4.3.12.3, found by the process of
verification. All the pointers inside Rec's aux should be set
as REC_AUX granule.
```
B4.3.12.3 Success conditions
ID Condition
rec_aux_state AuxStateEqual(
Rec(rec).aux, RecAuxCount(rd), REC_AUX)
```
Signed-off-by: Changho Choi <[email protected]>
This is done to reduce the overall state size as well as verification time. Signed-off-by: Changho Choi <[email protected]>
This harness verifies RMI_REC_AUX_COUNT's behaviors using model checking. Usage) (in islet/model-checking) $ RMI_TARGET=rmi_rec_aux_count make verify Signed-off-by: Changho Choi <[email protected]>
This harness verifies RMI_REC_DESTROY's behaviors using model checking. Usage) (in islet/model-checking) $ RMI_TARGET=rmi_rec_destroy make verify Signed-off-by: Changho Choi <[email protected]>
This fixes rec_state in B4.3.13.2, detected by model checking.
Rec's state should not be running in order to be destroyed.
```
B4.3.13.2 Failure conditions
ID Condition
rec_state pre: Rec(rec).state == REC_RUNNING
post: ResultEqual(result, RMI_ERROR_REC)
```
Signed-off-by: Changho Choi <[email protected]>
This fixes rec_aux_state in B4.3.13.3, detected by model checking.
All the pointers inside Rec's aux should be set as Delegated.
```
B4.3.13.3 Success conditions
ID Condition
rec_aux_state AuxStateEqual(
Rec(rec).aux, RecAuxCount(rd), DELEGATED)
```
Signed-off-by: Changho Choi <[email protected]>
| @@ -94,15 +95,29 @@ pub fn set_event_handler(mainloop: &mut Mainloop) { | |||
| // `rsi` is currently not reachable in model checking harnesses | |||
| HashContext::new(&mut rd)?.measure_rec_params(¶ms)?; | |||
|
|
|||
| for i in 0..rmi::MAX_REC_AUX_GRANULES { | |||
There was a problem hiding this comment.
Not directly related to this PR,
it seems that rd.inc_rec_index(); at line-93 in this function should be placed at the end of this function (after all operations are done correctly, as set_granule is).
If something goes wrong in this rec_aux loop, it would return without decrementing rec_index by one, leaving rec_index incorrect.
There was a problem hiding this comment.
Good finding! I totally agree with you. Similarly, I think that most of the setting in rec.init() above also might need to be done at the end of the function, because they should be only set in the success condition. One issue is that setting the successful conditions also may involve an error handling which is a bit of mess.
There was a problem hiding this comment.
It's not just rec.init() but there might be similar issues in other functions as well. (e.g., rmm page table mapping. we should unmap things from the rmm page table if something goes wrong in the middle)
We'd better come up with a kind of design pattern to gracefully deal with such issues.
I think it's ok to put this off until we settle up that pattern, and we can apply that pattern to all relevant codes at once. (this PR might be not that small in size?)
EDIT: #375 --> I created an issue for this
There was a problem hiding this comment.
Thank you for opening the issue there!
zpzigi754
force-pushed
the
verify-rec-aux-count-destroy
branch
from
dc041c1 to
f8d384c
Compare
zpzigi754
requested review from
lkh8291,
bitboom,
bokdeuk-jeong,
jinbpark,
hihi-wang and
nook1208
This PR adds model checking harnesses for rec_aux_count and rec_destroy: they verify RMI_REC_AUX_COUNT and RMI_REC_DESTROY's behaviors respectively. It also fixes several spec violations two of which were detected by the included harness while others were found by the process of verification.