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