Date Added: Aug 2010
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 fulfill requirements relating to isolation and information flow, and that there is a direct connection to the actual capability distribution in the system. The authors claim that, in order to do this effectively, systems need to have explicit descriptions of their capability distributions. This paper presents the capDL capability distribution language for the capability-based seL4 microkernel.