MILS architecture simplifies design of high assurance systems – Part 1

MILS platform implementation approach
Two of the fundamental security policies, data isolation and periods processing, have some commonality with the two fundamental concepts of integrated modular avionics (IMA): spatial partitioning and temporal partitioning.⁷ There are also some key differences in relation to safety and security objectives, however, and while it might be convenient to reuse an existing Avionics Application Standard Software Interface (ARINC 653) real-time operating system (RTOS) implementation as the basis for a MILS implementation, this approach has some fundamental drawbacks.⁸ First, it would be costly to perform a Common Criteria security evaluation of an ARINC 653 RTOS kernel at high evaluation assurance levels (EAL) due to the relatively large size of the kernel. This is because the ARINC 653 kernel implements extensive functionality, including a health-management framework for process-level, partition-level, and module-level recovery and restarts, as well as inter-processor communications features that enable communications such as ARINC 653 blackboards between IMA applications running at the same security classification. Such functionality may not be appropriate for use in multilevel secure systems.

Second, ARINC 653 kernels can provide the option of implementing device drivers in kernel space. This approach can increase I/O performance but requires the device driver to undergo safety certification to the same level as the kernel, which in turn needs to be safety-certified to the level of the most critical application. (In cases in which the driver is sufficiently large and/or the safety level is sufficiently high, the device driver can be implemented in an I/O partition in user space instead.)

When Wind River set out to make its VxWorks RTOS MILS compliant, we started the implementation of the VxWorks MILS 2.0 separation kernel with a clean slate. We developed the kernel using state-of-the-art virtualization technology, which resulted in a secure kernel that implements the four fundamental security policies for MILS while achieving the small footprint necessary for security evaluation at Common Criteria EAL 6+ (see figure 2).

Figure 2: The VxWorks MILS 2.0 architecture features a separation kernel running in kernel mode, providing partitions or virtual boards, which contain different guest operating systems. (Courtesy of Wind River Services)

The VxWorks MILS 2.0 separation kernel is compliant with SKPP. Although the SKPP was sunsetted by NIAP on June 1, 2011, NIAP and NSA stand behind the separation kernel as a secure, foundational technology for high assurance systems. The SKPP specifies a set of security policies based on the Common Criteria security functional requirements and security assurance requirements, tailored for separation kernels. These include information flow control (information flow); resource isolation (data isolation and fault isolation); trusted recovery (data isolation and fault isolation); audit (which augments security policy); and trusted initialization and trusted delivery, which are outside the scope of the separation kernel itself. The SKPP thus provides the foundation for a MILS system and can be augmented with other components and protection profiles using a compositional approach — for example, using a secure network stack compliant with a future MILS Network Subsystem Protection Profile (MNSPP).

Data isolation
The VxWorks MILS 2.0 separation kernel uses a Type 1 or native hypervisor, which enables guest operating systems to run on top of the separation kernel in a virtualized environment. Two approaches are often used here: paravirtualization, in which the guest operating system is modified to improve system performance in the absence of hardware virtualization support; and full virtualization, in which the guest operating system runs unmodified due to the presence of hardware virtualization support.

VxWorks MILS 2.0 exploits the virtualization capabilities of modern processors such as those developed by Freescale and Intel. For processors with Intel Virtualization Technology (Intel VT), the separation kernel is able to use the processor hardware support to run guest operating systems in a virtual machine environment, or partition, on top of the separation kernel at a reduced processor privilege level. It can also prevent the guest operating system from accessing physical memory outside of its virtual machine. This data isolation is implemented and controlled solely by the separation kernel and is not dependent on the cooperation of the partitions to achieve virtualization. In the case of processors without hardware virtualization support, the separation kernel enforces data isolation using the processor’s memory management unit (MMU).

VxWorks only allows MILS 2.0 device drivers to run in partitions in processor user mode, rather than in the separation kernel in processor supervisor mode. Allowing the latter would undermine the evaluation of the trusted separation kernel and dramatically increase the size of the trusted computing base. This contrasts with some other MILS implementations that allow device driver code to run in the separation kernel, rendering it potentially vulnerable to the actions of untrusted code in the device driver.