Model-Driven Development for the seL4 Microkernel Using the HAMR Framework

Verified microkernels such as seL4 provide trustworthy foundations for safety- and security-critical systems. However, their full potential remains unrealized due, in part, to the lack of application development environments that help engineers integrate the microkernel’s configuration and hosting of application code with modeling, analysis, and verification tools that address broader aspects of the development lifecycle. This paper presents a model-driven tool chain for the seL4 microkernel based on the open source High Assurance Modeling and Rapid engineering (HAMR) code generation framework for the Architecture and Analysis Definition Language (AADL). We describe how the semantics of AADL communication and threading can be realized in terms of the access primitives and strong spatial and temporal partitioning mechanisms provided by seL4. For AADL users, seL4 provides a high-assurance platform with formally verified enforcement of component boundaries and communication pathways. For seL4 users, AADL provides high-level abstractions for developing seL4 applications, along with an ecosystem of system engineering and analysis tools. We illustrate the framework by applying a model-based development environment for increasing resiliency against cyber attacks to an unmanned aircraft flight control system.