1<!--
2 Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4 SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7[![DOI][0]](http://dx.doi.org/10.5281/zenodo.591732)
8
9 [0]: https://zenodo.org/badge/doi/10.5281/zenodo.591732.svg
10
11
12[The L4.verified Proofs][1]
13===========================
14
15This is the L4.verified git repository with formal specifications and
16proofs for the seL4 microkernel.
17
18Most proofs in this repository are conducted in the interactive proof
19assistant [Isabelle/HOL][2]. For an introduction to Isabelle, see its
20[official website][2] and [documentation][3].
21
22 [1]: https://github.com/seL4/l4v "L4.verified Repository"
23 [2]: http://isabelle.in.tum.de "Isabelle Website"
24 [3]: http://isabelle.in.tum.de/documentation.html "Isabelle Documentation"
25
26<a name="setup"></a>
27Setup
28-----
29
30This repository is meant to be used as part of a Google [repo][5] setup.
31Instead of cloning it directly, follow the instructions at the [manifest git
32repo](https://github.com/seL4/verification-manifest).
33
34 [5]: http://source.android.com/source/downloading.html#installing-repo "google repo installation"
35
36
37Dependencies
38------------
39
40For software dependencies and Isabelle setup, see the
41[setup.md](docs/setup.md) file in the `docs` directory.
42
43
44Contributing
45------------
46
47Contributions to this repository are welcome.
48Please read [`CONTRIBUTING.md`](CONTRIBUTING.md) for details.
49
50Overview
51--------
52
53The repository is organised as follows.
54
55 * [`docs`](docs/): documentation on conventions, style, etc.
56
57 * [`spec`](spec/): a number of different formal specifications of seL4
58 * [`abstract`](spec/abstract/): the functional abstract specification of seL4
59 * [`sep-abstract`](spec/sep-abstract/): an abstract specification for a reduced
60 version of seL4 that is configured as a separation kernel
61 * [`haskell`](spec/haskell/): Haskell model of the seL4 kernel, kept in sync
62 with the C code
63 * [`machine`](spec/machine/): the machine interface of these two specifications
64 * [`cspec`](spec/cspec/): the entry point for automatically translating the seL4 C code
65 into Isabelle
66 * [`capDL`](spec/capDL/): a specification of seL4 that abstracts from memory content and
67 concrete execution behaviour, modelling the protection state of the
68 system in terms of capabilities. This specification corresponds to the
69 capability distribution language *capDL* that can be used to initialise
70 user-level systems on top of seL4.
71 * [`take-grant`](spec/take-grant/): a formalisation of the classical take-grant security
72 model, applied to seL4, but not connected to the code of seL4.
73
74 * There are additional specifications that are not tracked in this repository,
75 but are generated from other files:
76 * [`design`](spec/design/): the design-level specification of seL4,
77 generated from the Haskell model.
78 * [`c`](spec/cspec/c/): the C code of the seL4 kernel, preprocessed into a form that
79 can be read into Isabelle. This is generated from the [seL4 repository](https://github.com/seL4/seL4).
80
81 * [`proof`](proof/): the seL4 proofs
82 * [`invariant-abstract`](proof/invariant-abstract/): invariants of the seL4 abstract specification
83 * [`refine`](proof/refine/): refinement between abstract and design specifications
84 * [`crefine`](proof/crefine/): refinement between design specification and C semantics
85 * [`access-control`](proof/access-control/): integrity and authority confinement proofs
86 * [`infoflow`](proof/infoflow/): confidentiality and intransitive non-interference proofs
87 * [`asmrefine`](proof/asmrefine/): Isabelle/HOL part of the seL4 binary verification
88 * [`drefine`](proof/drefine/): refinement between capDL and abstract specification
89 * [`sep-capDL`](proof/sep-capDL/): a separation logic instance on capDL
90 * [`capDL-api`](proof/capDL-api/): separation logic specifications of selected seL4 APIs
91
92 * [`lib`](lib/): generic proof libraries, proof methods and tools. Among these,
93 further libraries for fixed-size machine words, a formalisation of state
94 monads with nondeterminism and exceptions, a generic verification condition
95 generator for monads, a recursive invariant prover for these (`crunch`), an
96 abstract separation logic formalisation, a prototype of the [Eisbach][6] proof
97 method language, a prototype `levity` refactoring tool, and others.
98
99 * [`tools`](tools/): larger, self-contained proof tools
100 * [`asmrefine`](tools/asmrefine/): the generic Isabelle/HOL part of the binary
101 verification tool
102 * [`c-parser`](tools/c-parser/): a parser from C into the Simpl language in Isabelle/HOL.
103 Includes a C memory model.
104 * [`autocorres`](tools/autocorres/): an automated, proof-producing abstraction tool from
105 C into higher-level Isabelle/HOL functions, based on the C parser above
106 * [`haskell-translator`](tools/haskell-translator/): a basic python script for converting the Haskell
107 prototype of seL4 into the executable design specification in
108 Isabelle/HOL.
109
110 * [`misc`](misc/): miscellaneous scripts and build tools
111
112 * [`camkes`](camkes/): an initial formalisation of the CAmkES component platform
113 on seL4. Work in progress.
114
115 * [`sys-init`](sys-init/): specification of a capDL-based, user-level system initialiser
116 for seL4, with proof that the specification leads to correctly initialised
117 systems.
118
119
120 [6]: https://ts.data61.csiro.au/publications/nictaabstracts/Matichuk_WM_14.abstract.pml "An Isabelle Proof Method Language"
121
122
123Hardware requirements
124---------------------
125
126Almost all proofs in this repository should work within 4GB of RAM. Proofs
127involving the C refinement, will usually need the 64bit mode of polyml and
128about 16GB of RAM.
129
130The proofs distribute reasonably well over multiple cores, up to about 8
131cores are useful.
132
133
134jEdit
135-----
136
137We provide a jEdit macro that is very useful when working with large theory
138files, **goto-error**, which moves the cursor to the first error in the file.
139
140To install the macro, run the following commands in the directory
141`verification/l4v/`:
142```bash
143mkdir -p ~/.isabelle/jedit/macros
144cp misc/jedit/macros/goto-error.bsh ~/.isabelle/jedit/macros/.
145```
146
147You can add keybindings for this macro in the usual way, by going to
148`Utilities -> Global Options -> jEdit -> Shortcuts`.
149
150Additionally, our fork of Isabelle/jEdit has an updated indenter which is more
151proof-context aware than the 'original' indenter. Pressing `ctrl+i` while some
152`apply`-script text is selected should auto-indent the script while respecting
153subgoal depth and maintaining the relative indentation of multi-line `apply`
154statements.
155
156Running the Proofs
157------------------
158
159If Isabelle is set up correctly, a full test for the proofs in this repository
160can be run with the command
161
162 ./run_tests
163
164from the directory `l4v/`.
165
166Not all of the proof sessions can be built directly with the `isabelle build` command.
167The seL4 verification proofs depend on Isabelle specifications that are
168generated from the C source code and Haskell model.
169Therefore, it's recommended to always build using the supplied makefiles,
170which will ensure that these generated specs are up to date.
171
172To do this, enter one level under the `l4v/` directory and run `make <session-name>`.
173For example, to build the C refinement proof session, do
174
175 cd l4v/proof
176 make CRefine
177
178As another example, to build the session for the Haskell model, do
179
180 cd l4v/spec
181 make ExecSpec
182
183See the `HEAPS` variable in the corresponding `Makefile` for available targets.
184
185Proof sessions that do not depend on generated inputs can be built directly with
186
187 ./isabelle/bin/isabelle build -d . -v -b <session name>
188
189from the directory `l4v/`. For available sessions, see the corresponding
190`ROOT` files in this repository. There is roughly one session corresponding to
191each major directory in the repository.
192
193For interactively exploring, say the invariant proof of the abstract
194specification with a pre-built logic image for the abstract specification,
195run
196
197 ./isabelle/bin/isabelle jedit -d . -l ASpec
198
199in `l4v/` and open one of the files in `proof/invariant-abstract`.
200
201
