Safe to the Last Instruction

Chris Hawblitzel and I just submitted the camera-ready version of our PLDI 2010 paper Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System.

The main idea is as follows. Much of traditional operating systems verification is quite difficult because the projects verify properties of low-level code. Microsoft's Singularity project aims to make the verification process easier by verifying an operating system written in a higher-level, type-safe language (C#) that provides memory safety properties for free. The problem here is that OS's necessarily have low-level code--for instance, context-switching code involves moving the stack pointer. We propose a verification approach that involves designing the OS around a small low-level "Nucleus" that we verify using Hoare logic, verifying the interface between the Nucleus and higher-level, type-safe code, and writing the rest of the OS using the higher-level language. We describe Verve, a prototype OS verified automatically end-to-end for type safety.

Abstract below; paper here:

Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code.We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our techniques and tools mechanically verify the safety of every assembly language instruction in the operating system, run-time system, drivers, and applications (in fact, every part of the system software except the boot loader). Verve consists of a “Nucleus” that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and applications that run on top of the kernel. The Nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access. The kernel, written in C# and compiled to TAL, builds higher-level services, such as preemptive threads, on top of the Nucleus. A TAL checker verifies the safety of the kernel and applications. A Hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the Nucleus. Verve is, to the best of our knowledge, the first operating system mechanically verified to guarantee both type and memory safety. More generally, Verve’s approach demonstrates a practical way to mix high-level typed code with low-level untyped code in a verifiably safe manner.