Foundational and Automated Verification of
Bitfield-Manipulating Programs

Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg.

Preprint Appendix Source (repo) Source (zip) Artifact

Low-level systems code often needs to interact with data, such as page table entries or network packet headers, in which multiple pieces of information are packaged together as bitfield components of a single machine integer and accessed via bitfield manipulations (eg shifts and masking). Most existing approaches to verifying such code employ SMT solvers, instantiated with theories for bit vector reasoning: these provide a powerful hammer, but also significantly increase the trusted computing base of the verification toolchain.

In this work, we propose an alternative approach to the verification of bitfield-manipulating systems code, which we call BFF. Building on the RefinedC framework, BFF is not only highly automated (as SMT-based approaches are) but also foundational—i.e., it produces a machine-checked proof of program correctness against a formal semantics for C programs, fully mechanized in Coq. Unlike SMT-based approaches, we do not try to solve the general problem of arbitrary bit vector reasoning, but rather observe that real systems code typically accesses bitfields using simple, well-understood programming patterns: the layout of a bit vector is known up front, and its bitfields are accessed in predictable ways through a handful of bitwise operations involving bit masks. Correspondingly, we center our approach around the concept of a structured bit vector—i.e., a bit vector with a known bitfield layout—which we use to drive simple and predictable automation. We validate the BFF approach by verifying a range of bitfield-manipulating C functions drawn from real systems code, including page table manipulation code from the Linux kernel and the pKVM hypervisor.

Structural Specification

Instead of low-level bit specification (as in SMT-based approaches), users express high-level specification on records/structs in BFF.

Clean Core Theory

Based on how bitwise operations are used to reasonably manipulate bitfields, we propose a simpler core theory than the bit vector theory.

Linux Case Studies

BFF successfully verified bitfield-manipulating functions extracted from four Linux code bases. A fair amount of user annotations were needed.

This work was realized using RefinedC.