salle A. Turing CE4
14 September 2012 - 14h00
MILS and DMILS project
by Rance Delong from SRI International
Abstract: Prior MILS work has focused on relatively simple applications that could be implemented on a single MILS node. These simple applications have used a modest number of subjects and objects, organized into disjoint partitions. The architecture of such systems has been simple enough that its correspondence to the configuration of the separation kernel may be validated by inspection, with rigorous assurance only for the correctness of the kernel. This approach limits the size and complexity of the problems that can be addressed by MILS. Even with simple problems, the complexity of the configuration data pushes the limits of what a person can comprehend while maintaining confidence that it implements the intended architecture.
Distributed MILS provides deterministic operation over the entire network of nodes by extending time and space partitioning to communications by using hardware-based, time-triggered Ethernet (TTEthernet) as a “backplane”.
Extensions to a separation kernel, its configuration tools, and the MILS Network Subsystem, will make it possible for a single MILS policy architecture to seamlessly span multiple MILS nodes, with predictable execution, opening many new practical application areas for MILS.
As MILS systems grow to take advantage of the capacity and capabilities of distributed MILS, the increase in complexity will exceed that which can be managed with current methodology. Large distributed MILS systems will make it imperative to design and reason about the system at a higher level of abstraction, while maintaining assurance that the system implementation is faithful to the design. The resulting increase in configuration complexity makes automated assistance indispensable for the development and verification of a distributed MILS system and its configuration data.
To enable the vision of distributed MILS, the key research problems fall into 3 primary areas: 1) high-level declarative languages to specify the architecture and refine the design of a system; 2) assurance and verification tools to provide compositional assurance that desirable system properties are achieved; and, 3) a configuration compiler that generates configuration data for the components of the distributed MILS platform that is provably consistent with the high-level declarative description and the actual available resources. The research results will be combined with existing commercial products to yield a technology that can be evaluated by industrial partners.
