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
Related Publications
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 | ||
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 | ||
|
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 | |
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 | ||
Johannes Åman Pohjola, Henrik Rostedt and Magnus Myreen Characteristic formulae for liveness properties of non-terminating CakeML programs International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019 |
People
Past
|