|
USENIX Technical Program - Abstract - USENIX Annual
Conference, Freenix Session - June 2000
Safety Checking of Kernel Extensions
Craig Metz, University of Virginia
Abstract
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.
|
Need help? Use our Contacts page.
