Multicore seL4 Verification
-
Aim:
This project aims to develop and apply frameworks for reasoning
about concurrency in OS-code, with a particular focus on verifying the
multicore version of seL4.
-
Context:
Formal verification is important in safety critical software. To
make sure that a verified system runs correctly one also needs to
provide formal guarantees about the correctness of the underlying
operating system (OS) that the program runs on. Data61's
Trustworthy Systems group is famous for its formal verification of
the seL4 microkernel in the Isabelle-HOL theorem prover.
Most recent successfully verified operating systems, including
seL4, run on uniprocessor platforms and with interrupts largely
disabled. However, there is an increasing demand for verified
real-time operating systems (RTOS) which require support for
concurrency.
-
Approach:
The project extends existing concurrency methods for verifying
shared-variable programs, such as the foundational Owicki-Gries and
Rely-Guarantee approaches. To reach our goal of improving the ease
at which concurrent programs can be verified we have had a
particular focus on increasing the automation and scalability of
these methods, especially within the Isabelle-HOL theorem
prover. We are also aiming to create a sound, modular and useful
framework for proving refinement of concurrent programs.
-
Case Study:
As part of this project we are modelling and verifying two example
operating systems. These are the small, embedded
eChronos
RTOS, and a multicore version of seL4. Both have been embedded
in high-assurance autonomous flying vehicles that have been
developed in collaboration with industry and university partners
as part of the DARPA-funded SMACCM
project.
Activities
This project is presently on hold. We are looking for funding to complete the verification of multicore seL4.
Past activities:
- Functional Correctness of the
eChronos RTOS: We have developed an abstract model of the
eChronos RTOS that accurately represents the interleaving of the
real implementation. Using this model we have then verified the
main correctness property of the eChronos RTOS with a formal
machine-checked proof within Isabelle/HOL.
- Refinement to the
Implementation: To complete the verification of the
eChronos RTOS we wish to provide a refinement between the above
abstract model and the actual implementation. This requires
developing a scalable framework that supports both atomicity and data
refinement.
- Verification of Multicore
seL4: The verification of multicore seL4 is a new project,
targeting the "big lock" version of seL4 [1] and aiming at
providing a formal model of interleaved execution. This will
also include investigation of the best logic and concurrency
model to use.
[1] APSys For a microkernel, a big lock is fine, 2015
Availability
The proofs for the eChronos RTOS are open source and are available
under the BSD 2-clause license
on github.
People
Publications
2017
|
 |
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joey Tuong
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138–150, Paris, France, January, 2017 |
2016
|
 |
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah
Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016 |
2015

|
 |
June Andronick, Corey Lewis and Carroll Morgan
Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system
Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015 |

|
 |
Sean Peters, Adrian Danis, Kevin Elphinstone and Gernot Heiser
For a microkernel, a big lock is fine
Asia-Pacific Workshop on Systems (APSys), Tokyo, JP, July, 2015 |