The goal of DARPA's Cyber Assured Systems Engineering (CASE) program is to develop the necessary design, analysis and verification tools to allow system engineers to design-in cyber resiliency and manage tradeoffs as they do the other nonfunctional properties when designing complex embedded computing systems. Cyber-resiliency means that the system is tolerant to cyberattacks in the same way that safety-critical systems are tolerant to random faults - they recover and continue to execute their mission function.
Collins Aerospace, Data61, and The University of Kansas have teamed to provide a comprehensive solution to the Design Resiliency objectives for Technical Area 2 of the CASE program. We are pursuing four technology development thrusts:
- Verification of Cyber Requirements via formal architecture, design, and implementation modeling/analysis, and automated information flow analysis
- Cyber-Resilient Design Patterns via tool-assisted model transformations utilizing verified cyber-resilient components
- Runtime Assurance for Requirements via verified cyber-resilient components and remote attestation
- Architectural Design Model Validation via model-based test generation
In CASE Technical Area 5, Collins Aerospace and our teammates, Data61, Adventium, and Kansas State University, will develop an integrated formal methods-based systems engineering tool suite and work with military platform providers applying these tools to construct cyber-resilient systems. This effort will leverage our expertise in industrial application of formal methods, development of complex military vehicles, formally verified operating system components, and formal design languages and synthesis.
Models and code for the project are available on github.