Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA)

Formal methods have been successfully deployed at scale in production environments at large internet companies, but barriers remain to their adoption by defense companies developing national security systems. The goal of the INSPECTA project (part of DARPA PROVERS) is to improve the security of defense and aerospace systems by dramatically improving the usability, flexibility, and accessibility of formal methods based development and verification tools. We will leverage memory-safe programming languages (Rust), a provably secure microkernel (seL4), and new formal methods tools and make them accessible to the defense industry workforce. These open source technologies will be integrated into an aerospace CertDevOps workflow automation processes and applied to the development of mission critical systems to demonstrate their usability, practicality, and effectiveness. We will demonstrate the tools and workflow by addressing emerging security requirements for the Air Launched Effects (ALE) mission computing platform. This will include re-architecting the mission software as a collection of virtual machines running legacy code and selected high-criticality components, producing an architecture model for the system, porting selected software to Rust, building software to run on seL4, and verifying critical safety and security properties.