This is a test suite for running the generated capDL refinement proofs. These are Isabelle proof scripts, to prove that the generated capDL respects the isolation properties expected from its CAmkES system specification.
Currently, the verification only supports apps that use the basic CAmkES features and connectors. We plan to extend verification support to more complex CAmkES assemblies in the future (eventually including a CAmkES VMM). Also note that only the AARCH32 platform is supported.
When building a CAmkES app, enable proof generation with the CAmkESCapDLVerification
option. The proof scripts will be generated in projects/camkes
in your build directory. This also requires CAmkESCapDLStaticAlloc
to be enabled.
The top-level test script is ./run_tests
.
The tests expect to run as part of a camkes-manifest checkout. In the camkes-manifest repo, do
repo sync -m l4v-master.xml
This will clone the Isabelle theorem prover and the L4.verified infrastructure into projects/l4v
.
Then run the run_tests
script that is in this directory.