1[![DOI][0]](http://dx.doi.org/10.5281/zenodo.591732)
2
3 [0]: https://zenodo.org/badge/doi/10.5281/zenodo.591732.svg
4
5
6[The L4.verified Proofs][1]
7===========================
8
9This is the L4.verified git repository with formal specifications and
10proofs for the seL4 microkernel.
11
12Most proofs in this repository are conducted in the interactive proof
13assistant [Isabelle/HOL][2]. For an introduction to Isabelle, see its
14[official website][2] and [documentation][3].
15
16 [1]: https://github.com/seL4/l4v "L4.verified Repository"
17 [2]: http://isabelle.in.tum.de "Isabelle Website"
18 [3]: http://isabelle.in.tum.de/documentation.html "Isabelle Documentation"
19
20Repository Setup
21----------------
22
23This repository is meant to be used as part of a Google [repo][5] setup.
24Instead of cloning it directly, please go to the following repository
25and follow the instructions there:
26
27 https://github.com/seL4/verification-manifest
28
29For setting up the theorem prover and other dependencies, please see the
30section [Dependencies](#dependencies) below.
31
32 [5]: http://source.android.com/source/downloading.html#installing-repo "google repo installation"
33
34Contributing
35------------
36
37Contributions to this repository are welcome.
38Please read [`CONTRIBUTING.md`](CONTRIBUTING.md) for details.
39
40Overview
41--------
42
43The repository is organised as follows.
44
45 * [`spec`](spec/): a number of different formal specifications of seL4
46 * [`abstract`](spec/abstract/): the functional abstract specification of seL4
47 * [`sep-abstract`](spec/sep-abstract/): an abstract specification for a reduced
48 version of seL4 that is configured as a separation kernel
49 * [`haskell`](spec/haskell/): Haskell model of the seL4 kernel, kept in sync
50 with the C code
51 * [`machine`](spec/machine/): the machine interface of these two specifications
52 * [`cspec`](spec/cspec/): the entry point for automatically translating the seL4 C code
53 into Isabelle
54 * [`capDL`](spec/capDL/): a specification of seL4 that abstracts from memory content and
55 concrete execution behaviour, modelling the protection state of the
56 system in terms of capabilities. This specification corresponds to the
57 capability distribution language *capDL* that can be used to initialise
58 user-level systems on top of seL4.
59 * [`take-grant`](spec/take-grant/): a formalisation of the classical take-grant security
60 model, applied to seL4, but not connected to the code of seL4.
61
62 * There are additional specifications that are not tracked in this repository,
63 but are generated from other files:
64 * [`design`](spec/design/): the design-level specification of seL4,
65 generated from the Haskell model.
66 * [`c`](spec/cspec/c/): the C code of the seL4 kernel, preprocessed into a form that
67 can be read into Isabelle. This is generated from the [seL4 repository](../seL4).
68
69 * [`proof`](proof/): the seL4 proofs
70 * [`invariant-abstract`](proof/invariant-abstract/): invariants of the seL4 abstract specification
71 * [`refine`](proof/refine/): refinement between abstract and design specifications
72 * [`crefine`](proof/crefine/): refinement between design specification and C semantics
73 * [`access-control`](proof/access-control/): integrity and authority confinement proofs
74 * [`infoflow`](proof/infoflow/): confidentiality and intransitive non-interference proofs
75 * [`asmrefine`](proof/asmrefine/): Isabelle/HOL part of the seL4 binary verification
76 * [`drefine`](proof/drefine/): refinement between capDL and abstract specification
77 * [`sep-capDL`](proof/sep-capDL/): a separation logic instance on capDL
78 * [`capDL-api`](proof/capDL-api/): separation logic specifications of selected seL4 APIs
79
80 * [`lib`](lib/): generic proof libraries, proof methods and tools. Among these,
81 further libraries for fixed-size machine words, a formalisation of state
82 monads with nondeterminism and exceptions, a generic verification condition
83 generator for monads, a recursive invariant prover for these (`crunch`), an
84 abstract separation logic formalisation, a prototype of the [Eisbach][6] proof
85 method language, a prototype `levity` refactoring tool, and others.
86
87 * [`tools`](tools/): larger, self-contained proof tools
88 * [`asmrefine`](tools/asmrefine/): the generic Isabelle/HOL part of the binary
89 verification tool
90 * [`c-parser`](tools/c-parser/): a parser from C into the Simpl language in Isabelle/HOL.
91 Includes a C memory model.
92 * [`autocorres`](tools/autocorres/): an automated, proof-producing abstraction tool from
93 C into higher-level Isabelle/HOL functions, based on the C parser above
94 * [`haskell-translator`](tools/haskell-translator/): a basic python script for converting the Haskell
95 prototype of seL4 into the executable design specification in
96 Isabelle/HOL.
97
98 * [`misc`](misc/): miscellaneous scripts and build tools
99
100 * [`camkes`](camkes/): an initial formalisation of the CAmkES component platform
101 on seL4. Work in progress.
102
103 * [`sys-init`](sys-init/): specification of a capDL-based, user-level system initialiser
104 for seL4, with proof that the specification leads to correctly initialised
105 systems.
106
107
108 [6]: http://www.nicta.com.au/pub?id=7847 "An Isabelle Proof Method Language"
109
110
111Dependencies
112------------
113
114### Hardware
115
116Almost all proofs in this repository should work within 4GB of RAM. Proofs
117involving the C refinement, will usually need the 64bit mode of polyml and
118about 16GB of RAM.
119
120The proofs distribute reasonably well over multiple cores, up to about 8
121cores are useful.
122
123### Software
124
125The proofs in this repository use `Isabelle2018`. A copy of Isabelle
126is included in the repository setup.
127
128The dependencies for installing Isabelle in this repository are
129
130 * Perl 5.x with `libwww-perl`
131 * Python 2.x
132 * LaTeX, for instance on Ubuntu 14.04
133 `sudo apt-get install texlive-fonts-recommended texlive-latex-extra texlive-metapost texlive-bibtex-extra`
134 * 32-bit C/C++ standard libraries on 64-bit platforms (optional)
135
136For running the standalone version of the C Parser you will additionally need
137
138 * [MLton][7] ML compiler (package `mlton-compiler` on Ubuntu)
139
140For building the Haskell kernel model, the Haskell build tool [stack][] is
141required. The Haskell kernel `Makefile` will use `stack` to obtain appropriate
142versions of `ghc` and `cabal-install`. Note that this repository does not
143contain the QEmu interface for actually running the model.
144
145For running the C proofs, you need a working C preprocessor setup for the seL4
146repository.
147
148*On Linux*: the best way to make sure you have everything is to install the
149full build environment for seL4:
150
151 * seL4 [development tool chain][8] on Debian and Ubuntu
152 * `make` version 3.81 or higher
153
154You can get away with avoiding a full cross compiler setup form the above,
155but you will need at least these:
156
157 sudo apt-get install python-pip python-dev libxml2-utils
158 sudo pip install sel4-deps
159
160*On MacOS*: here it is harder to get a full cross-compiler setup going. For
161normal proof development, a full setup is not necessary, though. You mostly
162need a gcc-compatible C pre-processor and python. Try the following steps:
163
164 * install `XCode` from the AppStore and its command line tools. If you are
165 running MacPorts, you have these already. Otherwise, after you have
166 XCode installed, run `gcc --version` in a terminal window. If it reports a
167 version, you're set. Otherwise it should pop up a window and prompt for
168 installation of the command line tools.
169 * install the seL4 Python dependencies, for instance using
170 `sudo easy_install sel4-deps`.
171 `easy_install` is part of Python's [`setuptools`][9].
172 * install the [`misc/scripts/cpp`](misc/scripts/cpp) wrapper for clang,
173 by putting it in `~/bin`, or somewhere else in your `PATH`.
174
175
176[7]: http://mlton.org "MLton ML compiler"
177[8]: http://sel4.systems/Info/GettingStarted/DebianToolChain.pml "seL4 tool chain setup"
178[9]: https://pypi.python.org/pypi/setuptools "python package installer"
179[stack]: https://haskellstack.org/
180
181
182Isabelle Setup
183--------------
184
185After the repository is set up in Google repo, you should have following
186directory structure, where `l4v` is the repository you are currently looking
187at:
188
189 verification/
190 isabelle/
191 l4v/
192 seL4/
193
194To set up Isabelle for use in `l4v/`, assuming you have no previous
195installation of Isabelle, run the following commands in the directory
196`verification/l4v/`:
197
198 mkdir -p ~/.isabelle/etc
199 cp -i misc/etc/settings ~/.isabelle/etc/settings
200 ./isabelle/bin/isabelle components -a
201 ./isabelle/bin/isabelle jedit -bf
202 ./isabelle/bin/isabelle build -bv HOL-Word
203
204These commands perform the following steps:
205
206 * create an Isabelle user settings directory.
207 * install L4.verified Isabelle settings.
208 These settings initialise the Isabelle installation to use the standard
209 Isabelle `contrib` tools from the Munich Isabelle repository and set up
210 paths such that multiple Isabelle repository installations can be used
211 side by side without interfering with each other.
212 * download `contrib` components from the Munich repository. This includes
213 Scala, a Java JDK, PolyML, and multiple external provers. You should
214 download these, even if you have these tools previously installed
215 elsewhere to make sure you have the right versions. Depending on your
216 internet connection, this may take some time.
217 * compile and build the Isabelle PIDE jEdit interface.
218 * build basic Isabelle images, including `HOL-Word` to ensure that
219 the installation works. This may take a few minutes.
220
221Alternatively, it is possible to use the official Isabelle2018 release
222bundle for your platform from the [Isabelle website][2]. In this case, the
223installation steps above can be skipped, and you would replace the directory
224`verification/isabelle/` with a symbolic link to the Isabelle home directory
225of the release version. Note that this is not recommended for development,
226since Google repo will overwrite this link when you synchronise repositories
227and Isabelle upgrades will have to be performed manually as development
228progresses.
229
230
231Running the Proofs
232------------------
233
234If Isabelle is set up correctly, a full test for the proofs in this repository
235can be run with the command
236
237 ./run_tests
238
239from the directory `l4v/`.
240
241Not all of the proof sessions can be built directly with the `isabelle build` command.
242The seL4 verification proofs depend on Isabelle specifications that are
243generated from the C source code and Haskell model.
244Therefore, it's recommended to always build using the supplied makefiles,
245which will ensure that these generated specs are up to date.
246
247To do this, enter one level under the `l4v/` directory and run `make <session-name>`.
248For example, to build the C refinement proof session, do
249
250 cd l4v/proof
251 make CRefine
252
253As another example, to build the session for the Haskell model, do
254
255 cd l4v/spec
256 make ExecSpec
257
258See the `HEAPS` variable in the corresponding `Makefile` for available targets.
259
260Proof sessions that do not depend on generated inputs can be built directly with
261
262 ./isabelle/bin/isabelle build -d . -v -b <session name>
263
264from the directory `l4v/`. For available sessions, see the corresponding
265`ROOT` files in this repository. There is roughly one session corresponding to
266each major directory in the repository.
267
268For interactively exploring, say the invariant proof of the abstract
269specification with a pre-built logic image for the abstract specification,
270run
271
272 ./isabelle/bin/isabelle jedit -d . -l ASpec
273
274in `l4v/` and open one of the files in `proof/invariant-abstract`.
275
276
277License
278-------
279
280The files in this repository are released under standard open source
281licenses. Please see the individual file headers and
282[`LICENSE_GPLv2.txt`](LICENSE_GPLv2.txt) and
283[`LICENSE_BSD2.txt`](LICENSE_BSD2.txt) files for details.
284
285
286
