Software Engineering Institute

As part of DARPA's Cyber Assured Systems Engineering (CASE) program, we developed an AADL-based engineering environment to help build cyber-resilient systems. Our tools verify cyber requirements against a formal model of the system architecture, using both integrated model checking and information flow analysis. We track the satisfaction of cyber requirements throughout the design process by creating an assurance case that is integrated with the AADL system architecture model. Developers can select from our library of design patterns, including space and time partitioning, and verified cyber-resilient components such as verified filters, to address cyber requirements. Our automated model transformation tools help the developers apply these design patterns and insert these components into their designs. Our HAMR code generation framework automatically generates cyber-resilient implementations from the verified design model using high-assurance components and property-preserving transformations. Our AADL-to-code generators can target Linux or the formally verified seL4 microkernel. The tools have been demonstrated on an enhancement to a mission computing system in a military helicopter to demonstrate effectiveness of the approach on a real avionics system.

Darren Cofer is a Fellow 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 for Artificial Intelligence in Aviation, the Aerospace Control and Guidance Systems Committee (ACGSC), and a senior member of the IEEE.

Todd Carpenter is Chief Engineer and co-owner of Adventium Labs. His areas of expertise include engineering real-time, fault-tolerant, and secure systems in military and commercial avionics, medical, and petrochemical domains. His experience spans detailed hardware and software design, architecture development, systems design and specification, as well as tools and processes for enhancing design flows.  Current activities include developing architectures for safe and secure medical devices, avionics, and mission systems. He is also developing model-based systems engineering techniques to help others create such systems.