{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T08:08:54Z","timestamp":1790928534979,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":101,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3731569.3764796","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"736-751","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Prove It to the Kernel: Precise Extension Analysis via Proof-Guided Abstraction Refinement"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2095-092X","authenticated-orcid":false,"given":"Hao","family":"Sun","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2970-1391","authenticated-orcid":false,"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"bpftop. https:\/\/github.com\/Netflix\/bpftop. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_2_1","unstructured":"bpftune. https:\/\/github.com\/oracle\/bpftune. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_3_1","unstructured":"eBPF Build Config. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/tree\/tools\/testing\/selftests\/bpf\/config?id=0dd3ee311255."},{"key":"e_1_3_2_1_4_1","unstructured":"eBPF Helper Calls. https:\/\/man7.org\/linux\/man-pages\/man7\/bpf-helpers.7.html."},{"key":"e_1_3_2_1_5_1","unstructured":"Imprecision in SysmonForLinux. https:\/\/github.com\/microsoft\/SysmonForLinux\/blob\/407b2808b75afb0e8cf9a5d343c4ff9483c9737c\/ebpfKern\/sysmonProcCreate.c#L55. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_6_1","unstructured":"One Million Instruction Limit in eBPF Programs. https:\/\/github.com\/torvalds\/linux\/blob\/4e82c87058f45e79eeaa4d5bcc3b38dd3dce7209\/include\/linux\/bpf.h#L2009. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_7_1","unstructured":"PREVAIL: eBPF Verifier Based on Abstract Interpretation. https:\/\/github.com\/vbpf\/ebpf-verifier. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_8_1","unstructured":"Rust for linux. https:\/\/rust-for-linux.com\/. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_9_1","unstructured":"The do_check() routine of the eBPF Verifier. https:\/\/github.com\/torvalds\/linux\/blob\/e48e99b6edf41c69c5528aa7ffb2daf3c59ee105\/kernel\/bpf\/verifier.c#L19392. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_10_1","unstructured":"The eBPF Verifier's Imprecision Issue in KubeArmor. https:\/\/github.com\/kubearmor\/KubeArmor\/blob\/31c0977b6c63743b7a8268a2922875f9b9051820\/KubeArmor\/BPF\/system_monitor.c#L612. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_11_1","unstructured":"The jump history entry of the eBPF Verifier. https:\/\/github.com\/torvalds\/linux\/blob\/e48e99b6edf41c69c5528aa7ffb2daf3c59ee105\/kernel\/bpf\/verifier.c#L19392. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_12_1","unstructured":"Verifier Imprecision in Tetragon. https:\/\/github.com\/cilium\/tetragon\/blob\/6fd02f91d15b93e75ae42df7ac131c5ebff77c41\/bpf\/lib\/process.h#L70. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_13_1","unstructured":"Andrea Arcangeli. Seccomp (Secure Computing Mode) Documentation. https:\/\/docs.kernel.org\/userspace-api\/seccomp_filter.html. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_14_1","first-page":"442","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Barbosa Haniel","unstructured":"Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, et al. cvc5: A Versatile and Industrial-Strength SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 415\u2013442. Springer, 2022."},{"key":"e_1_3_2_1_15_1","first-page":"35","volume-title":"International Joint Conference on Automated Reasoning","author":"Barbosa Haniel","unstructured":"Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, et al. Flexible Proof Production in an Industrial-Strength SMT Solver. In International Joint Conference on Automated Reasoning, pages 15\u201335. Springer International Publishing Cham, 2022."},{"key":"e_1_3_2_1_16_1","unstructured":"Clark Barrett Aaron Stump Cesare Tinelli et al. Fixedsizebitvectors. SMT-LIB Theories. Last updated: 2025-02-25."},{"key":"e_1_3_2_1_17_1","first-page":"14","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14, 2010."},{"key":"e_1_3_2_1_18_1","first-page":"527","volume-title":"Proceedings of DAC '98","author":"Barrett Clark W.","year":"1998","unstructured":"Clark W. Barrett, David L. Dill, and Jeremy R. Levitt. A decision procedure for bit-vector arithmetic. In Proceedings of DAC '98, page 522\u2013527, New York, NY, USA, 1998. Association for Computing Machinery."},{"key":"e_1_3_2_1_19_1","first-page":"252","volume-title":"Galen C Hunt. Composing OS Extensions Safely and Efficiently with Bascule. In Proceedings of the 8th ACM European Conference on Computer Systems","author":"Baumann Andrew","year":"2013","unstructured":"Andrew Baumann, Dongyoon Lee, Pedro Fonseca, Lisa Glendenning, Jacob R Lorch, Barry Bond, Reuben Olinsky, and Galen C Hunt. Composing OS Extensions Safely and Efficiently with Bascule. In Proceedings of the 8th ACM European Conference on Computer Systems, pages 239\u2013252, 2013."},{"key":"e_1_3_2_1_20_1","unstructured":"BCC. Tools for BPF-based Linux IO analysis networking monitoring and more. https:\/\/github.com\/iovisor\/bcc. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_21_1","first-page":"283","volume-title":"Proceedings of SOSP '95","author":"Bershad B. N.","year":"1995","unstructured":"B. N. Bershad, S. Savage, P. Pardyak, E. G. Sirer, M. E. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility Safety and Performance in the SPIN Operating System. In Proceedings of SOSP '95, page 267\u2013283, New York, NY, USA, 1995. Association for Computing Machinery."},{"key":"e_1_3_2_1_22_1","first-page":"121","article-title":"Extension Framework for File Systems in User space","volume":"19","author":"Bijlani Ashish","year":"2019","unstructured":"Ashish Bijlani and Umakishore Ramachandran. Extension Framework for File Systems in User space. In USENIX ATC 19, pages 121\u2013134, Renton, WA, July 2019. USENIX Association.","journal-title":"USENIX ATC"},{"key":"e_1_3_2_1_23_1","first-page":"14","article-title":"Attacking Path Explosion in Constraint-Based Test Generation. In Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest","author":"Boonstoppel Peter","year":"2008","unstructured":"Peter Boonstoppel, Cristian Cadar, and Dawson Engler. Rwset: Attacking Path Explosion in Constraint-Based Test Generation. In Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14, pages 351\u2013366. Springer, 2008.","journal-title":"Hungary, March 29-"},{"key":"e_1_3_2_1_24_1","unstructured":"bpftool Developers. bpftool: A command-line tool to inspect and manage bpf objects. https:\/\/github.com\/libbpf\/bpftool. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_25_1","unstructured":"calico. Cloud native networking and network security. https:\/\/github.com\/projectcalico\/calico. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_26_1","unstructured":"Calico project. felix\/bpf-gpl\/tc.c. https:\/\/github.com\/projectcalico\/calico\/blob\/fbd467de86d2a18a7071d8e19ee47d72f7037065\/felix\/bpf-gpl\/tc.c. Accessed: 2025-09-01."},{"key":"e_1_3_2_1_27_1","first-page":"58","volume-title":"Richard Black. Fast Byte-Granularity Software Fault Isolation. In Proceedings SOSP '09","author":"Castro Miguel","year":"2009","unstructured":"Miguel Castro, Manuel Costa, Jean-Philippe Martin, Marcus Peinado, Periklis Akritidis, Austin Donnelly, Paul Barham, and Richard Black. Fast Byte-Granularity Software Fault Isolation. In Proceedings SOSP '09, page 45\u201358, New York, NY, USA, 2009."},{"key":"e_1_3_2_1_28_1","unstructured":"Cilium. eBPF-based Networking Security and Observability. https:\/\/github.com\/cilium\/cilium. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_29_1","unstructured":"Cilium project. bpf\/bpf_host.c. https:\/\/github.com\/cilium\/cilium\/blob\/4415e131d4c113d2d576d3a00f0d37445804eb81\/bpf\/bpf_host.c. Accessed: 2025-09-01."},{"key":"e_1_3_2_1_30_1","unstructured":"Cilium project. bpf\/bpf_lxc.c. https:\/\/github.com\/cilium\/cilium\/blob\/4415e131d4c113d2d576d3a00f0d37445804eb81\/bpf\/bpf_lxc.c. Accessed: 2025-09-01."},{"key":"e_1_3_2_1_31_1","first-page":"169","volume-title":"Helmut Veith. Counterexample-Guided Abstraction Refinement. In In Computer Aided Verification: 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings 12","author":"Clarke Edmund","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-Guided Abstraction Refinement. In In Computer Aided Verification: 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings 12, pages 154\u2013169. Springer, 2000."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","DOI":"10.21236\/ADA461189","volume-title":"Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM (JACM), 50(5):752\u2013794","author":"Clarke Edmund","year":"2003","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM (JACM), 50(5):752\u2013794, 2003."},{"issue":"7","key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","article-title":"SAT-Based Counterexample-Guided Abstraction Refinement","volume":"23","author":"Clarke Edmund M","year":"2004","unstructured":"Edmund M Clarke, Anubhav Gupta, and Ofer Strichman. SAT-Based Counterexample-Guided Abstraction Refinement. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 23(7):1113\u20131123, 2004.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_2_1_34_1","first-page":"152","volume-title":"Cook","author":"Cook Stephen A","unstructured":"Stephen A Cook. The Complexity of Theorem-Proving Procedures. In Logic, automata, and computational complexity: The works of Stephen A. Cook, pages 143\u2013152. 2023."},{"key":"e_1_3_2_1_35_1","volume-title":"October","author":"Corbet Jonathan","year":"2019","unstructured":"Jonathan Corbet. BPF at Facebook (and beyond). LWN.net, October 2019."},{"key":"e_1_3_2_1_36_1","first-page":"238","article-title":"A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints","volume":"97","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of POPL 97, page 238\u2013252, 1977.","journal-title":"Proceedings of POPL"},{"key":"e_1_3_2_1_37_1","first-page":"94","volume-title":"Cousot and Radhia Cousot. Static Determination of Dynamic Properties of Generalized Type Unions. In Proceedings of an ACM Conference on Language Design for Reliable Software","author":"Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot. Static Determination of Dynamic Properties of Generalized Type Unions. In Proceedings of an ACM Conference on Language Design for Reliable Software, page 77\u201394, New York, NY, USA, 1977. Association for Computing Machinery."},{"key":"e_1_3_2_1_38_1","first-page":"96","volume-title":"Proceedings of POPL","author":"Cousot Patrick","year":"1978","unstructured":"Patrick Cousot and Nicolas Halbwachs. Automatic Discovery of Linear Restraints Among Variables of a Program. In Proceedings of POPL, page 84\u201396, 1978."},{"key":"e_1_3_2_1_39_1","unstructured":"cvc5 Developers. cvc5 documentation - proofrule. https:\/\/cvc5.github.io\/docs\/latest\/api\/cpp\/enums\/proofrule.html. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_40_1","first-page":"388","volume-title":"Proceedings of the International Conference on Automated Deduction (CADE)","author":"Moura Leonardo De","year":"2015","unstructured":"Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Proceedings of the International Conference on Automated Deduction (CADE), pages 378\u2013388, 2015."},{"key":"e_1_3_2_1_41_1","first-page":"264","volume-title":"Practical Kernel Extensions. SOSP '24","author":"Dwivedi Kumar Kartikeya","year":"2024","unstructured":"Kumar Kartikeya Dwivedi, Rishabh Iyer, and Sanidhya Kashyap. Fast, Flexible, and Practical Kernel Extensions. SOSP '24, page 249\u2013264, New York, NY, USA, 2024. Association for Computing Machinery."},{"key":"e_1_3_2_1_42_1","unstructured":"eBPF Community. ebpf applications. https:\/\/ebpf.io\/applications\/. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_43_1","unstructured":"eBPF Community. eBPF Case Studies. https:\/\/ebpf.io\/case-studies\/. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_44_1","unstructured":"eBPF Maintainers. ebpf instruction set standardization documentation. https:\/\/docs.kernel.org\/bpf\/standardization\/instruction-set.html. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_45_1","unstructured":"elastic. Elastic eBPF Deployment. https:\/\/github.com\/elastic\/ebpf. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_46_1","first-page":"88","volume-title":"Proceedings of OSDI '06","author":"Erlingsson \u00dalfar","year":"2006","unstructured":"\u00dalfar Erlingsson, Mart\u00edn Abadi, Michael Vrable, Mihai Budiu, and George C. Necula. XFI: Software Guards for System Address Spaces. In Proceedings of OSDI '06, page 75\u201388, USA, 2006. USENIX Association."},{"key":"e_1_3_2_1_47_1","first-page":"390","volume-title":"Armin Biere. More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics With Binary Encoding. In International Computer Science Symposium in Russia","author":"Fr\u00f6hlich Andreas","unstructured":"Andreas Fr\u00f6hlich, Gergely Kov\u00e1sznai, and Armin Biere. More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics With Binary Encoding. In International Computer Science Symposium in Russia, pages 378\u2013390. Springer, 2013."},{"key":"e_1_3_2_1_48_1","first-page":"1084","volume-title":"Mooly Sagiv. Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions. In Proceedings of PLDI","author":"Gershuni Elazar","year":"2019","unstructured":"Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv. Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions. In Proceedings of PLDI, page 1069\u20131084, 2019."},{"key":"e_1_3_2_1_49_1","volume-title":"Suva, Fiji","author":"Hadarean Liana","year":"2015","unstructured":"Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, and Morgan Deters. Fine Grained Smt Proofs for the Theory of Fixed-Width Bit-Vectors. In Logic for Programming, Artificial Intelligence, and Reasoning: 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings 20, pages 340\u2013355. Springer, 2015."},{"key":"e_1_3_2_1_50_1","volume-title":"October","author":"Hodges Daniel","year":"2024","unstructured":"Daniel Hodges. Scheduling at Scale: eBPF Schedulers with Sched_ext. Dublin, October 2024. USENIX Association."},{"key":"e_1_3_2_1_51_1","first-page":"613","volume":"22","author":"Huang Yongzhe","year":"2022","unstructured":"Yongzhe Huang, Vikram Narayanan, David Detweiler, Kaiming Huang, Gang Tan, Trent Jaeger, and Anton Burtsev. KSplit: Automating Device Driver Isolation. In OSDI 22, pages 613\u2013631, Carlsbad, CA, July 2022. USENIX Association.","journal-title":"Automating Device Driver Isolation. In OSDI"},{"key":"e_1_3_2_1_52_1","unstructured":"inspektor gadget. Data collection and system inspection using eBPF. https:\/\/github.com\/inspektor-gadget\/inspektor-gadget. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_53_1","unstructured":"IOVisor project. ksnoop.bpf.c. https:\/\/github.com\/iovisor\/bcc\/blob\/0ae562c8862f4aa7a028a3f9bc561636a63a507d\/libbpf-tools\/ksnoop.bpf.c. Accessed: 2025-09-01."},{"key":"e_1_3_2_1_54_1","volume-title":"Practical and Flexible Kernel CFI Enforcement using eBPF. eBPF '23, page 84\u201385","author":"Jia Jinghao","year":"2023","unstructured":"Jinghao Jia, Michael V. Le, Salman Ahmed, Dan Williams, and Hani Jamjoom. Practical and Flexible Kernel CFI Enforcement using eBPF. eBPF '23, page 84\u201385, New York, NY, USA, 2023. Association for Computing Machinery."},{"key":"e_1_3_2_1_55_1","first-page":"342","volume-title":"2025 USENIX Annual Technical Conference (USENIX ATC 25)","author":"Jia Jinghao","year":"2025","unstructured":"Jinghao Jia, Ruowen Qin, Milo Craun, Egor Lukiyanov, Ayush Bansal, Minh Phan, Michael V Le, Hubertus Franke, Hani Jamjoom, Tianyin Xu, et al. Rex: Closing the language-verifier gap with safe and usable kernel extensions. In 2025 USENIX Annual Technical Conference (USENIX ATC 25), pages 325\u2013342, 2025."},{"key":"e_1_3_2_1_56_1","first-page":"157","volume-title":"Tianyin Xu. Kernel Extension Verification Is Untenable. In Proceedings of HOTOS '23","author":"Jia Jinghao","year":"2023","unstructured":"Jinghao Jia, Raj Sahu, Adam Oswald, Dan Williams, Michael V. Le, and Tianyin Xu. Kernel Extension Verification Is Untenable. In Proceedings of HOTOS '23, page 150\u2013157, New York, NY, USA, 2023. Association for Computing Machinery."},{"key":"e_1_3_2_1_57_1","volume-title":"Programmable System Call Security with eBPF","author":"Jia Jinghao","year":"2023","unstructured":"Jinghao Jia, YiFei Zhu, Dan Williams, Andrea Arcangeli, Claudio Canella, Hubertus Franke, Tobin Feldman-Fitzthum, Dimitrios Skarlatos, Daniel Gruss, and Tianyin Xu. Programmable System Call Security with eBPF, 2023."},{"key":"e_1_3_2_1_58_1","first-page":"288","volume-title":"USENIX ATC","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim, J Gregory Morrisett, Dan Grossman, Michael W Hicks, James Cheney, and Yanling Wang. Cyclone: A Safe Dialect of C. In USENIX ATC, pages 275\u2013288, 2002."},{"key":"e_1_3_2_1_59_1","first-page":"630","volume-title":"USENIX Security 24","author":"Jin Di","year":"2024","unstructured":"Di Jin, Alexander J. Gaidis, and Vasileios P. Kemerlis. BeeBox: Hardening BPF against Transient Execution Attacks. In USENIX Security 24, pages 613\u2013630, Philadelphia, PA, August 2024. USENIX Association."},{"key":"e_1_3_2_1_60_1","first-page":"620","volume-title":"Christos Kozyrakis. Syrup: User-Defined Scheduling Across the Stack. In Proceedings of SOSP '21","author":"Kaffes Kostis","year":"2021","unstructured":"Kostis Kaffes, Jack Tigar Humphries, David Mazi\u00e8res, and Christos Kozyrakis. Syrup: User-Defined Scheduling Across the Stack. In Proceedings of SOSP '21, page 605\u2013620, New York, NY, USA, 2021. Association for Computing Machinery."},{"issue":"7","key":"e_1_3_2_1_61_1","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic Execution and Program Testing","volume":"19","author":"King James C.","year":"1976","unstructured":"James C. King. Symbolic Execution and Program Testing. CACM, 19(7):385\u2013394, 1976.","journal-title":"CACM"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/s00224-015-9653-1","article-title":"Complexity of Fixed-Size Bit-Vector Logics","volume":"59","author":"Kov\u00e1sznai Gergely","year":"2016","unstructured":"Gergely Kov\u00e1sznai, Andreas Fr\u00f6hlich, and Armin Biere. Complexity of Fixed-Size Bit-Vector Logics. Theory of Computing Systems, 59:323\u2013376, 2016.","journal-title":"Theory of Computing Systems"},{"key":"e_1_3_2_1_63_1","first-page":"48","volume-title":"Proceedings of eBPF '23","author":"Lim Soo Yee","year":"2023","unstructured":"Soo Yee Lim, Xueyuan Han, and Thomas Pasquier. Unleashing Unprivileged eBPF Potential with Dynamic Sandboxing. In Proceedings of eBPF '23, page 42\u201348, New York, NY, USA, 2023. Association for Computing Machinery."},{"key":"e_1_3_2_1_64_1","volume-title":"Fengwei Zhang. MOAT: Towards Safe BPF Kernel Extension. In Proceedings of SEC '24","author":"Lu Hongyi","year":"2024","unstructured":"Hongyi Lu, Shuai Wang, Yechang Wu, Wanning He, and Fengwei Zhang. MOAT: Towards Safe BPF Kernel Extension. In Proceedings of SEC '24, USA, 2024. USENIX Association."},{"key":"e_1_3_2_1_65_1","volume-title":"McCanne and Van Jacobson. The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX","author":"Steven","year":"1993","unstructured":"Steven McCanne and Van Jacobson. The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX Winter 1993 Conference (USENIX Winter 1993 Conference), San Diego, CA, January 1993. USENIX Association."},{"key":"e_1_3_2_1_66_1","unstructured":"Microsoft. ebpf for windows. https:\/\/github.com\/microsoft\/ebpf-for-windows. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_67_1","volume-title":"A New Numerical Abstract Domain Based on Difference-Bound Matrices. PADO '01, page 155\u2013172","author":"Min\u00e9 Antoine","year":"2001","unstructured":"Antoine Min\u00e9. A New Numerical Abstract Domain Based on Difference-Bound Matrices. PADO '01, page 155\u2013172, Berlin, Heidelberg, 2001. Springer-Verlag."},{"key":"e_1_3_2_1_68_1","first-page":"319","volume-title":"Min\u00e9. The Octagon Abstract Domain. In Proceedings of WCRE","author":"Antoine","year":"2001","unstructured":"Antoine Min\u00e9. The Octagon Abstract Domain. In Proceedings of WCRE, pages 310\u2013319, 2001."},{"key":"e_1_3_2_1_69_1","first-page":"269","article-title":"Towards Isolation of Kernel Subsystems","volume":"19","author":"Narayanan Vikram","year":"2019","unstructured":"Vikram Narayanan, Abhiram Balasubramanian, Charlie Jacobsen, Sarah Spall, Scott Bauer, Michael Quigley, Aftab Hussain, Abdullah Younis, Junjie Shen, Moinak Bhattacharyya, and Anton Burtsev. LXDs: Towards Isolation of Kernel Subsystems. In USENIX ATC 19, pages 269\u2013284, Renton, WA, July 2019. USENIX Association.","journal-title":"USENIX ATC"},{"key":"e_1_3_2_1_70_1","volume-title":"Necula and Peter Lee. Safe Kernel Extensions Without Run-Time Checking. In USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"George","year":"1996","unstructured":"George C. Necula and Peter Lee. Safe Kernel Extensions Without Run-Time Checking. In USENIX Symposium on Operating Systems Design and Implementation (OSDI), 1996."},{"key":"e_1_3_2_1_71_1","first-page":"139","volume-title":"Westley Weimer. CCured: TypeSafe Retrofitting of Legacy Code. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"Necula George C","year":"2002","unstructured":"George C Necula, Scott McPeak, and Westley Weimer. CCured: TypeSafe Retrofitting of Legacy Code. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 128\u2013139, 2002."},{"key":"e_1_3_2_1_72_1","unstructured":"Luke Nelson Xi Wang and Emina Torlak. A Proof-Carrying Approach to Building Correct and Flexible In-Kernel Verifiers. https:\/\/homes.cs.washington.edu\/~lukenels\/slides\/2021-09-23-lpc21.pdf."},{"key":"e_1_3_2_1_73_1","first-page":"200","volume-title":"Yoni Zohar. Scalable Bit-Blasting With Abstractions. In International Conference on Computer Aided Verification","author":"Niemetz Aina","unstructured":"Aina Niemetz, Mathias Preiner, and Yoni Zohar. Scalable Bit-Blasting With Abstractions. In International Conference on Computer Aided Verification, pages 178\u2013200. Springer, 2024."},{"key":"e_1_3_2_1_74_1","unstructured":"OpenTelemetry. Verifier Imprecision in OpenTelemetry eBPF Profiler. https:\/\/github.com\/open-telemetry\/opentelemetry-ebpf-profiler\/blob\/fa444a2b9c38532fe04a5c856f48b09bb8b449c5\/support\/ebpf\/interpreter_dispatcher.ebpf.c#L334. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_75_1","unstructured":"Kindling Project. Verifier Imprecision in Agent-Libs. https:\/\/github.com\/KindlingProject\/agent-libs\/blob\/cfb3275cf5d03fc67d0242daee733d0bf4b6493a\/driver\/bpf\/types.h#L214. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_76_1","first-page":"14","volume-title":"Proceedings of the 2009 Conference on USENIX Annual Technical Conference, USENIX'09","author":"Matthew","year":"2009","unstructured":"Matthew J. Renzelmann and Michael M. Swift. Decaf: Moving Device Drivers to a Modern Language. In Proceedings of the 2009 Conference on USENIX Annual Technical Conference, USENIX'09, page 14, USA, 2009. USENIX Association."},{"issue":"1","key":"e_1_3_2_1_77_1","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson J. A.","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23\u201341, January 1965.","journal-title":"J. ACM"},{"key":"e_1_3_2_1_78_1","unstructured":"sched ext. Verifier imprecision in sched_ext. https:\/\/github.com\/sched-ext\/scx\/blob\/5933fc301ed1eee59bbe0a61da279748cce6b43a\/scheds\/rust\/scx_layered\/src\/bpf\/util.bpf.c#L24. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_79_1","first-page":"227","volume-title":"Proceedings of OSDI 96","author":"Seltzer Margo I.","year":"1996","unstructured":"Margo I. Seltzer, Yasuhiro Endo, Christopher Small, and Keith A. Smith. Dealing with disaster: surviving misbehaved kernel extensions. In Proceedings of OSDI 96, page 213\u2013227, New York, NY, USA, 1996. Association for Computing Machinery."},{"key":"e_1_3_2_1_80_1","unstructured":"Alexei Starovoitov and Daniel Borkmann. The ebpf verifier. https:\/\/docs.kernel.org\/bpf\/verifier.html. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_81_1","unstructured":"Alexei Starovoitov and Daniel Borkmann. The eBPF Subsystem. https:\/\/docs.kernel.org\/bpf\/. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_82_1","volume-title":"Accessed","author":"Sun Hao","year":"2025","unstructured":"Hao Sun. BCF: artifact-evaluation branch. https:\/\/github.com\/SunHao-0\/BCF\/tree\/artifact-evaluation, 2025. Accessed August 12, 2025."},{"key":"e_1_3_2_1_83_1","volume-title":"Accessed","author":"Sun Hao","year":"2025","unstructured":"Hao Sun. BCF: artifact-evaluation program dataset. https:\/\/github.com\/SunHao-0\/BCF\/tree\/artifact-evaluation\/bpf-progs, 2025. Accessed August 12, 2025."},{"issue":"5","key":"e_1_3_2_1_84_1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1165389.945466","volume":"37","author":"Swift Michael M.","year":"2003","unstructured":"Michael M. Swift, Brian N. Bershad, and Henry M. Levy. Improving the Reliability of Commodity Operating Systems. SIGOPS Oper. Syst. Rev., 37(5):207\u2013222, oct 2003.","journal-title":"Levy. Improving the Reliability of Commodity Operating Systems. SIGOPS Oper. Syst. Rev."},{"key":"e_1_3_2_1_85_1","unstructured":"Benjamin Tissoires. Hid-bpf documentation. https:\/\/docs.kernel.org\/hid\/hid-bpf.html. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_86_1","volume-title":"Code, Challenges, and Applications. ACM Comput. Surv., 53(1), feb","author":"Vieira Marcos A. M.","year":"2020","unstructured":"Marcos A. M. Vieira, Matheus S. Castanho, Racyus D. G. Pac\u00edfico, Elerson R. S. Santos, Eduardo P. M. C\u00e2mara J\u00fanior, and Luiz F. M. Vieira. Fast Packet Processing with EBPF and XDP: Concepts, Code, Challenges, and Applications. ACM Comput. Surv., 53(1), feb 2020."},{"key":"e_1_3_2_1_87_1","first-page":"265","volume-title":"Fast Abstract Interpretation With Tristate Numbers. In Proceedings of CGO","author":"Vishwanathan Harishankar","year":"2022","unstructured":"Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. Sound, Precise, and Fast Abstract Interpretation With Tristate Numbers. In Proceedings of CGO, pages 254\u2013265, 2022."},{"key":"e_1_3_2_1_88_1","first-page":"251","volume-title":"CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part III","author":"Vishwanathan Harishankar","year":"2023","unstructured":"Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. Verifying the Verifier: eBPF Range Analysis Verification. In CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part III, page 226\u2013251, Berlin, Heidelberg, 2023. Springer-Verlag."},{"key":"e_1_3_2_1_89_1","unstructured":"Xiwei Wu Qinxiang Cao Shizhen Zhao Yueyang Feng Tianyi Huang Xiaoyang Lu Lihan Xie and Shengkai Lin. VEP: A Two-stage Verification Toolchain for Full eBPF Programmability."},{"key":"e_1_3_2_1_90_1","unstructured":"xdp-project. bpf-examples. https:\/\/github.com\/xdp-project\/bpf-examples. Accessed: 2025-03-12."},{"key":"e_1_3_2_1_91_1","unstructured":"XDP project. pping\/pping_kern.c. https:\/\/github.com\/xdp-project\/bpf-examples\/blob\/main\/pping\/pping_kern.c. Accessed: 2025-09-01."},{"key":"e_1_3_2_1_92_1","unstructured":"XDP project. xdp-synproxy\/xdp_synproxy_kern.c. https:\/\/github.com\/xdp-project\/bpf-examples\/blob\/d1cc8a27e75498b6c06ee67fd66bf37b05900f80\/xdp-synproxy\/xdp_synproxy_kern.c. Accessed: 2025-09-01."},{"key":"e_1_3_2_1_93_1","first-page":"362","volume-title":"FAST 23","author":"Yang Zhe","year":"2023","unstructured":"Zhe Yang, Youyou Lu, Xiaojian Liao, Youmin Chen, Junru Li, Siyu He, and Jiwu Shu. \u03bb-IO: A Unified IO Stack for Computational Storage. In FAST 23, pages 347\u2013362, Santa Clara, CA, February 2023."},{"key":"e_1_3_2_1_94_1","volume-title":"BPF-oF: Storage Function Pushdown Over the Network. arXiv preprint arXiv:2312.06808","author":"Zarkadas Ioannis","year":"2023","unstructured":"Ioannis Zarkadas, Tal Zussman, Jeremy Carin, Sheng Jiang, Yuhong Zhong, Jonas Pfefferle, Hubertus Franke, Junfeng Yang, Kostis Kaffes, Ryan Stutsman, et al. BPF-oF: Storage Function Pushdown Over the Network. arXiv preprint arXiv:2312.06808, 2023."},{"key":"e_1_3_2_1_95_1","first-page":"180","volume-title":"USENIX Security 24","author":"Zhang Peihua","year":"2024","unstructured":"Peihua Zhang, Chenggang Wu, Xiangyu Meng, Yinqian Zhang, Mingfan Peng, Shiyang Zhang, Bing Hu, Mengyao Xie, Yuanming Lai, Yan Kang, and Zhe Wang. HIVE: A Hardware-assisted Isolated Execution Environment for eBPF on AArch64. In USENIX Security 24, pages 163\u2013180, Philadelphia, PA, August 2024. USENIX Association."},{"key":"e_1_3_2_1_96_1","first-page":"41","volume-title":"Proceedings EuroSys","author":"Zhong Shawn Wanxiang","year":"2025","unstructured":"Shawn Wanxiang Zhong, Jing Liu, Andrea Arpaci-Dusseau, and Remzi Arpaci-Dusseau. Revealing the Unstable Foundations of eBPF-Based Kernel Extensions. In Proceedings EuroSys, pages 21\u201341, 2025."},{"key":"e_1_3_2_1_97_1","first-page":"393","volume-title":"OSDI 22","author":"Zhong Yuhong","year":"2022","unstructured":"Yuhong Zhong, Haoyu Li, Yu Jian Wu, Ioannis Zarkadas, Jeffrey Tao, Evan Mesterhazy, Michael Makris, Junfeng Yang, Amy Tai, Ryan Stutsman, and Asaf Cidon. XRP: In-Kernel Storage Functions with eBPF. In OSDI 22, pages 375\u2013393, July 2022."},{"key":"e_1_3_2_1_98_1","first-page":"60","volume-title":"Eric Brewer. SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI '06","author":"Zhou Feng","year":"2006","unstructured":"Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew Harren, George Necula, and Eric Brewer. SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI '06, page 45\u201360, USA, 2006. USENIX Association."},{"key":"e_1_3_2_1_99_1","first-page":"417","volume-title":"NSDI 24","author":"Zhou Yang","year":"2024","unstructured":"Yang Zhou, Xingyu Xiang, Matthew Kiley, Sowmya Dharanipragada, and Minlan Yu. DINT: Fast In-Kernel Distributed Transactions with eBPF. In NSDI 24, pages 401\u2013417, Santa Clara, CA, April 2024. USENIX Association."},{"key":"e_1_3_2_1_100_1","first-page":"518","volume-title":"International Conference on Verification, Model Checking, and Abstract Interpretation","author":"Zohar Yoni","unstructured":"Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres N\u00f6tzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning via Int-Blasting. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 496\u2013518. Springer, 2022."},{"key":"e_1_3_2_1_101_1","volume-title":"Cache is King: Smart Page Eviction with eBPF. arXiv preprint arXiv:2502.02750","author":"Zussman Tal","year":"2025","unstructured":"Tal Zussman, Ioannis Zarkadas, Jeremy Carin, Andrew Cheng, Hubertus Franke, Jonas Pfefferle, and Asaf Cidon. Cache is King: Smart Page Eviction with eBPF. arXiv preprint arXiv:2502.02750, 2025."}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Lotte Hotel World Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles"],"original-title":[],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:56:17Z","timestamp":1759323377000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764796"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":101,"alternative-id":["10.1145\/3731569.3764796","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764796","relation":{},"subject":[],"published":{"date-parts":[[2025,10,12]]},"assertion":[{"value":"2025-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}