Research and development within the D-MILS project was completed at the end of October 2015. The following public reports describing new technologies from the project are available for download.
Requirements for distributed MILS technology
The requirements presented in this document cover the following key project technology areas: Graphical and Declarative Languages; Integration of GSN and AADL; Representation Semantics and Transformations; Compositional Verification; Compositional Assurance Cases; Configuration Compiler; and, Distributed MILS Platform. The technology requirements are intended to provide the necessary foundation to implement two targeted industrial use cases, and to be ample for other applications as well.
Specification of AADL/MILS
This document describes the syntax of a MILS dialect of the Architecture Analysis and Design Language (AADL), denoted by MILS-AADL. Essential features of this new language are component definitions in terms of interfaces and implementations, their interaction and dynamic activation, architecture refinement, error modelling, and security-related mechanisms such as encryption and authentication, and the ability to analyse security- and safety-related behavioural constraints. This goal is achieved by extending a core fragment of AADL by new features to support the representation of security architectures and their effect on quantitative system attributes.
Translation of AADL/MILS into formal architectural modeling framework
The logical and technical architectural and platform modeling of distributed MILS requires an intermediate formal language representation on its own. A central part of the D-MILS tool chain will therefore be a cross-compiler that translates high-level to such intermediate representations. To guarantee the correctness of this approach, it is necessary for both the high-level and the intermediate language to have a precise formal semantics, and to have that semantics preserved by the translation. The aim of this document is to describe the MILS-AADL features for policy architecture and platform modeling, and to specify their translation into the intermediate representation.
Principles, syntax and notation for mapping AADL models to modular GSN
This report establishes the principles of how to map an AADL architectural model to a modular GSN argument structure. This includes general assurance argument patterns for the MILS-AADL subset. In addition, we establish the semantic mapping between AADL and modular GSN concepts. Finally, we show how the links between AADL and modular GSN can be notationally represented. Establishing these principles and patterns will help build compelling, compositional, assurance cases using MILS-AADL modelling.
Assurance arguments for AADL error models and AADL/MILS formal translations
This report describes an approach for generating an assurance argument for a D-MILS system through establishing direct relationships between D-MILS assurance argument patterns and models of the D-MILS system. Taking this integrated approach to developing the D-MILS assurance argument brings a number of advantages for any D-MILS development including greater integration with, and traceability to development artefacts, and also automating large parts of the argument construction process.
Review of the state of the art and candidate languages for intermediate representations
The D-MILS tool chain supports the verification of critical properties of a D-MILS system, the organisation of claims and evidence in an assurance case, and the automated generation of correct configurations for the D-MILS nodes and networks comprising the D-MILS platform. Back-end assurance and verification engines accept their own, sometimes unique, languages. An intermediate language serves to provide a lingua franca that is precise and amenable to translation. At the centre of the D-MILS tool chain are intermediate languages to model the evolving design of a D-MILS system throughout its development and deployment. This document describes the role of the intermediate languages in D-MILS, the necessary features, and their selection criteria.
Intermediate languages and semantics transformations for distributed MILS – part 1
D-MILS provides validation of critical system properties using formal verification techniques such as model checking. The back-end assurance and verification engines accept their own specification languages for defining the structure and behaviour of systems. A central part of the D-MILS tool chain is therefore cross-compilers that translate high-level to such intermediate representations. To guarantee the correctness of this approach, it is necessary for both the high-level and the intermediate languages to have a precise formal semantics, and to have that semantics preserved by the translations. The aim of this document is to define a formal semantics for MILS-AADL specifications, to identify the intermediate languages that are required for the various analyses.
Intermediate languages and semantics transformations for distributed MILS – part 2
A central part of the D-MILS tool chain are cross-compilers that translate high-level to intermediate representations. To guarantee the correctness of this approach, it is necessary for both the high-level and the verification languages to have a precise formal semantics, and to have that semantics preserved by the translations. The aim of this document is to define a formal semantics for MILS-AADL specifications, to identify the verification languages that are required for the various analyses, and to describe the corresponding semantics-preserving transformations from the high-level to the intermediate representations of systems.
State of the art in compositional reasoning for functional safety and security formal verification
This deliverable provides a thorough analysis of the state-of-the-art in: compositional reasoning for the verification of functional properties expressed as temporal formulas; compositional dependability assessment techniques and tools; and compositional verification techniques and tools for the analysis of security properties. Compositional techniques allow managing the inherent complexity of verification problems. In contrast to monolithical techniques, which rely on full state-space exploration and face the stateexplosition problem, compositional techniques exploit divide and conquer principles and therefore allow inferring (correctness of) properties at system level from properties on system’s components.
Compositional assurance cases and arguments for distributed MILS
This deliverable builds on the work addressing assurance arguments for AADL error models and AADL/MILS formal translations. In particular, it describes the work undertaken in two areas. First, to describe a model-based automated instantiation approach for D-MILS arguments utilising a weaving metamodel to integrate a range of system information models with D-MILS assurance argument patterns. Second, the principles and examples demonstrating how the infrastructure arguments supporting the overall D-MILS assurance case shall be constructed.
Integration of formal evidence and expression in MILS assurance case
This document describes how to integrate formal verification evidence, including evidence obtained with compositional reasoning, as part of the assurance case. In addition, it presents an approach to more formally underpinning the argument module interfaces with assume/guarantee reasoning. This provides a more compelling assurance case, increasing confidence in both the argument and the techniques used. It also improves the ability to re-use argument modules.
Compositional verification techniques and tools for distributed MILS – part 1
This document describes the principles behind the different tools used to analyse MILS-AADL models. The tools are to be called by a common interface in charge of proposing the right backend with respect to the analysis to perform. The toolset covers various types of compositional verification, including functional, real-time, security and safety properties. Methods and tools proposed here provide evidences for assurance cases that aim to assess the safety or security level of the system.
Compositional verification techniques and tools for distributed MILS – part 2
This deliverable describes the final formal framework and the corresponding formal verification methodology unifying the different verification activities for distributed MILS as result of a first iteration of the methodology and tools on the Starlight example. It will also describe the final results on the use of compositional reasoning for each of the functional, safety and security verification activities. Finally, it reports on the result of integration of the different verification subsystems in a unique toolset.
This document presents the requirements, approach, theory, design, and implementation of the configuration compiler providing the configuration automation backend for the D-MILS tool chain. The configuration compiler performs model refinement downward through a hierarchy of abstract models that are increasingly detailed in terms of MILS implementation conventions and deployment choices and options that captures low-level configuration descriptions. These can then be transliterated by adapters into the languages of the initialization functions of the foundational components comprising the D-MILS platform.
Configuration correctness and definition of semantics-preserving transformations
The D-MILS configuration compiler automatically provides a configuration file for the hardware and low-level software of the platform according to the system model. This document provides some methods to validate the the configuration file output of the configuration compiler with respect to the MILS-AADL model and the model of the platform. A MILS-AADL model is first reconstructed from the configuration files and is then compared with the original MILS-AADL model for one or several deployment constraints, encoded as relations between MILS-AADL models.
MILS console system
This document describes the implementation of MILS Console Subsystem (MCS) for D-MILS. It is implemented as a single subject running on each D-MILS node needing that feature. Since the MCS is required to simultaneously handle user interface data from multiple security/safety domains, it implements and enforces separation of such data as per its role in the MILS platform. The internal structure of the MCS is illustrated, the communication between the MCS and its clients is discussed, and the configuration and initialization of the MCS are described.
© 2014-2016 Copyright in all of the above documents and any related software remains vested in the D-MILS Project Partners