Trustworthy Systems

Our Partners DARPA
Collins Aerospace
Adventium Labs
Kansas State University
The University of Kansas

Cyber Assured Systems Engineering (CASE)

We are working on the DARPA-sponsored Cyber Assured Systems Engineering (CASE) project, building on our successful work in the SMACCM and HACMS projects. DARPA, the Defense Advanced Research Projects Agency (DARPA), is a US defense agency that oversees the development of emerging technologies for military use.

The goal of the CASE project is to develop re-usable design, analysis and verification tools that allow system engineers to design-in cyber resiliency when building 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.

A novel outcome of this project will be to formally establish cyber resiliency as an explicit system property. System requirements for specific functional behaviours (e.g. to fly in a certain direction) and non-functional properties (e.g. system performance) are usually captured as “shall” statements. This approach has proven to be ineffective in engineering cyber resilient systems because cyber requirements are often statements on what the system should not do, i.e., “shall not” statements.

This project is developing ways to design and verify an embedded system when requirements are not testable (i.e., when they are expressed in “shall not” statements). We are also developing tools to automatically adapt software to new non-functional requirements and techniques to scale and provide meaningful feedback from analysis tools that reside low in the development tool chain.

Timeline

Phase 1 consists of initial research and tool development.

Phase 2 consists of technology enhancements and testing of the emerging tools on one or more experimental platform(s).

In Phase 3 the CASE tools will be used to re-engineer a selected representative demonstration of a real system for cyber resiliency.

Contact

Gernot Heiser

Related Publications

 

Abstract PDF Jason Belt, John Hatcliff, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren Cofer, David Hardin, Karl Hoech, Konrad Slind, Ihor Kuz and Kent Mcleod
Model-driven development for the seL4 microkernel using the HAMR framework
Journal of Systems Architecture, Volume 134, pp. 102789, 2023
Abstract PDF Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer and John Shackleton
Cyberassured systems engineering at scale
IEEE Security and Privacy, Volume 20, Number 3, pp. 52–64, March, 2022
Abstract PDF
Presentation Video
Alejandro Gomez-Londono, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus Myreen and Yong Kiam Tan
Do you have space for dessert? A verified space cost semantics for CakeML programs
OOPSLA, pp. 204:1-29, Chicago, IL, November, 2020
Abstract PDF Konrad Slind, David Hardin, Johannes Åman Pohjola and Michael Sproul
Synthesis of verified architectural components for autonomy hosted on a verified microkernel
Hawaii International Conference on System Sciences, pp. 6365-6374, Grand Wilea, Hawaii, January, 2020
Abstract PDF Johannes Åman Pohjola, Henrik Rostedt and Magnus Myreen
Characteristic formulae for liveness properties of non-terminating CakeML programs
Proceedings of the 10th International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019

 

People

Past