Applying the composition principle to verify a hierarchy of security servers
Mark R. Heckman, Karl Levitt · 2002
This paper describes how the composition principle of Abadi and Lamport (1991) can be applied to specify and compose systems where access control policies are distributed among a hierarchy of agents. Examples of such systems are layered secure operating systems, where the mandatory access control policy is enforced by the lowest system layer and discretionary and application-specific policies are implemented by outer layers, and microkernel operating systems, where the access control policy may be distributed among a hierarchy of server processes. We specifically consider the case of a microkernel operating system type architecture, in which resource management policies are enforced by server processes outside of the kernel, and where the system access control policy is a composition of the distinct policies implemented by the servers. As an example, we have specified a two-server system, including both safety and progress properties. We formally verified the composition of the two server processes using the HOL theorem proving system.