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, Adventium, the University of New South Wales (Sydney), the University of Kansas, and Kansas State University have teamed to provide a comprehensive solution to the design resiliency and tool integration objectives of the CASE program. We have developed a model-based systems engineering environment called BriefCASE that allows engineers to address a range of properties and manage system complexity through compositional analysis, integrating formal methods at all levels of the design process. Our tools are based on the Architecture Analysis and Design Language (AADL) and extend the Open Source AADL Tool Environment (OSATE).
The main innovations of the BriefCASE tools and methodology are:
- We provide automated architectural design patterns to address cyber-resiliency requirements, including synthesis of highassurance components from formal specifications.
- Our MBSE environment can target different operating systems including the seL4 microkernel, making its formal security guarantees easily accessible to developers. This ensures that the implementation produced is faithful to the modeled system.
- Our approach is based upon co-evolution of system design and assurance artifacts, so that design changes automatically update the associated certification evidence. An assurance case is a structured argument, supported by evidence, intended to justify that a system is acceptably assured relative to a concern (such as safety or security) in the intended operating environment. An assurance case is embedded in the architecture model to capture and document the design decisions along with associated rationale.
- Formal methods are integrated throughout the workflow, including requirements capture, component synthesis, verification, code generation, and the seL4 microkernel.
Tools developed on the CASE project are open-source and are available on GitHub.
- AADL modeling and analysis tools
- Installation script for Windows
- Installation script for Linux
- Vagrant script for configuring a virtual machine containing the both the modeling/analysis tools and the build environment for targeting seL4
- User Guide for the BriefCASE tools
A tutorial on the BriefCASE tools and workflow is available here. Example AADL models and code for a simple UAV system that can be run on the QEMU emulator are included with the tutorial.
This video provides a demonstration of the BriefCASE tool environment that we have developed. It shows how to use the tools to address multiple cyber-resiliency requirements for a UAV mission computing system. AADL models for the experimental UAV application in the video are available here.
In part two, we run the hardened UAV mission computing system built in the first video and test it against several cyber attacks to show the effectiveness of the approach.