Confinement is an essential feature of any secure component-based system. This paper presents a proof of correctness of the operating system architecture with respect to confinement. We give a formal statement of the requirements, construct a model of the architecture's security policy and operational semantics, and develop a formal methodology for verifying confinement policy.
展开▼
