README.md
1<!--
2 Copyright 2018, Data61
3 Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 ABN 41 687 119 230.
5
6 This software may be distributed and modified according to the terms of
7 the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 See "LICENSE_BSD2.txt" for details.
9
10 @TAG(DATA61_BSD)
11-->
12
13This is a test suite for running the generated capDL refinement proofs.
14These are Isabelle proof scripts, to prove that the generated capDL
15respects the isolation properties expected from its CAmkES system
16specification.
17
18Currently, the verification only supports apps that use the basic
19CAmkES features and connectors.
20We plan to extend verification support to more complex CAmkES
21assemblies in the future (eventually including a CAmkES VMM).
22Also note that only the AARCH32 platform is supported.
23
24When building a CAmkES app, enable proof generation with the
25`CAmkESCapDLVerification` option. The proof scripts will be
26generated in `projects/camkes` in your build directory. This also
27requires `CAmkESCapDLStaticAlloc` to be enabled.
28
29# Tests
30The top-level test script is `./run_tests`.
31
32The tests expect to run as part of a
33[camkes-manifest](https://github.com/seL4/camkes-manifest) checkout.
34In the camkes-manifest repo, do
35
36```
37repo sync -m l4v-master.xml
38```
39
40This will clone the Isabelle theorem prover and the L4.verified
41infrastructure into `projects/l4v`.
42
43Then run the `run_tests` script that is in this directory.
44