Increasing network speeds and interest in applying this approach to other problems have made emulation overhead an issue. Also an issue is that the BPF program must be written in a special assembly language; no high-level language compilers currently exist that target the BPF machine. Native machine code has neither problem; it executes at full machine speed and can be targeted by whatever compilers are available. Many systems have a facility for extending the running kernel using native instructions (loadable kernel modules). Typically, these extensions are installed by a privileged process, are not subject to any sort of verification at installation time, and have the same run-time privileges as the rest of the kernel (in particular, there is usually almost no access checking). Such facilities are inappropriate for use by unprivileged processes, and represent serious risks even when restricted to privileged processes. In particular, the extension code can put the entire system in a bad state, either due to deliberate actions or unintended flaws.
A possible solution to the problem is to statically analyze program code to determine whether it obeys certain restrictions and safety policies. BPF already does this in a very limited way. The bpf_validate() function is called before code is installed into the running system, and checks three safety properties [1]:
A similar approach is used by the Java Virtual Machine (JVM), which uses a bytecode verifier to check for memory and type safety as code is loaded into the system[2]. Again, some safety is provided by the emulated machine, which provides no truly unsafe instructions and guarantees that the calling convention will be obeyed. However, the JVM approach alleviates the need for run-time bounds checking of memory accesses by moving that overhead to a load-time static analysis. While this improves run-time performance, there is still significant overhead due to the emulation of the JVM's instruction set.
In theory, the instructions present in the BPF virtual machine's instruction set and the JVM's instruction set are functionally equivalent to instructions (or short sequences of instructions) in native machine instructions. If it is possible to reason about the BPF or JVM instructions statically, it may be possible to do the same with a constrained version of a real machine's instruction set. This is an active area of research typically for use with micro-kernels, where fast and safe kernel extensions are more commonly needed. A particularly interesting research solution is Proof Carrying Code (PCC) [3], in which native code is statically analyzed, an attempt is made to generate a proof that the code obeys certain safety properties, and the proof and code are later verified by the kernel before accepting the code as an extension.
If a proof can be found and verified, then the code is known to have the safety properties and run-time checks are not needed [4]. If a proof cannot be found, this does not necessarily mean that the code is unsafe - as a nontrivial program property, this is an undecidable problem[5], but it is always a safe default action to consider code to be unsafe. If a programmer has the prover in hand and knows what the safety policy is, development can be done iteratively where the programmer adjusts the code in equivalent ways until it passes the prover; while the prover might not be able to reason about arbitrary programs, it is usually possible for a programmer to find a functionally similar program that it can reason about.
The main problem with the PCC approach is that the prover is too heavyweight, yet is still very limited in its ability to actually prove properties of programs. In one PCC implementation, the prover is a general-purpose theorem prover, which is very large and slow, but can attempt to prove rather arbitrary properties of programs. In practice, this approach becomes far less likely to successfully generate a proof as program complexity increases. In another, the prover is built into a special type-safe C compiler; most of the overhead of the prover is shared with the compiler and proofs are always generated for valid programs in the language (the property proved is type safety and the language is a type-safe language, so one is always possible), but now a specific compiler must be used. Because the proof generation step is so heavyweight, the PCC approach separates proof generation and proof verification and makes only the latter a trusted component.
A promising direction for a solution to this problem is to start with the PCC approach and to make the prover sufficiently fast and lightweight that the proof generation can be a trusted component (eliminating the need for an intermediate representation of the proof and a proof verifier). This is done by greatly constraining what programs are allowed to do; if programs are simple enough, reasoning about them becomes simple also. In particular, extensions are currently required to be stateless and return a simple integer result. This is still interesting for many problems such as packet filtering, and allows the extension to be terminated by the system without having to worry about cleanup. Conditions like division by zero are already checked at run-time ``for free'' by the hardware and global state can be recovered from rather painlessly, so there is little value in a relatively expensive static analysis to decide whether the condition is possible. In contrast, safety of memory accesses is expensive to do with the hardware (due to the time required to switch to more restrictive page tables), and backing out a write to a random memory location is painful if not effectively impossible, so statically checking for this kind of safety is valuable.