A Family of Securable Protection Systems

This paper describes Metagap'e, a formally specified family of capability systems capable of restricting the transfer of both information and access rights. Previous work indicates that the identification of such architectures is difficult, and in most cases their verification is undecidable. To the best of our knowledge, Metagap'e spans all real capability systems known to support the confinement property, and excludes all known systems that do not. One test of effectiveness for a protection system is its ability to enforce the confinement property, which requires that information be contained within well-specified boundaries. This paper demonstrates a proof of correctness of Metagap'e with respect to confinement. We show that the model enforces the confinement requirements if a small number of initial static checks on the confined subsystem are satisfied. Keywords: proof of correctness, capability systems, operating systems, confinement, verification, formal specification. 1 Introd..