D-MILS Project Overview

The objective of the D-MILS is to provide an environment for the design, analysis, verification, compositional implementation and certification of scalable, interoperable, and affordable trustworthy architectures. D-MILS uses an advanced time-triggered network architecture for communication among its nodes, providing, predictable, deterministic behaviour for safety-, security-, and enterprise-critical operation.

High-level Language

D-MILS provides an end-to-end and top-to-bottom solution for certifiable highly-dependable systems that starts from a high-level, declarative (and graphical) language, the Architecture Analysis and Design Language (AADL), and provides a complete machine-processable chain of representations, usable within a verification framework providing sophisticated analysis and verification of probabilistic and non-probabilistic properties in both finite- and infinite state systems, all the way down to the automated compilation of the detailed resource, schedule, and interaction policy configurations of a distributed collection of single- and multi-processor MILS platform nodes.


D-MILS establishes a concrete linkage between the assurance activities performed at various levels of the system specification, design and implementation, and the high-level claims (and derivative sub-claims) made for the complete D-MILS system, using another declarative language, Goal Structuring Notation (GSN), to represent the assurance case for the system, with an automated connection to the component- and composition-centric verification framework

Flow Control

The implementation of D-MILS systems depend upon the use of a separation kernel/hypervisor, a high-assurance virtual machine monitor (VMM) that enforces information flow control and deterministic execution in addition to providing isolation as do ordinary VMMs. This provides a strong basis for protection, assurance and integrity in a virtualization environment.


D-MILS is strictly oriented to demonstrable assurance of security, safety, and other dependability attributes of its distributed systems. D-MILS builds upon a foundation of high-assurance components, combined within a scientifically-based framework for composition, that permits the security and dependability attributes of the composite to be computed from the properties of the components and the manner (architecture) of their composition.

Critical System Support

Because of the strong analytical environment being assembled in the D-MILS project, and the concrete linkage between evidence and system claims, established by the assurance case, some of the most important application domains for D-MILS are critical service infrastructures, utilities, transportation, energy, communication, and critical financial and economic systems. Because all phases of the system specification, analysis, and implementation are expressed in a common set of formally-specified representations, D-MILS will provide an unprecedented opportunity for instrumentation from end-to-end and top-to-bottom, both during development and at runtime.


D-MILS features a runtime monitoring plane implemented within the architectural framework, making it possible to safely and securely deploy any form of monitoring that serves the testing, diagnosis, assessment, auditing, and management of a D-MILS system. Instrumentation within a D-MILS system can be more effective, and far safer, than in conventional systems because of the strong isolation that can be provided, the monitoring implementation and the data that it gathers.

D-MILS Partners









© 2017   Created by Scott Hansen.   Powered by

Badges  |  Report an Issue  |  Terms of Service