{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T15:33:33Z","timestamp":1783611213761,"version":"3.55.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/3563345","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1613-1638","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["BFF: foundational and automated verification of bitfield-manipulating programs"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4219-0837","authenticated-orcid":false,"given":"Fengmin","family":"Zhu","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2849-5338","authenticated-orcid":false,"given":"Rodolphe","family":"Lepigre","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0888-3093","authenticated-orcid":false,"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010 . The SMT-LIB standard: Version 2.0 . In Proceedings of the 8th international workshop on satisfiability modulo theories ( Edinburgh, England). 13, 14. Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England). 13, 14."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_15"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the LPAR 2008 Workshops","author":"de Moura Leonardo Mendon\u00e7a","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner . 2008. Proofs and Refutations , and Z3. In Proceedings of the LPAR 2008 Workshops , Knowledge Exchange : Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008 , Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate A. Schmidt, and Stephan Schulz (Eds.) (CEUR Workshop Proceedings , Vol. 418). CEUR-WS.org. http:\/\/ceur-ws.org\/Vol-418\/paper 10 .pdf Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Proofs and Refutations, and Z3. In Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008, Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate A. Schmidt, and Stephan Schulz (Eds.) (CEUR Workshop Proceedings, Vol. 418). CEUR-WS.org. http:\/\/ceur-ws.org\/Vol-418\/paper10.pdf"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_11_1","unstructured":"Will Deacon. 2020. Virtualization for the Masses: Exposing KVM on Android. https:\/\/www.youtube.com\/watch?v=wY-u6n75iXc KVM Forum Talk \t\t\t\t  Will Deacon. 2020. Virtualization for the Masses: Exposing KVM on Android. https:\/\/www.youtube.com\/watch?v=wY-u6n75iXc KVM Forum Talk"},{"key":"e_1_2_1_12_1","unstructured":"Claire Dross Cl\u00e9ment Fumex Jens Gerlach and Claude March\u00e9. 2015. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Ph. D. Dissertation. Inria Saclay. \t\t\t\t  Claire Dross Cl\u00e9ment Fumex Jens Gerlach and Claude March\u00e9. 2015. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Ph. D. Dissertation. Inria Saclay."},{"key":"e_1_2_1_13_1","volume-title":"The yices smt solver. Tool paper at http:\/\/yices. csl. sri. com\/tool-paper. pdf, 2, 2","author":"Dutertre Bruno","year":"2006","unstructured":"Bruno Dutertre and Leonardo De Moura . 2006. The yices smt solver. Tool paper at http:\/\/yices. csl. sri. com\/tool-paper. pdf, 2, 2 ( 2006 ), 1\u20132. Bruno Dutertre and Leonardo De Moura. 2006. The yices smt solver. Tool paper at http:\/\/yices. csl. sri. com\/tool-paper. pdf, 2, 2 (2006), 1\u20132."},{"key":"e_1_2_1_14_1","unstructured":"Jake Edge. 2020. KVM for Android. https:\/\/lwn.net\/Articles\/836693\/ \t\t\t\t  Jake Edge. 2020. KVM for Android. https:\/\/lwn.net\/Articles\/836693\/"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181791"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498681"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_23"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485529"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_7"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.70.7"},{"key":"e_1_2_1_29_1","unstructured":"The Coqutil Team. 2022. coqutil. https:\/\/github.com\/mit-plv\/coqutil \t\t\t\t  The Coqutil Team. 2022. coqutil. https:\/\/github.com\/mit-plv\/coqutil"},{"key":"e_1_2_1_30_1","unstructured":"The Tokei Team. 2022. Tokei. https:\/\/github.com\/XAMPPRocky\/tokei \t\t\t\t  The Tokei Team. 2022. Tokei. https:\/\/github.com\/XAMPPRocky\/tokei"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7079022"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563345","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563345","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:11Z","timestamp":1750178291000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563345"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":33,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563345"],"URL":"https:\/\/doi.org\/10.1145\/3563345","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}