The Collins Aerospace INSPECTA project (part of the DARPA PROVERS program) aims to provide a model-based development tool chain with integrated formal methods for building verified applications on the verified seL4 microkernel. The High Assurance Modeling and Rapid engineering for embedded systems (HAMR) framework, whose development is led by researchers at Kansas State University, is a key part of the INSPECTA tool chain. As originally developed on the DARPA CASE project within Collins Aerospace team and on other US Department of Defense projects led by Galois, HAMR supported system modeling using the SAE standard AADL modeling language. On these projects, HAMR generated infrastructure code and application code thread skeletons in C and in Slang (a safety-critical subset of Scala developed at Kansas State University). In this talk, we describe a number of new capabilities of HAMR developed on the INSPECTA project. First, the modeling layer of HAMR has been extended to support SysMLv2 – a new version of the widely used SysML modeling language standardized by the Object Modeling Group (OMG). We describe how HAMRsupported AADL based formal specifications and tooling, including the GUMBO behavior contract language, are integrated within SysMLv2 modeling environments. Second, we have extended HAMR’s code generation to support the Rust programming language and the seL4 microkit kernel configuration framework. This provides both C and Rust-based development of application components on seL4. HAMR auto-generates kernel configurations and system builds that integrate application code (and virtual machines, e.g., with legacy code) with the configured kernel and microkit-based infrastructure components (network stacks, drivers, etc.) with support for cloud-based continuous integration. We have extended HAMR Rust code generation to automatically translate GUMBO model-level behavior specifications into (a) automated property-based testing infrastructure using the Rust PropTest libraries, (b) code-level formal contract specifications (enabling Rust code to be verified to conform to contracts using the Verus verification tool from CMU), and (c) automatically generated run-time monitoring infrastructure that enables contract semantics to be monitored during system testing or deployments. 

This talk addresses the HCSS Beyond AI “Models and representations for software knowledge” theme. Through its supported architecture specifications, the HAMR tool chain provides a variety of ways to represent knowledge of critical systems including component interfaces and system design, nonfunctional properties such as timing constraints (leveraged for schedule generation and enforced via seL4 time partitioning), memory/resource utilization, configuration directives for underlying communication and spatial partitioning (enforced by seL4), as well as formal behavior constraints integrated and managed in a uniform manner across multiple layers of abstraction (models, code, kernel communication layers) --- with the constraints being verified by automated testing, formal verification, and run-time monitoring. The INSPECTA Assurance Management Framework enables semi-automated support for assurance cases that manage safety, security, and functional claims about the system along with evidence of claim satisfaction.

The framework generates a variety of dynamically navigable reports representing knowledge of the system including claim status, test coverage, and traceability from model artifacts (including formal specs) through source code all the way to micro-kernel partitioning and communication infrastructure. Life-cycle attestation infrastructure from the University of Kansas uses cryptographic techniques to guarantee that assurance is up-to-date and that development and assurance artifacts have not been tampered with “behind the scenes”.

We describe the application of the framework to the Collins PROVERS open platform mock UAV system developed by DornerWorks. We illustrate how the modeling, contracts are used to support development of multiple firewall components in Rust, with seamless switching between automated property-based testing and Verus SMT-based verification to assure that the firewall components deployed on seL4 meet their model-level contracts. The Collins Aerospace Launched Effects UAV product-line (specifically the RapidEdge mission computer) is the product-level demonstrator for the INSPECTA project. HAMR and the broader INSPECTA tool chain are available under an open-source license, and the project website includes an example repository and collection of videos, tutorials, and classroom lecture materials(also suited for workforce training).