Funding
Our Partners
Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA)
We are working on the DARPA-sponsored Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) project, building on our successful collaborations in the SMACCM and CASE 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 PROVERS is to develop formal methods tools fully integrated into pipelined software development and maintenance processes to enable higher levels of assurance that software systems are free of defects or security vulnerabilities. These formal methods tools will be designed for software engineers in the defense and aerospace industries who are not formal methods experts. Tooling will be integrated into currently used software development pipelines, enabling a continuous flow of capabilities over time while maintaining high assurance.
The INSPECTA Team, led by Collins Aerospace, addresses the entire software development stack, from requirements and system models to component source code, through build and deployment on the seL4, all linked by formal verification at each level.
Our contribution to INSPECTA is the further development of LionsOS, especially support for hard real-time applications in a strictly time- and space-partitioned system and enforcement of integrity and confidentiality, as well as making the verification of OS components a more repeatable process. The Pancake language is an important part of this.
Timeline
Phase 1 (March'24–March'25): Develop highly modular LionsOS and demonstrate performance and formally verify key properties of critical OS components and their interactions.
Phase 2 (March'25–Sep'26): Assist project partners with deployment of LionsOS and demonstrate swappable policies and inexpensive re-verification of changed policy implementations
In Phase 3 (Sep'26–Sep'27): Enhance LionsOS based on feedback, complete verification of critical components and interactions, ensure ease of use of LionsOS and verification artefacts for embedded-systems engineers with no background in formal methods.
Contact
Related Publications
|
 |
Gernot Heiser, Ivan Velickovic, Peter Chubb, Alwin Joshy, Anuraag Ganesh, Bill Nguyen, Cheng Li, Courtney Darville, Guangtao Zhu, James Archer, Jingyao Zhou, Krishnan Winter, Lucy Parker, Szymon Duchniewicz and Tianyi Bai Fast, secure, adaptable: LionsOS design, implementation and performance arXiv preprint, January, 2025 |
|
|
|
Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser Verifying device drivers with Pancake arXiv preprint, January, 2025 |