High Level Specification of Non-Interference Security Policies in Partitioned MLS Systems

J. Son and J. Alves-Foss (USA)


Formal specification, IPC-capable Separation kernel, Proof of Separability, and Non-Interference.


We provide a formal framework for specifying the secure behaviors of a Separation Kernel (SK) with Inter-Partition Communication (IPC) capability which satisfy two re quirements: 1) the Multi-Level Secure (MLS) partitioned components (called partitions) running on a SK must com municate with each other through designated communica tion channels, 2) IPC operations must satisfy information flow security policies such as Non-Interference. Using this framework, we present a formal model of an IPC-capable SK architecture which satisfies Non-Interference security policies.

Important Links:

Go Back