Safety Checking of Kernel Extensions

There are many places in operating systems today where extending the running kernel with small and fast extensions is an interesting thing to do. For example, the Berkeley Packet Filter (BPF) allows code for a virtual machine to be uploaded into a running kernel and executed at packet reception, allowing fairly arbitrary filtering of packets before they cross the expensive kernel to user interface. Whatever mechanism is used needs to provide some reasonable guarantees about the safety of the resulting code, which makes this problem complex.

This paper describes a simple x86 bytecode verifier that is intended to be used to verify that a small program that is to be loaded obeys a reasonable safety policy. For program constructs that it is able to reason about, it can verify that code does not execute privileged instructions, only accesses known memory locations, and terminates. It cannot reason about arbitrary programs, but can reason about simple programs and developers that know the prover's limitations can write their code to be recognizable by the verifier.

The contribution of this work is to show that a very limited prover can operate on native machine code and can efficiently reason about a small but still interesting set of programs.