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