Verifying the EROS Confinement Mechanism

Capability systems can be used to implement higher-level security policies including the *-property if a mechanism exists to ensure confinement. The implementation can be efficient if the "weak" access restriction described in this paper is introduced. In the course of developing EROS, a pure capability system, it became clear that verifying the correctness of the confinement mechanism was necessary in establishing the security of the operating system. This paper presents a verification of the EROS con nement mechanism with respect to a broad class of capability architectures (including EROS). We give a formal statement of the requirements, construct a model of the architecture's security policy and operational semantics, and show that architectures covered by this model enforce the confinement requirements if a small number of initial static checks on the con ned subsystem are satisfied. The method used generalizes to any capability system