History

Kent McLeod 3a160d043e Remove references to kzm platform This platform has been removed from seL4 due to ending support. The sabre platform should be substitutable for camkes examples. Signed-off-by: Kent McLeod <kent@kry10.com>		2021-09-30 18:43:23 +10:00
..
README.md	convert to SDPX license tags	2021-02-12 17:24:15 +11:00
run_tests	Remove references to kzm platform	2021-09-30 18:43:23 +10:00

README.md

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.

Tests

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.