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