Concurrency in Operating Systems
Aim: This project aims to develop and apply frameworks for reasoning about concurrency in OS-code.
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.
- 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  and aiming at
providing a formal model of interleaved execution. This will
also include investigation of the best logic and concurrency
model to use.
 APSys For a microkernel, a big lock is fine, 2015
The proofs for the eChronos RTOS are open source and are available under the BSD 2-clause license on github.
ContactJune Andronick, june.andronick <at> data61.csiro.au
|Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong|
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138-150, Paris, France, January, 2017
|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
||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