In order to gain more experience with and to compare it with other approaches to code safety, we have performed a series of experiments with safe network packet filters. We describe in this section the particulars of the approach to network packet filters. Then in pf-perf, we compare it with other approaches including interpreted packet filters (as exemplified by the BSD Packet Filter), code editing (through Software Fault Isolation), and using a safe programming language (the approach taken in the SPIN kernel).
A packet filter is an application-provided subroutine that scans each incoming network packet and decides whether the user application is interested in receiving it or not. Packet filters are supported by most of today's workstation operating systems. Since their first introduction in [15], packet filters have been used successfully in network monitoring and diagnosis.
In the approach the packet filter is a binary whose native code component is invoked by the kernel on each incoming network packet. Kernel safety is ensured by validating the safety proof.
Following the procedure described in pcc we first establish a safety policy. To allow for a fair comparison we follow the BSD Packet Filter model of safety. The packet filter code can examine the packet at will and can also write to a statically allocated scratch memory. Informally, the safety policy requires that: (1) memory reads are restricted to the packet and the scratch memory; (2) memory writes are limited to the scratch memory; (3) all branches are forward; and (4) reserved and callee-saves registers are not modified. These rules establish memory safety and termination assuming that the kernel calls the packet filter with valid packet and scratch memory addresses.
We write the packet filter code assuming that the return value must be in
, the aligned address and the length of the packet filter are given in
and 
respectively, and the address of a 16-byte aligned
scratch memory is given in 
. Moreover the packet's length is positive
and at least 64-bytes (the minimum length of an Ethernet packet). Formally this
is expressed as the precondition:
The first few conjuncts of the precondition restrict the values of input registers to valid machine word values. The last term of the precondition rules out the possibility of memory aliasing between packets and the scratch memory. This is useful when reasoning about filters that write to the scratch memory.
The postcondition in our packet filter experiment is the predicate 
,
meaning that no additional conditions are placed on the final state.
We have implemented four typical packet filters in assembly language and certified their safety with respect to the packet filter safety policy. Filter 1 accepts all IP packets. This is done by comparing a 16-bit word in the packet to a given value. Filter 2 accepts IP packets originating from a given network. This involves checking a 24-bit value in addition to the work done by Filter 1. Filter 3 accepts IP or ARP packets exchanged between two given networks. This includes all the work done by Filter 2 with the addition of checking the destination network address. Extra complexity is required because of different header layout of IP and ARP packets. Filter 4 accepts all TCP packets with a given destination port. This filter has to check that the Ethernet packet is an IP packet, then that it is a TCP packet, and lastly that the destination port matches a given value. The offset of the TCP destination port is computed based on a byte in the IP header (the length of the IP header).
The effort involved in hand-coding packet filters in assembly language is repaid in increased performance, because packet filters are usually small and very frequently executed. Hand-coding provides the opportunity to perform optimizations that are difficult to obtain from an optimizing compiler. The important point is that these optimizations are not an impediment to generation and validation of safety proofs. Here are a few optimizations that we incorporated in our packet filters:
, where 
denotes the byte at offset 14.
If loading 64 bits at a time on a little-endian machine, the formula becomes
. With further
simplification we reduce this to 
, which
is exactly how we coded Filter 4.
After we write a packet filter, our prototype assembler produces its safety
predicate using the verification-condition method presented in pcc.
The safety predicate is then proved using a theorem prover. We currently use
our own theorem prover, which is admittedly a toy. When it gets stuck, it
requires intervention from the programmer, mainly to learn new axioms about
arithmetic (for example, to know that 
). The
process is easy, and because user-provided axioms are remembered for future
sessions, by now our system works automatically for most practical packet
filters. With state-of-the-art theorem proving technology we expect to be able
to prove completely automatically most arithmetic facts involved in certifying
packet filters.
With our primitive theorem-prover we can generate safety proofs for packet filters in about 5 to 10 seconds, in the cases when no user-intervention is required.