Cyber Assured Systems Engineering at Scale
Abstract: Formal methods tools that provide mathematical proof of system properties have improved dramatically in their power and capabilities. As part of DARPA's Cyber Assured Systems Engineering (CASE) program, our team has developed a model-based systems engineering environment called BriefCASE that integrates formal methods at all levels of system design. Our methodology and tools enable systems engineers to address cybersecurity concerns early in the development of complex high-assurance systems. We track the satisfaction of cyber requirements throughout the design process by creating an assurance case that is integrated with an AADL model of the system architecture. In this talk we will describe the application of the BriefCASE tools and workflow to the mission computing system in a military helicopter. The demonstration system integrated wireless devices for pilots and soldiers with the existing avionics networks. BriefCASE tools were used to implement a new high-assurance gateway based on the seL4 secure microkernel, including new components for monitoring messages to and from the wireless devices. Remote attestation was also added to ensure that any devices that attempt to join the wireless network are running trustworthy software.
Darren Cofer is a Fellow in the Trusted Systems group at Collins Aerospace. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin.
His principal 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.
He has served as principal investigator on government-sponsored research programs with NASA, NSA, AFRL, and DARPA, developing and using formal methods for verification of safety and security properties. He is currently the principal investigator for Collins teams working on DARPA's Cyber Assured Systems Engineering (CASE) and Assured Autonomy programs.
Dr. Cofer 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 a member of SAE committee G-34 on Artificial Intelligence in Aviation, the Aerospace Control and Guidance Systems Committee (ACGSC), and a senior member of the IEEE.