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.
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.
||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
Proceedings of the 10th International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019