A Gypsy-Based Kernel

Several members of the Research and Development Office at the DoD Computer Security Center are involved in an in-house research effort on security kernels called VIKING (Verified Implementationof a Kernel IN Gypsy). The primary objective of this work is to provide formally verified implementation of security kernel targeted specifically for communications applications. For this reason, the VIKING kernel is a "separation kernel"; its requirements are different from previous general purpose operating system security kernels. This kernel will not directly enforce traditional multilevel security (MLS), but will instead form a foundation for the security of application programs. MLS properties enforced in the application will be proved based on the fundamental properties proved in the kernel. The kernel will support concurrency, interprocess communication (IPC), and will enforce isolation between processes. The kernel performs these functions by implementing the Gypsy cobegin and buffer communication mechanisms.