Name
Abstract | ||
|---|---|---|
This paper proposes a generalized framework to build large, complex systems where security guarantees can be given for the overall system's implementation. The work builds on the formally proven correct seL4 micro-kernel and on its fine-grained access control. This access control mechanism allows large untrusted components to be isolated in a way that prevents them from violating a defined security property, leaving only the trusted components to be formally verified. The first steps of the approach are illustrated by the formalisation of a multi-level secure access device and a proof in Isabelle/HOL that information cannot flow from one back-end network to another. |
Year | Venue | Keywords |
|---|---|---|
2010 | SSV | large untrusted component,fine-grained access control,complex system,generalized framework,security property,security guarantee,multi-level secure access device,overall system,access control mechanism,back-end network |
Field | DocType | Citations |
HOL,Complex system,Trusted components,Computer science,Access control,Distributed computing | Conference | 17 |
PageRank | References | Authors |
0.92 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| June Andronick | 1 | 903 | 42.66 |
| David Greenaway | 2 | 30 | 1.52 |
| K. Elphinstone | 3 | 1190 | 65.76 |