1<!--
2     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4     SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7Access Control Proof
8====================
9
10This proof establishes that seL4 enforces the security properties of
11*authority confinement* and *integrity*. These are essential correctness
12properties of its capability-based access control system: authority
13confinement means that authority propagates only in accordance with
14capabilities, and integrity means that data cannot be modified without
15possession of an appropriate *write* capability to the data. These
16properties and proofs are described in detail in an ITP 2011 [paper][1].
17These properties are phrased over seL4's
18[abstract specification](../../spec/abstract/) and this proof builds on
19top of the [Abstract Spec Invariant Proof](../invariant-abstract/).
20
21  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_WGMAK_11.abstract.pml "seL4 Enforces Integrity"
22
23
24Building
25--------
26
27To build from the `l4v/` directory, run:
28
29    ./isabelle/bin/isabelle build -d . -v -b Access
30
31
32Important Theories
33------------------
34
35The top-level theory where these two properties are proved for the
36kernel is [`Syscall_AC`](Syscall_AC.thy); the bottom-level theory where
37the properties are defined is [`Access`](Access.thy).
38
39