Verification

Note

This document regards an older version of Islet (tag v1.0-seur).

We formally verify Islet using Kani’s model checking. Our verification harnesses adopt the same input and output conditions as well as similar structures used in TF-RMM’s harnesses which are extracted from Machine Readable Specification. It would help to check the conformance of the two systems written in different languages.

Verification dependency

• patched Kani

Available RMI targets

rmi_features
rmi_granule_delegate
rmi_granule_undelegate
rmi_realm_activate
rmi_realm_destroy
rmi_rec_aux_count
rmi_rec_destroy
rmi_version

Verifying Islet

(in islet/model-checking)

# Choose one among the list in `Available RMI targets` for the value of `RMI_TARGET`
$ RMI_TARGET=rmi_granule_undelegate make verify

For more about Islet’s model-checking, please refer to here.