Name
Abstract | ||
|---|---|---|
We prove that the seL4 microkernel enforces two high-level access control properties: integrity and authority confinement. Integrity provides an upper bound on write operations. Authority confinement provides an upper bound on how authority may change. Apart from being a desirable security property in its own right, integrity can be used as a general framing property for the verification of user-level system composition. The proof is machine checked in Isabelle/HOL and the results hold via refinement for the C implementation of the kernel. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22863-6_24 | ITP |
Keywords | Field | DocType |
desirable security property,authority confinement,sel4 microkernel,own right,c implementation,general framing property,user-level system composition,high-level access control property | Kernel (linear algebra),HOL,Framing (construction),Computer science,Upper and lower bounds,Algorithm,Microkernel,Access control | Conference |
Citations | PageRank | References |
24 | 1.03 | 14 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Sewell | 1 | 914 | 37.60 |
| Simon Winwood | 2 | 713 | 30.07 |
| Peter Gammie | 3 | 48 | 2.29 |
| Toby Murray | 4 | 242 | 17.03 |
| June Andronick | 5 | 903 | 42.66 |
| Gerwin Klein | 6 | 1450 | 87.47 |