BPF and Formal Verification (2015)

The below BPF program, taken from the OpenBSD man page and translated into a more readable representation, returns all Ethernet packets between IP addresses 128.3.112.15 and 128.3.112.35. We introduce a new type representing the two possible final states of a BPF program: a return value or an error. Coq programs generally use numbers of type , an inductive type:

Fixed sized binary data – mostly 32-bit ints in our case – are not well represented with .

Source: www.sccs.swarthmore.edu