Design, implementation and verification of MILS systems

SUMMARY Safety-critical systems are used in many domains (military, avionics, aerospace, etc.) and handle critical data in hostile environments. To prevent data access by unauthorized subjects, they must protect and isolate information so that only allowed entities can read or write information. However, because of their increased number of functionalities, safety-critical systems design becomes more complex; this increases difficulties in the design and the verification of security functions and potential error in their implementation. The multiple independent levels of security (MILS) approach introduces rules and guidelines for the design of secure systems. It isolates data according to their security levels, reducing system complexity to ease development. However, there is no approach addressing the whole development of MILS systems from high-level specification (application components with their security levels) to the final implementation (code that executes application functions and provide security mechanisms). This paper presents a complete development approach for the design, verification and implementation of MILS architectures. It aims at providing a complete framework to build secure applications based on MILS guidelines. We describe security concerns using a modeling language, verify security requirements and automatically implement the system code generation techniques and a MILS-compliant operating system that provides security functions.