tree: befd3ee0bf7386cd9656ecddd26af58aa9e1bb91 [path history] [tgz]
  2. run_tests

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.