Formal verification leverages the power of formal logic to reason about computer programs. Programmers can rely on it to verify that an implementation adheres to an abstract specification of behavior.

This is of great interest when dealing with complex systems, such as an operating system kernel. Previous work, most notably seL4, apply formal verification in this way to reason about the safety of OS kernels.

Formal verification is not without its costs, however. Powerful provers like Coq and Isabel require programmers to write manual proofs, which may take comparable time to write as the source code itself. Hyperkernel takes the opposite approach, where it uses a restricted set of logic in its verification, but in a fully automated, “push-button” manner.

The two major contributions of this paper are:

1. Push-button verification workflow for OS kernels

2. Kernel interface design amenable to SMT solving

Push-button verification workflow

Hyperkernel uses the Z3 theorem solver that operates on the satisfiability modulo theories (SMT) problem. SMT is similar to constraint satisfaction problems, which try to find solutions to a series of constraints over variables.

In the verification for Hyperkernel, the constraint equations are generated based on the abstract specification of the kernel using symbolic execution, and the Z3 solver can try to find counterexamples that violate those constraints using the LLVM intermediate representation of the source code.

There are two specifications, written in Python. The first is the abstract kernel state that defines the data structures used by the kernel as well as the states that the kernel can inhabit. The second specification is the declarative specification, which defines high-level correctness properties about the abstract kernel state.

Not all of the kernel can be verified this way, however. The kernel initialization and glue code that deals with the hardware can’t be verified because Hyperkernel would require an abstract machine model, which it does not currently have.

Finitizing kernel interface

Hyperkernel is based on the xv6 kernel, which is an educational kernel made by MIT that implements Unix V6 on modern systems. Its kernel interface is POSIX-like, which can be difficult to formally verify due to the system calls’ behavior. Specifically, when system calls have run times dependent on system resources, increasing the amount of resources (RAM, hard disk size, etc.) will increase the number of states the variables can take, which produces state explosion in the verification.

The solution is to finitize the kernel interface so system calls have a finite run time regardless of the size of system resources. For example, the dup syscall normally walks through the global list of free file descriptors and finds the first free descriptor. In the worst case it will have to walk through the entire list, and the Z3 solver would have to check every case. Hyperkernel’s finitized dup runs in constant time because it checks the user-provided file descriptor to see if it is free, which runs in constant time regardless of how many file descriptors there are in the global list.

Limitations

While Hyperkernel demonstrates the feasibility of push-button formal verification of an OS kernel, it has several limitations. The first is that xv6 lacks features such as threading, copy-on-write fork, shared pages, and UNIX permissions that mainstream kernels like Linux implement. Furthermore, complex system calls like fork and mmap are difficult to finitize and write abstract specifications for, so a new approach may be necessary to automate the verification for these system calls. Lastly, Hyperkernel verifies LLVM IR, but the correctness guarantees do not extend to the C source code or the final binary. Also, LLVM IR does not model machine details such as the stack so its behavior is not verifiable.

Slides for this presentation can be found here.

Reference

Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), Oct 2017.