A separation kernel is a type of security
kernel
Kernel may refer to:
Computing
* Kernel (operating system), the central component of most operating systems
* Kernel (image processing), a matrix used for image convolution
* Compute kernel, in GPGPU programming
* Kernel method, in machine learn ...
used to simulate a distributed environment. The concept was introduced by
John Rushby
John Rushby (born 1949) is a British computer scientist now based in the United States and working for SRI International. He previously taught and did research for Manchester University and later Newcastle University.
Early life and education
J ...
in a 1981 paper.
[John Rushby, "The Design and Verification of Secure Systems," Eighth ACM Symposium on Operating System Principles, pp. 12-21, Asilomar, CA, December 1981. (''ACM Operating Systems Review'', Vol. 15, No. 5).] Rushby proposed the separation kernel as a solution to the difficulties and problems that had arisen in the development and verification of large, complex security kernels that were intended to "provide multilevel secure operation on general-purpose multi-user systems." According to Rushby, "the task of a separation kernel is to create an environment which is indistinguishable from that provided by a physically distributed system: it must appear as if each regime is a separate, isolated machine and that information can only flow from one machine to another along known external communication lines. One of the properties we must prove of a separation kernel, therefore, is that there are no channels for information flow between regimes other than those explicitly provided."
A variant of the separation kernel, the partitioning kernel, has gained acceptance in the commercial aviation community as a way of consolidating, onto a single processor, multiple functions, perhaps of
mixed criticality. Commercial
real-time operating system
A real-time operating system (RTOS) is an operating system (OS) for real-time applications that processes data and events that have critically defined time constraints. An RTOS is distinct from a time-sharing operating system, such as Unix, which m ...
products in this genre have been used by
aircraft manufacturers for safety-critical avionics applications.
In 2007 the Information Assurance Directorate of the U.S.
National Security Agency
The National Security Agency (NSA) is a national-level intelligence agency of the United States Department of Defense, under the authority of the Director of National Intelligence (DNI). The NSA is responsible for global monitoring, collect ...
(NSA) published the Separation Kernel Protection Profile (SKPP),
[Information Assurance Directorate, National Security Agency, Fort George G. Meade, MD. "U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness," Version 1.03, June 2007.] a security requirements specification for separation kernels suitable to be used in the most hostile threat environments. The SKPP describes, in
Common Criteria parlance, a class of modern products that provide the foundational properties of Rushby's conceptual separation kernel. It defines the security functional and assurance requirements for the construction and evaluation of separation kernels while yet providing some latitude in the choices available to developers.
The SKPP defines separation kernel as "hardware and/or firmware and/or software mechanisms whose primary function is to establish, isolate and separate multiple partitions and control information flow between the subjects and exported resources allocated to those partitions." Further, the separation kernel's core functional requirements include:
* Protection of all resources (including
CPU, memory and devices) from unauthorized access.
* Separation of internal resources used by the Target of Evaluation Security Functions (TSF) from exported resources made available to subjects.
* Partitioning and isolation of exported resources.
* Mediation of information flows between partitions and between exported resources.
* Audit services.
The separation kernel allocates all exported resources under its control into partitions. The partitions are isolated except for explicitly allowed information flows. The actions of a subject in one partition are isolated from (viz., cannot be detected by or communicated to) subjects in another partition, unless that flow has been allowed. The partitions and flows are defined in configuration data. Note that 'partition' and 'subject' are orthogonal abstractions. 'Partition,' as indicated by its mathematical genesis, provides for a set-theoretic grouping of system entities, whereas 'subject' allows us to reason about the individual active entities of a system. Thus, a partition (a collection, containing zero or more elements) is not a subject (an active element), but may contain zero or more subjects.
The separation kernel provides to its hosted software programs high-assurance partitioning and information flow control properties that are both tamperproof and non-bypassable. These capabilities provide a configurable trusted foundation for a variety of system architectures.
Solutions
*
PikeOS combines separation kernel hypervisor technology with hard real-time capabilities.
*
INTEGRITY-178B
INTEGRITY and INTEGRITY-178B are real-time operating systems (RTOSes) produced and marketed by Green Hills Software.
INTEGRITY
INTEGRITY is POSIX-certified and intended for use in embedded systems of 32-bits or 64-bits. Supported computer arch ...
from
Green Hills Software
Green Hills Software is a privately owned company that builds operating systems and programming tools for embedded systems. The firm was founded in 1982 by Dan O'Dowd and Carl Rosenberg. Its world headquarters are in Santa Barbara, California.
...
In September 2008 it became the first separation kernel certified against the SKPP.
*
Wind River Systems
Wind River Systems, also known as Wind River (trademarked as Wndrvr), is an Alameda, California–based company, subsidiary of Aptiv PLC. The company develops embedded system and cloud software consisting of real-time operating systems software, ...
has separation kernel technology that was in active certification process in 2009.
*
Lynx Software Technologies
Lynx Software Technologies, Inc. (formerly LynuxWorks) is a San Jose, California software company founded in 1988. Lynx specializes in secure virtualization and open, reliable, certifiable real-time operating systems (RTOSes). Originally known as ...
has a separation kernel,
LynxSecure.
In 2011, the Information Assurance Directorate sunset the SKPP. NSA will no longer certify specific operating systems, including separation kernels against the SKPP, noting "conformance to this protection profile, by itself, does not offer sufficient confidence that national security information is appropriately protected in the context of a larger system in which the conformant product is integrated".
The
seL4 microkernel has a formal proof of concept that it can be configured as a separation kernel. The enforced continuance of information along with this implies it is an elevated level example of assurance. The Muen
[https://muen.sk/muen-report.pdf ] separation kernel is also a formally verified open source separation kernel for x86 machines.
See also
* For a computer security architecture based on a separation kernel see
Multiple Independent Levels of Security.
*
Chroot
A chroot on Unix and Unix-like operating systems is an operation that changes the apparent root directory for the current running process and its children. A program that is run in such a modified environment cannot name (and therefore normall ...
*
FreeBSD jail
The jail mechanism is an implementation of FreeBSD's OS-level virtualisation that allows system administrators to partition a FreeBSD-derived computer system into several independent mini-systems called ''jails'', all sharing the same kernel, with ...
*
Operating-system-level virtualization
OS-level virtualization is an operating system (OS) paradigm in which the kernel allows the existence of multiple isolated user space instances, called ''containers'' (LXC, Solaris containers, Docker, Podman), ''zones'' (Solaris containers), '' ...
References
{{Operating system
Distributed computing
Operating system kernels