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.  

Darren Cofer is a Principal Fellow at Collins Aerospace. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin.  His area of expertise is developing and applying advanced analysis methods and tools for verification and certification of high-integrity systems. His background includes work with formal methods for system and software analysis, the design of real-time embedded systems for safety-critical applications, and the development of nuclear propulsion systems in the U.S. Navy.  

Dr. Cofer has served as principal investigator on many government-sponsored research programs, developing and using formal methods for verification of safety and security properties.  He served on RTCA committee SC-205 developing new certification guidance for airborne software (DO-178C) and was one of the developers of the Formal Methods Supplement (DO-333). He is currently a member of SAE committee G-34 developing certification guidance for the use of machine learning technologies onboard aircraft.