Separation kernel

Last updated

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. [1] 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."

Contents

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), [2] a security requirements specification for separation kernels suitable to be used in the most hostile threat environments. The SKPP describes, in Common Criteria [3] 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. [2] 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. [2]

Solutions

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". [5]

The seL4 microkernel has a formal proof of concept that it can be configured as a separation kernel. [6] The enforced continuance of information [7] along with this implies it is an elevated level example of assurance. The Muen [8] separation kernel is also a formally verified open source separation kernel for x86 machines.

See also

Related Research Articles

The trusted computing base (TCB) of a computer system is the set of all hardware, firmware, and/or software components that are critical to its security, in the sense that bugs or vulnerabilities occurring inside the TCB might jeopardize the security properties of the entire system. By contrast, parts of a computer system outside the TCB must not be able to misbehave in a way that would leak any more privileges than are granted to them in accordance to the security policy.

The U.S. National Security Agency (NSA) ranks cryptographic products or algorithms by a certification called product types. Product types are defined in the National Information Assurance Glossary which defines Type 1, 2, 3, and 4 products.

The Common Criteria for Information Technology Security Evaluation is an international standard for computer security certification. It is currently in version 3.1 revision 5.

This is a list of operating systems specifically focused on security. Operating systems for general-purpose usage may be secure without having a specific focus on security.

In computer security, mandatory access control (MAC) refers to a type of access control by which the operating system or database constrains the ability of a subject or initiator to access or generally perform some sort of operation on an object or target. In the case of operating systems, a subject is usually a process or thread; objects are constructs such as files, directories, TCP/UDP ports, shared memory segments, IO devices, etc. Subjects and objects each have a set of security attributes. Whenever a subject attempts to access an object, an authorization rule enforced by the operating system kernel examines these security attributes and decides whether the access can take place. Any operation by any subject on any object is tested against the set of authorization rules to determine if the operation is allowed. A database management system, in its access control mechanism, can also apply mandatory access control; in this case, the objects are tables, views, procedures, etc.

Green Hills Software American software company

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.

Multilevel security or multiple levels of security (MLS) is the application of a computer system to process information with incompatible classifications, permit access by users with different security clearances and needs-to-know, and prevent users from obtaining access to information for which they lack authorization. There are two contexts for the use of multilevel security. One is to refer to a system that is adequate to protect itself from subversion and has robust mechanisms to separate information domains, that is, trustworthy. Another context is to refer to an application of a computer that will require the computer to be strong enough to protect itself from subversion and possess adequate mechanisms to separate information domains, that is, a system we must trust. This distinction is important because systems that need to be trusted are not necessarily trustworthy.

INTEGRITY and INTEGRITY-178B are real-time operating systems (RTOSes) produced and marketed by Green Hills Software.

Multiple single-level or multi-security level (MSL) is a means to separate different levels of data by using separate computers or virtual machines for each level. It aims to give some of the benefits of multilevel security without needing special changes to the OS or applications, but at the cost of needing extra hardware.

PikeOS Real-time operating system

PikeOS is a commercial, hard real-time operating system (RTOS) that offers a separation kernel based hypervisor with multiple logical partition types for many other operating systems (OS), each called a GuestOS, and applications. It enables users to build certifiable smart devices for the Internet of things (IoT) according to the high quality, safety and security standards of different industries. For safety and security critical real-time applications on controller-based systems without memory management unit (MMU) but with memory protection unit (MPU) PikeOS for MPU is available.

The XTS-400 is a multilevel secure computer operating system. It is multiuser and multitasking that uses multilevel scheduling in processing data and information. It works in networked environments and supports Gigabit Ethernet and both IPv4 and IPv6.

A Protection Profile (PP) is a document used as part of the certification process according to ISO/IEC 15408 and the Common Criteria (CC). As the generic form of a Security Target (ST), it is typically created by a user or user community and provides an implementation independent specification of information assurance security requirements. A PP is a combination of threats, security objectives, assumptions, security functional requirements (SFRs), security assurance requirements (SARs) and rationales.

Common Criteria Evaluation and Validation Scheme

Common Criteria Evaluation and Validation Scheme (CCEVS) is a United States Government program administered by the National Information Assurance Partnership (NIAP) to evaluate security functionality of an information technology with conformance to the Common Criteria international standard. The new standard uses Protection Profiles and the Common Criteria Standards to certify the product. This change happened in 2009. Their stated goal in making the change was to ensure achievable, repeatable and testable evaluations.

The Common Criteria model provides for the separation of the roles of evaluator and certifier. Product certificates are awarded by national schemes on the basis of evaluations carried by independent testing laboratories.

Multiple Independent Levels of Security/Safety (MILS) is a high-assurance security architecture based on the concepts of separation and controlled information flow. It is implemented by separation mechanisms that support both untrusted and trustworthy components; ensuring that the total security solution is non-bypassable, evaluatable, always invoked, and tamperproof.

LynxSecure is a least privilege real-time separation kernel hypervisor from Lynx Software Technologies designed for safety and security critical applications found in military, avionic, industrial, and automotive markets.

An embedded hypervisor is a hypervisor that supports the requirements of embedded systems.

Trusted Computer System Evaluation Criteria

Trusted Computer System Evaluation Criteria (TCSEC) is a United States Government Department of Defense (DoD) standard that sets basic requirements for assessing the effectiveness of computer security controls built into a computer system. The TCSEC was used to evaluate, classify, and select computer systems being considered for the processing, storage, and retrieval of sensitive or classified information.

Fishbowl is a mobile phone architecture developed by the U.S. National Security Agency (NSA) to provide a secure Voice over IP (VoIP) capability using commercial grade products that can be approved to communicate classified information. It is the first phase of NSA's Enterprise Mobility Architecture. According to a presentation at the 2012 RSA Conference by Margaret Salter, a Technical Director in the Information Assurance Directorate, "The plan was to buy commercial components, layer them together and get a secure solution. It uses solely commercial infrastructure to protect classified data." Government employees were reportedly testing 100 of the phones as of the announcement.

In information security, a guard is a device or system for allowing computers on otherwise separate networks to communicate, subject to configured constraints. In many respects a guard is like a firewall and guards may have similar functionality to a gateway.

References

  1. 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).
  2. 1 2 3 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.
  3. "Common Criteria for Information Technology Security Evaluation," Version 3.1, CCMB-2006-09-001, 002, 003, September 2006.
  4. http://www.niap-ccevs.org/cc-scheme/st/st_vid10119-st.pdf [ bare URL PDF ]
  5. https://www.niap-ccevs.org/pp/archived/PP_SKPP_HR_V1.03/
  6. "The L4.verified Proofs". GitHub . 18 November 2021.
  7. https://www.nicta.com.au/publications/research-publications/?pid=6464
  8. https://muen.sk/muen-report.pdf [ bare URL PDF ]