Add harnesses for verifying rmi granule delegate and undelegate

zpzigi754 commented 4 months ago

This PR adds two verification harnesses for model checking: RMI_GRANULE_DELEGATE and RMI_GRANULE_UNDELEGATE.

It found one correctness bug (https://github.com/islet-project/islet/pull/307).

How to use?

(in islet/model-checking)

$ RMI_TARGET=rmi_granule_(un)delegate make verify 

...
SUMMARY:
 ** 0 of 3055 failed (81 unreachable)

 ** 14 of 14 cover properties satisfied

Summary of changes

Add a ghost gpt field in granule entry for tracking Granule Protection Table (GPT)'s change
Add is_valid predicate for ensuring Granule Status Table (GST)'s valid status
Put common helper functions in common module (pre_/post_granule_state(), pre_/post_granule_gpt(), etc)
Add host memory and EL3 gpt change modeling code to help harnesses interact with their environment

About host memory modeling

This models the Host memory as a pre-allocated memory region which can avoid a false positive related to invalid memory accesses in model checking. Also, instead of using the same starting address (e.g., 0x8000_0000), it uses a mock region filled with non-deterministic contents. This approach helps to address an issue related to the backend CBMC's pointer encoding, as 0x8000_0000 cannot be distinguished from null pointer in CBMC.

Invariants with `is_valid()` predicate

The added is_valid() predicate can be used to ensure that all granule entries in GST are in valid status conforminig to the spec A2.2.1.

A2.2.1 Granule attributes in beta0-eac4

If the state of a Granule is not UNDELEGATED then the PAS of the Granule is REALM.
If the state of a Granule is UNDELEGATED then the PAS of the Granule is not REALM.

jinbpark commented 4 months ago

How about putting $ RMI_TARGET=rmi_granule_(un)delegate make verify into README.md (in root dir). It would be nice to show people what we're doing for verification in the first place, especially given that only one month left to CC summit. (+ updating our github pages later?)

zpzigi754 commented 4 months ago

How about putting $ RMI_TARGET=rmi_granule_(un)delegate make verify into README.md (in root dir). It would be nice to show people what we're doing for verification in the first place, especially given that only one month left to CC summit. (+ updating our github pages later?)

Thank you for the suggestion! I've slightly updated README.md and added a page about verification.

islet-project / islet