This technique provides an alternative to BPF for packet filtering at gigabit speeds. In this application, an order of magnitude run-time performance increase is very helpful because receiving the packets is already pushing the limits of what common x86 hardware can do. With some straightforward modifications, the commonly used packet capture library libpcap can be made to generate native machine code rather than BPF code, which can then be passed to the kernel for verification and installation. Such an arrangement would allow many common packet-capture programs, such as tcpdump, ethereal, and the ISC DHCP server, to take advantage of this performance increase simply by linking with the new library. Alternately, libpcap could be completely bypassed and a compiler could be used to generate an optimized binary for installation in the kernel, but this would require applications to change.
The single greatest danger of this approach is that the prover is a trusted component and has not been developed using high-assurance software techniques. If the prover were to be flawed in such a way that an unsafe program could be loaded as an extension, it could circumvent the security of the entire system. The prover's implementation needs to be subjected to serious scrutiny before it could be deployed for use by unprivileged users. A reasonable strategy would be to initially constrain it to use by privileged users only.
Another problem is that the linear representation of values is done as the sum of several machine integers, each of which has as much precision as the sum will have in the running program. It may be possible to use this difference in precision to subvert the prover. A work-around that is currently employed is to constrain the range of values allowed in each field of a known value, so that sign reversals are not possible as long as the base values are not close to the beginning or the end of the number space.
For the immediately intended application, static verification appears to be viable and the prover implemented for this project appears to be a successful proof of concept. This technique is probably also applicable to other problems, but care must be taken to address the generality and trust issues of building a practical prover.
There has been a good bit of similar work to this, both on verification of synthetic machine codes that make properties easier to reason about at a higher run-time cost and on extensive verification of real machine codes at a high proof cost. The expected contribution of this work is to show that a very limited prover can operate on native machine code (to get the best performance for the code that's executing) and can efficiently reason about a very small but still interesting set of programs.