Safety Critical Products: Integrity-178B real-time OS

Very, well-designed separation kernel. The main competitors in this space are LynxSecure, VxWorks MILS, and PikeOS. There's others but all of these target security. The advantage of a separation kernel is it (a) has tiny attack surface; (b) is efficient, eg cache-friendly; (c) is easy to analyse; (d) has necessary features for isolation, mediation of communication, & covert channel suppression. INTEGRITY-178B's EAL6 evaluation against SKPP means it went through around two years of analysis, testing, and pen testing by an evaluator plus NSA. Within the evaluated portion/usage, it should do exactly what it says and with high security. Still gotta protect under and around that.

Contrary to acveilleux's claim, the separation kernels can be used for all kinds of things much like the security kernels before them. Security kernels were used in thin clients, UNIX clones, VPN's, mail guards, web servers, file storage, embedded systems, a Scheme implementation, and so on. If Scheme isn't flexible, I don't know what is. ;) The separation kernels do similar isolation and have been used to do most of the above. A recent addition is virtualization of Windows and Linux desktops, which is supported by every commercial kernel. Dell Consolidated Client is one implementation using INTEGRITY-178B backed by their INTEGRITY Global Security company that markets it. Only gripe with Green Hills is their marketing department is so full of shit that I've had to bust them out plenty of times.

Note: Kleidermacher et al actually wrote a book [1] on their approach to embedded design that many claimed to enjoy. Haven't read it myself yet. Might help others trying to duplicate the good aspects. You can also find descriptions of their PHASE development methodology with Google.

Anyway, the other component that was critical to MILS or separation kernel models was the middleware: how the partitions interact. The kernel can enforce static flows of information. However, dynamic flows need another enforcer to identify them, optionally inspect traffic, and decide if it's allowed. These end up using a single node as a message router/guard, guards on input within a partition, or partitions specifically designed as guards. Various tradeoffs in performance and security there. So, for dynamic systems, you typically need to secure isolation and at least part of middleware.

There's hardware, firmware, and software methods to deal with many of the rests of the risks. It's not uncommon seeing a combination of a separation kernel like INTEGRITY-178B with custom, rigorously-built drivers and apps on a carefully chosen Ada runtime. Holistic approaches are still best for risk reduction even with strong isolation of a separation kernel.

Far as open-source and general-purpose, closest things to this are the Genode Architecture [2], Nizza Architecture [3], Muen Separation Kernel [4], and seL4 kernel [5]. Readiness, features, assurance, etc vary considerably. GenodeOS is most promising as they incorporate, rather than ignore, advances in INFOSEC research. They actually started out that way then incorporated similarly strong work (eg Nitpicker GUI). Anyone looking for a Masters or Ph.D project should look for fundamental flaws or improvements in their architecture along with submitting that back to team. Formal analysis or proof of it against invariants or known issues would be nice.

[1] http://www.amazon.com/Embedded-Systems-Security-Practical-De...

[2] http://http://genode.org/documentation/general-overview/

[3] http://genode-labs.com/publications/mikro-sina-2005.pdf

[4] http://muen.sk/

[5] https://sel4.systems/

The more limitations you're willing to impose on the applications, the easier it is to make precise and strict behaviour promises in the O/S:

> The kernel's design guarantees bounded computation times by eliminating features such as dynamic memory allocation.

It's no surprise that Green Hill is going for embedded security device market now. Once you have the robust partitioning required for avionics it's mostly a matter of documenting how the same features allow for security...