README.md
1<!--
2 Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4 SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7This example target can be used to run the seL4 binary verification. It
8assumes that the graph-refine repository has been placed along side the
9l4v and HOL4 repositories, as will be the case if checked out as part of
10the [NICTA verification manifest](https://github.com/seL4/verification-manifest).
11
12The Makefile will invoke all the necessary steps, however, not all the tools
13needed are provided, and some require additional configuration.
14
15In particular:
16 - Python is required. Any python2 installation should be compatible.
17 - A cross compiler targeting 32-bit ARM is required.
18 + e.g. to use `arm-linux-gnueabi-gcc`, set environment variable `TOOLPREFIX=arm-linux-gnueabi-`
19 + gcc-4 series compilers are recommended for use with seL4.
20 + non-gcc compilers may require `CONFIG_KERNEL_COMPILER=compiler-name`
21 - An instance of binutils' `objdump` for 32-bit ARM is required
22 + this tool should be named `"$TOOLPREFIX"-objdump`
23 - Isabelle is provided but must be configured, see its README
24 + the configuration requirements are the same as for the [L4.verified proofs](https://github.com/seL4/l4v)
25 + the seL4 C model is built, which usually requires Isabelle in 64-bit mode ( `ML_PLATFORM="$ISABELLE_PLATFORM64"` in Isabelle's etc/settings )
26 - HOL4 is provided but must be configured, see its README and INSTALL files.
27 + HOL4 will require an ML environment, typically polyML.
28 + the final `bin/build` step of installing HOL4 can be deferred (to save time) and will be run by the Makefile.
29 + transient faults have sometimes been observed running the HOL4
30decompiler. try rerunning the decompiler, or adjusting polyML version.
31 - The standalone variant of the NICTA C parser must build
32 + the parser is provided in the `l4v` directory
33 + building the parser may require MLton installed, see the [L4.verified README.md](https://github.com/seL4/l4v)
34 - Either one or two SMT solvers is required, and a .solverlist file must locate them.
35 + the solver self-test `python ../solver.py test` will document the
36.solverlist format, and check for solver compatibility if solvers are found.
37 + the tool uses an online solver and an offline solver, with different requirements.
38 + any SMTLIB2-compatible solver supporting the `QF_ABV` logic can be used,
39and we have had success with Z3, CVC4, MathSAT5 and SONOLAR.
40 + Using Z3 as the offline solver is not recommended, because of the way it
41generates underspecified models for some array problems.
42 + SONOLAR cannot be used as the online solver.
43 - The proof process takes a long time, and some goals may time out.
44 + the process typically takes around 10 hours, but this varies extensively
45with SMT solver version and compiler version.
46 + SONOLAR is the only solver known to solve all the problems created here
47without timeouts, using other solvers will probably result in numerous timeouts.
48 + timeouts are not fatal, they will be handled and summarised in the final report.
49
50
51