一句话：提出 BFF，在 Coq 中机械化地对位域操作的 C 系统代码实现既自动化又有形式语义基础的正确性验证。
底层系统代码常需通过移位、掩码等位域操作访问页表项、网络包头等打包在单个机器整数中的数据。现有验证方法多依赖配备位向量理论的 SMT 求解器，虽自动化程度高，却显著扩大了验证工具链的可信基。本文提出 BFF，一种基于 RefinedC 框架的替代方案：它既保持 SMT 方法那样的高度自动化，又是基础化的——其正确性证明针对 C 程序的形式语义，并在 Coq 中完全机械化。BFF 不试图解决任意的位向量推理问题，而是观察到真实系统代码通常以简单、可预期的模式访问位域：位向量的布局事先已知，位域通过少量含位掩码的位运算按可预测方式访问。据此，作者以“结构化位向量”（即具有已知位域布局的位向量）为核心概念来驱动简单而可预测的自动化。作者通过验证来自真实系统代码的一系列位域操作 C 函数（包括 Linux 内核与 pKVM hypervisor 的页表操作代码）来评估 BFF。
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 (e.g., 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.
@article{paperbot1474,
title = {BFF: foundational and automated verification of bitfield-manipulating programs},
author = {Fengmin Zhu and Michael Sammler and Rodolphe Lepigre and Derek Dreyer and Deepak Garg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563345}
}