Commercial real-time operating system products in this genre have been used by aircraft manufacturers for safety-critical avionics applications.
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.
[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.
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".