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
