Microkernel Application Information fLow with Logic-based Enforcement (MAILLE)

Security certification of software for life- and mission-critical systems impacts both cost and schedule. While some microkernels offer significant safety and security advantages over classic operating system and real-time operating system approaches, it remains difficult to certify the resulting systems. It is also easy to construct unsafe and insecure systems based on microkernels. The proposed Microkernel Application Information fLow with Logic-based Enforcement (MAILLE) will be a usable development and verification environment for mixed-criticality and multiple independent levels of security (MILS) embedded systems. MAILLE targets systems that require safety and security guarantees from the kernel through user space applications. MAILLE leverages advances in microkernels, highly disaggregated separation architectures, model-based system engineering (MBSE), and integrated verification environments. A model-based front-end enables specification of the system components, integrated model-level and code-level information flow discovery, and enforcement, configuration, and code generation tools. These tools will directly implement the modeled system onto the desired microkernel. MAILLE will include a path for formal correctness, as well as effective tools that scale to real systems, providing system analysis, trust, and use of separation architectures by enabling development in a semantically sound approach across the system.