MarketSeparation kernel
Company Profile

Separation kernel

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."

Solutions
PikeOS combines separation kernel hypervisor technology with hard real-time capabilities. • INTEGRITY-178B from Green Hills Software In September 2008 it became the first separation kernel certified against the SKPP. • Wind River Systems has separation kernel technology that was in active certification process in 2009. • Lynx Software Technologies 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 separation kernel is also a formally verified open source separation kernel for x86 machines. ==See also==
tickerdossier.comtickerdossier.substack.com