The seL4 microkernel is currently the only kernel that has been fully formally verified. In general, the increased interest in ensuring the security of a kernel’s code results from its important role in the entire operating system. One of the basic features of an operating system is that it abstracts the handling of devices. This abstraction is represented by device drivers – the software that manages the hardware. A proper verification of the software component could ensure that the device would work properly unless there is a hardware failure. In this paper, we choose to model the behavior of a device driver and build the proof that the code implementation matches the expected behavior. The proof was written in Isabelle/HOL, the code translation from C to Isabelle was done automatically by the use of the C-to-Isabelle Parser and AutoCorres tools. We choose Isabelle theorem prover because its efficiency was already shown through the verification of seL4 microkernel.
Some light reading that would’ve been for the weekend had I not gotten sick and unable to work on OSNews much.
Interesting read, and I hope you’re feeling better 🙂
What is the goal of this paper? Is it trying to replace OpenSD’s kernel with SEL4?
From the paper: In this paper we investigate the process of adapting and applying the seL4 verification process for verify parts of another operating system and present a concrete case for the octrng(4) driver for the Octeon/MIPS64 platform provided by the OpenBSD operating system.