Separation kernel
Encyclopedia
A separation kernel is a type of security kernel used to simulate a distributed environment. The concept was introduced by John Rushby
in a 1981 paper. 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
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
(NSA) published the Separation Kernel Protection Profile (SKPP), 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:
"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."
In September 2008, Green Hills' INTEGRITY-178B became the first separation kernel certified against the SKPP.
Wind River Systems
has separation kernel technology that was in active certification process in 2009.
John Rushby
John Rushby is a British computer scientist now based in the United States.John Rushby was born and brought up in London, where he attended Dartford Grammar School. He studied at the University of Newcastle in the UK, gaining his computer science BSc there in 1971 and his PhD in 1977.From 1974 to...
in a 1981 paper. 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
Real-time operating system
A real-time operating system is an operating system intended to serve real-time application requests.A key characteristic of a RTOS is the level of its consistency concerning the amount of time it takes to accept and complete an application's task; the variability is jitter...
products in this genre have been used by aircraft manufacturers
Aerospace manufacturer
An aerospace manufacturer is a company or individual involved in the various aspects of designing, building, testing, selling, and maintaining aircraft, aircraft parts, missiles, rockets, and/or spacecraft....
for safety-critical avionics applications.
In 2007 the Information Assurance Directorate of the U.S. National Security Agency
National Security Agency
The National Security Agency/Central Security Service is a cryptologic intelligence agency of the United States Department of Defense responsible for the collection and analysis of foreign communications and foreign signals intelligence, as well as protecting U.S...
(NSA) published the Separation Kernel Protection Profile (SKPP), a security requirements specification for separation kernels suitable to be used in the most hostile threat environments. The SKPP describes, in Common Criteria
Common Criteria
The Common Criteria for Information Technology Security Evaluation is an international standard for computer security certification...
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 CPUCentral processing unitThe central processing unit is the portion of a computer system that carries out the instructions of a computer program, to perform the basic arithmetical, logical, and input/output operations of the system. The CPU plays a role somewhat analogous to the brain in the computer. The term has been in...
, 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."
In September 2008, Green Hills' INTEGRITY-178B became the first separation kernel certified against the SKPP.
Wind River Systems
Wind River Systems
Wind River Systems, Inc. is a company providing embedded systems, development tools for embedded systems, middleware, and other types of software. The company was founded in Berkeley, California in 1981 by Jerry Fiddler and David Wilner. On June 4, 2009, Wind River announced that Intel had bought...
has separation kernel technology that was in active certification process in 2009.