Name
Abstract | ||
|---|---|---|
While intransitive noninterference is a natural property for any secure OS kernel to enforce, proving that the implementation of any particular general-purpose kernel enforces this property is yet to be achieved. In this paper we take a significant step towards this vision by presenting a machine-checked formulation of intransitive noninterference for OS kernels, and its associated sound and complete unwinding conditions, as well as a scalable proof calculus over nondeterministic state monads for discharging these unwinding conditions across a kernel's implementation. Our ongoing experience applying this noninterference framework and proof calculus to the seL4 microkernel validates their utility and real-world applicability. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-35308-6_12 | CPP |
Keywords | Field | DocType |
machine-checked formulation,particular general-purpose kernel,os kernel,associated sound,intransitive noninterference,system kernel,proof calculus,noninterference framework,secure os kernel,scalable proof calculus,natural property,scheduling,refinement,information flow | Kernel (linear algebra),Information flow (information theory),Nondeterministic algorithm,Computer science,Scheduling (computing),Proof calculus,Algorithm,Microkernel,Theoretical computer science,Monad (functional programming),Scalability | Conference |
Citations | PageRank | References |
18 | 0.74 | 15 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Toby Murray | 1 | 242 | 17.03 |
| Daniel Matichuk | 2 | 129 | 6.01 |
| Matthew Brassil | 3 | 18 | 0.74 |
| Peter Gammie | 4 | 48 | 2.29 |
| Gerwin Klein | 5 | 1450 | 87.47 |