Semantics, Verification, and Efficient Implementations for Tristate Numbers

Extended Berkeley Packet Filter(BPF)is an in-kernel, register-based virtual machine in the Linux operating system that allows non-superusers to execute code at specific points within the Linux kernel. To ensure that such user code is safe within the kernel, BPF relies on an in-kernel static analyzer that proves properties such as bounded memory access and the absence of illegal operations. This static analyzer uses an abstract domain, which it calls tnums (tristate numbers), to over-approximate the set of values that a variable may store. This abstract domain is implemented efficiently with bitwise and arithmetic operations. This paper formalizes the semantics and various properties of tnums and provides the first proofs of soundness and precision of arithmetic and logical operations with tnums. We describe a novel sound algorithm for multiplying two tnums that is more precise and efficient (runs 55% faster on average) than the Linux kernel's tnum multiplication.