Formal Model of a Multi Core Kernel-based System
Abstract
Professor Andronick and her research team sought to address the grand challenge of providing strong, mathematical guarantees for software that runs on multi-core platforms, thus meeting the increasing demand for more computing power even for critical real-world systems. The research team targeted the operating system kernel, which is the core and foundation of any software system. Their approach was to solve a large part of the scalability problem in foundational concurrency reasoning by exploiting automation in modern machine-checked theorem proving. In addition, they sought to soundly reduce reasoning about interleaving with a faithful representation of hardware and software mechanisms such as scheduling, priorities, interrupts, and locks; and to continue to exploit kernel design principles for reducing verification effort. The project has achieved all planned goals, including its stretch goals. They have defined a formal model of execution for a multi-core kernel, as well as a low-level formal language to push the guarantees as close as possible to the real implementation. This framework has been applied to a multi-core version of seL4 [Klein et al., 2009], the landmark verified microkernel, whose verification so far is restricted to uniprocessor systems. They have defined a formal high-level model of multi-core seL4 and proved the correctness of its most critical operation. They have also developed an initial refinement framework that will allow us to carry the proofs done at the high specification level down to the low implementation level. The project paves the way for proving full functional correctness of multi-core, high performance microkernels.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 10, 2018
- Accession Number
- AD1062068
Entities
People
- Carroll Morgan
- Gerwin Klein
- June Andronick
Organizations
- National ICT Australia