Abstract | ||
---|---|---|
Capabilities provide an access control model that can be used to construct systems where safety of protection can be precisely determined. However, in order to be certain of the security provided by such systems it is necessary to verify that their capability distributions do in fact fulfil requirements relating to isolation and information flow, and that there is a direct connection to the actual capability distribution in the system. We claim that, in order to do this effectively, systems need to have explicit descriptions of their capability distributions. In this paper we present the capDL capability distribution language for the capability-based seL4 microkernel. We present the capDL model, its main features and their motivations, and provide a small example to illustrate the language syntax and semantics. CapDL plays a key role in our approach to development, analysis, and verification of trustworthy systems. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1145/1851276.1851284 | ApSys |
Keywords | Field | DocType |
access control model,explicit description,capability distribution,fact fulfil requirement,capability-based system,information flow,capdl model,direct connection,capdl capability distribution language,actual capability distribution,language syntax,security analysis | Information flow (information theory),Software engineering,Trustworthiness,Computer security,Computer science,Microkernel,Security analysis,Access control,Syntax,Semantics | Conference |
Citations | PageRank | References |
12 | 0.71 | 7 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ihor Kuz | 1 | 304 | 30.28 |
Gerwin Klein | 2 | 1450 | 87.47 |
Corey Lewis | 3 | 33 | 3.30 |
Adam Walker | 4 | 119 | 10.61 |