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