2018-03-01 05:56:29 +00:00
|
|
|
[![DOI][0]](http://dx.doi.org/10.5281/zenodo.591732)
|
|
|
|
|
|
|
|
[0]: https://zenodo.org/badge/doi/10.5281/zenodo.591732.svg
|
|
|
|
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
[The L4.verified Proofs][1]
|
|
|
|
===========================
|
2014-07-14 19:32:44 +00:00
|
|
|
|
2014-07-22 22:35:05 +00:00
|
|
|
This is the L4.verified git repository with formal specifications and
|
|
|
|
proofs for the seL4 microkernel.
|
|
|
|
|
|
|
|
Most proofs in this repository are conducted in the interactive proof
|
|
|
|
assistant [Isabelle/HOL][2]. For an introduction to Isabelle, see its
|
|
|
|
[official website][2] and [documentation][3].
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
[1]: https://github.com/seL4/l4v "L4.verified Repository"
|
|
|
|
[2]: http://isabelle.in.tum.de "Isabelle Website"
|
|
|
|
[3]: http://isabelle.in.tum.de/documentation.html "Isabelle Documentation"
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2019-04-19 08:12:58 +00:00
|
|
|
<a name="setup"></a>
|
|
|
|
Setup
|
|
|
|
-----
|
2014-07-28 01:59:57 +00:00
|
|
|
|
2014-08-11 05:41:39 +00:00
|
|
|
This repository is meant to be used as part of a Google [repo][5] setup.
|
2019-04-19 08:12:58 +00:00
|
|
|
Instead of cloning it directly, follow the instructions at the [manifest git
|
|
|
|
repo](https://github.com/seL4/verification-manifest).
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2014-08-11 05:41:39 +00:00
|
|
|
[5]: http://source.android.com/source/downloading.html#installing-repo "google repo installation"
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2019-04-19 08:12:58 +00:00
|
|
|
### Software dependencies
|
|
|
|
|
|
|
|
On **Ubuntu 18.04**, to run all the tests against the **ARMv7-A** architecture
|
|
|
|
you will need to install the following packages:
|
|
|
|
```bash
|
|
|
|
sudo apt-get install \
|
|
|
|
haskell-stack python python-pip python-dev \
|
|
|
|
mlton-compiler gcc-arm-none-eabi \
|
|
|
|
build-essential libxml2-utils ccache ncurses-dev librsvg2-bin \
|
|
|
|
device-tree-compiler cmake ninja-build curl zlib1g-dev \
|
|
|
|
texlive-fonts-recommended texlive-latex-extra \
|
|
|
|
texlive-metapost texlive-bibtex-extra
|
|
|
|
```
|
|
|
|
```bash
|
|
|
|
sudo pip install --upgrade pip
|
|
|
|
sudo pip install sel4-deps
|
|
|
|
```
|
|
|
|
|
|
|
|
On **Debian Stretch**, install the above packages as well as:
|
|
|
|
```bash
|
|
|
|
sudo apt-get install \
|
|
|
|
rsync
|
|
|
|
```
|
|
|
|
|
|
|
|
### Haskell Stack
|
|
|
|
L4V requires [haskell-stack](https://docs.haskellstack.org/en/stable/README).
|
|
|
|
Make sure you've adjusted your `PATH` to include `$HOME/.local/bin`, and that
|
|
|
|
you're running an up-to-date version:
|
|
|
|
```bash
|
|
|
|
stack upgrade --binary-only
|
|
|
|
which stack # should be $HOME/.local/bin/stack
|
|
|
|
```
|
|
|
|
|
|
|
|
### MacOS
|
|
|
|
Other than the cross-compiler `gcc` toolchain, setup on MacOS should be similar
|
|
|
|
to that on Ubuntu. To set up a cross-compiler, try the following:
|
|
|
|
* Install `XCode` from the AppStore and its command line tools. If you are
|
|
|
|
running MacPorts, you have these already. Otherwise, after you have XCode
|
|
|
|
installed, run `gcc --version` in a terminal window. If it reports a version,
|
|
|
|
you're set. Otherwise it should pop up a window and prompt for installation
|
|
|
|
of the command line tools.
|
|
|
|
* Install the seL4 Python dependencies, for instance using `sudo easy_install
|
|
|
|
sel4-deps`. `easy_install` is part of Python's [`setuptools`][9].
|
|
|
|
* Install the [`misc/scripts/cpp`](misc/scripts/cpp) wrapper for clang, by
|
|
|
|
putting it in `~/bin`, or somewhere else in your `PATH`.
|
|
|
|
|
2015-01-27 00:14:51 +00:00
|
|
|
Contributing
|
|
|
|
------------
|
|
|
|
|
|
|
|
Contributions to this repository are welcome.
|
|
|
|
Please read [`CONTRIBUTING.md`](CONTRIBUTING.md) for details.
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
Overview
|
|
|
|
--------
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
The repository is organised as follows.
|
|
|
|
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`spec`](spec/): a number of different formal specifications of seL4
|
|
|
|
* [`abstract`](spec/abstract/): the functional abstract specification of seL4
|
2018-03-26 05:28:34 +00:00
|
|
|
* [`sep-abstract`](spec/sep-abstract/): an abstract specification for a reduced
|
|
|
|
version of seL4 that is configured as a separation kernel
|
2016-05-24 05:59:17 +00:00
|
|
|
* [`haskell`](spec/haskell/): Haskell model of the seL4 kernel, kept in sync
|
|
|
|
with the C code
|
2014-07-28 01:59:57 +00:00
|
|
|
* [`machine`](spec/machine/): the machine interface of these two specifications
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`cspec`](spec/cspec/): the entry point for automatically translating the seL4 C code
|
2014-07-22 22:35:05 +00:00
|
|
|
into Isabelle
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`capDL`](spec/capDL/): a specification of seL4 that abstracts from memory content and
|
2014-07-22 22:35:05 +00:00
|
|
|
concrete execution behaviour, modelling the protection state of the
|
|
|
|
system in terms of capabilities. This specification corresponds to the
|
2014-07-24 00:49:32 +00:00
|
|
|
capability distribution language *capDL* that can be used to initialise
|
2014-07-22 22:35:05 +00:00
|
|
|
user-level systems on top of seL4.
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`take-grant`](spec/take-grant/): a formalisation of the classical take-grant security
|
2014-07-22 22:35:05 +00:00
|
|
|
model, applied to seL4, but not connected to the code of seL4.
|
|
|
|
|
2018-03-26 05:28:34 +00:00
|
|
|
* There are additional specifications that are not tracked in this repository,
|
|
|
|
but are generated from other files:
|
|
|
|
* [`design`](spec/design/): the design-level specification of seL4,
|
|
|
|
generated from the Haskell model.
|
|
|
|
* [`c`](spec/cspec/c/): the C code of the seL4 kernel, preprocessed into a form that
|
|
|
|
can be read into Isabelle. This is generated from the [seL4 repository](../seL4).
|
|
|
|
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`proof`](proof/): the seL4 proofs
|
2014-07-28 01:59:57 +00:00
|
|
|
* [`invariant-abstract`](proof/invariant-abstract/): invariants of the seL4 abstract specification
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`refine`](proof/refine/): refinement between abstract and design specifications
|
|
|
|
* [`crefine`](proof/crefine/): refinement between design specification and C semantics
|
2014-07-28 01:59:57 +00:00
|
|
|
* [`access-control`](proof/access-control/): integrity and authority confinement proofs
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`infoflow`](proof/infoflow/): confidentiality and intransitive non-interference proofs
|
|
|
|
* [`asmrefine`](proof/asmrefine/): Isabelle/HOL part of the seL4 binary verification
|
2014-07-28 01:59:57 +00:00
|
|
|
* [`drefine`](proof/drefine/): refinement between capDL and abstract specification
|
|
|
|
* [`sep-capDL`](proof/sep-capDL/): a separation logic instance on capDL
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`capDL-api`](proof/capDL-api/): separation logic specifications of selected seL4 APIs
|
|
|
|
|
|
|
|
* [`lib`](lib/): generic proof libraries, proof methods and tools. Among these,
|
2014-07-22 22:35:05 +00:00
|
|
|
further libraries for fixed-size machine words, a formalisation of state
|
|
|
|
monads with nondeterminism and exceptions, a generic verification condition
|
|
|
|
generator for monads, a recursive invariant prover for these (`crunch`), an
|
2014-08-11 05:41:39 +00:00
|
|
|
abstract separation logic formalisation, a prototype of the [Eisbach][6] proof
|
2014-07-22 22:35:05 +00:00
|
|
|
method language, a prototype `levity` refactoring tool, and others.
|
|
|
|
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`tools`](tools/): larger, self-contained proof tools
|
2014-07-28 01:59:57 +00:00
|
|
|
* [`asmrefine`](tools/asmrefine/): the generic Isabelle/HOL part of the binary
|
|
|
|
verification tool
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`c-parser`](tools/c-parser/): a parser from C into the Simpl language in Isabelle/HOL.
|
2014-07-22 22:35:05 +00:00
|
|
|
Includes a C memory model.
|
2014-07-28 01:59:57 +00:00
|
|
|
* [`autocorres`](tools/autocorres/): an automated, proof-producing abstraction tool from
|
2014-07-22 22:35:05 +00:00
|
|
|
C into higher-level Isabelle/HOL functions, based on the C parser above
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`haskell-translator`](tools/haskell-translator/): a basic python script for converting the Haskell
|
2014-07-22 22:35:05 +00:00
|
|
|
prototype of seL4 into the executable design specification in
|
|
|
|
Isabelle/HOL.
|
|
|
|
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`misc`](misc/): miscellaneous scripts and build tools
|
2014-07-28 01:59:57 +00:00
|
|
|
|
|
|
|
* [`camkes`](camkes/): an initial formalisation of the CAmkES component platform
|
2014-07-22 22:35:05 +00:00
|
|
|
on seL4. Work in progress.
|
|
|
|
|
2014-07-24 00:49:32 +00:00
|
|
|
* [`sys-init`](sys-init/): specification of a capDL-based, user-level system initialiser
|
2014-07-22 22:35:05 +00:00
|
|
|
for seL4, with proof that the specification leads to correctly initialised
|
|
|
|
systems.
|
|
|
|
|
|
|
|
|
2014-08-11 05:41:39 +00:00
|
|
|
[6]: http://www.nicta.com.au/pub?id=7847 "An Isabelle Proof Method Language"
|
2014-07-28 01:59:57 +00:00
|
|
|
|
2014-07-28 19:27:46 +00:00
|
|
|
|
2019-04-19 08:12:58 +00:00
|
|
|
Hardware requirements
|
2014-08-03 03:01:58 +00:00
|
|
|
------------
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2015-04-21 14:55:43 +00:00
|
|
|
Almost all proofs in this repository should work within 4GB of RAM. Proofs
|
|
|
|
involving the C refinement, will usually need the 64bit mode of polyml and
|
2015-05-25 21:47:54 +00:00
|
|
|
about 16GB of RAM.
|
2015-04-21 14:55:43 +00:00
|
|
|
|
|
|
|
The proofs distribute reasonably well over multiple cores, up to about 8
|
2015-05-25 21:47:54 +00:00
|
|
|
cores are useful.
|
2015-04-21 14:55:43 +00:00
|
|
|
|
2014-08-03 03:01:58 +00:00
|
|
|
|
|
|
|
Isabelle Setup
|
|
|
|
--------------
|
|
|
|
|
2019-04-19 08:12:58 +00:00
|
|
|
After the repository is set up using `repo` (as per the [setup section](#setup) above), you
|
|
|
|
should have following directory structure, where `l4v` is the repository you
|
|
|
|
are currently looking at:
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2019-04-19 08:12:58 +00:00
|
|
|
```bash
|
|
|
|
verification/
|
|
|
|
isabelle/
|
|
|
|
l4v/
|
|
|
|
seL4/
|
|
|
|
```
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
To set up Isabelle for use in `l4v/`, assuming you have no previous
|
|
|
|
installation of Isabelle, run the following commands in the directory
|
|
|
|
`verification/l4v/`:
|
|
|
|
|
2019-04-19 08:12:58 +00:00
|
|
|
```bash
|
|
|
|
mkdir -p ~/.isabelle/etc
|
|
|
|
cp -i misc/etc/settings ~/.isabelle/etc/settings
|
|
|
|
./isabelle/bin/isabelle components -a
|
|
|
|
./isabelle/bin/isabelle jedit -bf
|
|
|
|
./isabelle/bin/isabelle build -bv HOL-Word
|
|
|
|
```
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
These commands perform the following steps:
|
|
|
|
|
|
|
|
* create an Isabelle user settings directory.
|
|
|
|
* install L4.verified Isabelle settings.
|
|
|
|
These settings initialise the Isabelle installation to use the standard
|
|
|
|
Isabelle `contrib` tools from the Munich Isabelle repository and set up
|
|
|
|
paths such that multiple Isabelle repository installations can be used
|
|
|
|
side by side without interfering with each other.
|
|
|
|
* download `contrib` components from the Munich repository. This includes
|
|
|
|
Scala, a Java JDK, PolyML, and multiple external provers. You should
|
|
|
|
download these, even if you have these tools previously installed
|
|
|
|
elsewhere to make sure you have the right versions. Depending on your
|
|
|
|
internet connection, this may take some time.
|
2014-07-28 01:59:57 +00:00
|
|
|
* compile and build the Isabelle PIDE jEdit interface.
|
|
|
|
* build basic Isabelle images, including `HOL-Word` to ensure that
|
2014-07-22 22:35:05 +00:00
|
|
|
the installation works. This may take a few minutes.
|
|
|
|
|
2018-06-22 14:52:35 +00:00
|
|
|
Alternatively, it is possible to use the official Isabelle2018 release
|
2014-07-22 22:35:05 +00:00
|
|
|
bundle for your platform from the [Isabelle website][2]. In this case, the
|
|
|
|
installation steps above can be skipped, and you would replace the directory
|
|
|
|
`verification/isabelle/` with a symbolic link to the Isabelle home directory
|
|
|
|
of the release version. Note that this is not recommended for development,
|
2014-07-28 01:59:57 +00:00
|
|
|
since Google repo will overwrite this link when you synchronise repositories
|
2014-07-22 22:35:05 +00:00
|
|
|
and Isabelle upgrades will have to be performed manually as development
|
|
|
|
progresses.
|
|
|
|
|
2019-05-09 08:08:22 +00:00
|
|
|
### JEdit
|
|
|
|
We provide a JEdit macro that is very useful when working with large theory
|
|
|
|
files, **goto-error**, which moves the cursor to the first error in the file.
|
|
|
|
|
|
|
|
To install the macro, run the following commands in the directory
|
|
|
|
`verification/l4v/`:
|
|
|
|
```bash
|
|
|
|
mkdir -p ~/.isabelle/jedit/macros
|
|
|
|
cp misc/jedit/macros/goto-error.bsh ~/.isabelle/jedit/macros/.
|
|
|
|
```
|
|
|
|
|
|
|
|
You can add keybindings for this macro in the usual way, by going to
|
|
|
|
`Utilities -> Global Options -> jEdit -> Shortcuts`.
|
|
|
|
|
|
|
|
Additionally, our fork of Isabelle/jEdit has an updated indenter which is more
|
|
|
|
proof-context aware than the 'original' indenter. Pressing `ctrl+i` while some
|
|
|
|
`apply`-script text is selected should auto-indent the script while respecting
|
|
|
|
subgoal depth and maintaining the relative indentation of multi-line `apply`
|
|
|
|
statements.
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
Running the Proofs
|
|
|
|
------------------
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
If Isabelle is set up correctly, a full test for the proofs in this repository
|
|
|
|
can be run with the command
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
./run_tests
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
from the directory `l4v/`.
|
|
|
|
|
2018-03-26 05:28:34 +00:00
|
|
|
Not all of the proof sessions can be built directly with the `isabelle build` command.
|
|
|
|
The seL4 verification proofs depend on Isabelle specifications that are
|
|
|
|
generated from the C source code and Haskell model.
|
|
|
|
Therefore, it's recommended to always build using the supplied makefiles,
|
|
|
|
which will ensure that these generated specs are up to date.
|
|
|
|
|
|
|
|
To do this, enter one level under the `l4v/` directory and run `make <session-name>`.
|
|
|
|
For example, to build the C refinement proof session, do
|
|
|
|
|
|
|
|
cd l4v/proof
|
|
|
|
make CRefine
|
|
|
|
|
|
|
|
As another example, to build the session for the Haskell model, do
|
|
|
|
|
|
|
|
cd l4v/spec
|
|
|
|
make ExecSpec
|
|
|
|
|
|
|
|
See the `HEAPS` variable in the corresponding `Makefile` for available targets.
|
|
|
|
|
|
|
|
Proof sessions that do not depend on generated inputs can be built directly with
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
./isabelle/bin/isabelle build -d . -v -b <session name>
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
from the directory `l4v/`. For available sessions, see the corresponding
|
|
|
|
`ROOT` files in this repository. There is roughly one session corresponding to
|
|
|
|
each major directory in the repository.
|
|
|
|
|
|
|
|
For interactively exploring, say the invariant proof of the abstract
|
|
|
|
specification with a pre-built logic image for the abstract specification,
|
|
|
|
run
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
./isabelle/bin/isabelle jedit -d . -l ASpec
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2018-05-30 05:22:20 +00:00
|
|
|
in `l4v/` and open one of the files in `proof/invariant-abstract`.
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
License
|
|
|
|
-------
|
2014-07-22 22:35:05 +00:00
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
The files in this repository are released under standard open source
|
|
|
|
licenses. Please see the individual file headers and
|
|
|
|
[`LICENSE_GPLv2.txt`](LICENSE_GPLv2.txt) and
|
2014-07-24 00:49:32 +00:00
|
|
|
[`LICENSE_BSD2.txt`](LICENSE_BSD2.txt) files for details.
|
2014-07-22 22:35:05 +00:00
|
|
|
|
|
|
|
|