Background: Capability systems have long been known to offer reliability advantages over current operating system architectures. Arguments have been made for and against their security advantages. Both Boebert and Karger have argued that unmodified capability systems cannot enforce mandatory access controls. Poor capability system performance has rendered the debate largely academic, and mainstream capability research was largely abandoned in the mid 1970s. Bershad and Chen have suggested that protection domain crossings have a large, intrinsic cache overhead, and have used some apparently supporting measurements to argue that microkernels (which incorporate such domain crossings) must have non-competitive performance for fundamental structural reasons.
Talk Description: In this talk (or talks), I will present two new results. The first shows that capability systems can meet or exceed the performance of conventional operating system architectures. The second is a formal specification of a policy that solves Lampson’s confinement problem and a verification that this policy is enforceable by a broad class of capability architectures. Given a working confinement mechanism, a non-kernel reference monitor can enforce mandatory access controls with only ordinary privileges and access rights.
The first result is demonstrated by EROS (the Extremely Reliable Operating System). EROS is a high-performance, unmodified (in the sense of Boebert and Karger) capability system built at the University of Pennsylvania. It is transparently persistent; all user-mode state, including processes, is periodically saved with low overhead. It is a modular, microkernel-style system. In spite of this, microbenchmarks show that it meets or exceeds the performance of the latest Linux kernel on semantically comparable operations. [This generation of Linux has incorporated significant optimizations in the areas of these microbenchmarks.] Our talk will show how this performance was accomplished.
The second result is joint work with Sam Weber (now at IBM T.J. Watson Research Center). We have modeled a class of capability systems, formally specified a confinement policy in terms of the protection state of the system, defined an operational semantics for the model, and verified that confinement is enforced given a set of initial static preconditions. In the process, we have identified two lemmas that seem of general use in operating system design and a property of capability systems that particularly seems to support successful information flow analysis.