{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:23:35Z","timestamp":1763054615059,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":102,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T00:00:00Z","timestamp":1760313600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2247687,2312346"],"award-info":[{"award-number":["2247687,2312346"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR001124C0486"],"award-info":[{"award-number":["HR001124C0486"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3764860.3768336","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T13:54:43Z","timestamp":1759326883000},"page":"118-126","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["KLean: Extending Operating System Kernels with Lean"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2950-6964","authenticated-orcid":false,"given":"Di","family":"Jin","sequence":"first","affiliation":[{"name":"Brown University, Providence, Rhode Island, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6750-4615","authenticated-orcid":false,"given":"Ethan","family":"Lavi","sequence":"additional","affiliation":[{"name":"Brown University, Providence, Rhode Island, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0837-4677","authenticated-orcid":false,"given":"Jinghao","family":"Jia","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, Champaign, Illinois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5266-1121","authenticated-orcid":false,"given":"Robert Y.","family":"Lewis","sequence":"additional","affiliation":[{"name":"Brown University, Providence, Rhode Island, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7347-298X","authenticated-orcid":false,"given":"Nikos","family":"Vasilakis","sequence":"additional","affiliation":[{"name":"Brown University, Providence, Rhode Island, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,13]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/github.com\/aya-rs\/aya\/issues\/100. (Nov","author":"Access","year":"2021","unstructured":"Access packet data as & [u8] from XdpContext. https:\/\/github.com\/aya-rs\/aya\/issues\/100. (Nov. 2021)."},{"key":"e_1_3_2_1_2_1","volume-title":"c_chars, and [u8]. https:\/\/github.com\/aya-rs\/aya\/issues\/546. (Mar","author":"Verifier","year":"2023","unstructured":"BPF Verifier errors when using aya logger with strings, c_chars, and [u8]. https:\/\/github.com\/aya-rs\/aya\/issues\/546. (Mar. 2023)."},{"key":"e_1_3_2_1_3_1","unstructured":"bpf-helpers(7) - Linux manual page. https:\/\/man7.org\/linux\/man-pages\/man7\/bpf-helpers.7.html."},{"key":"e_1_3_2_1_4_1","unstructured":"Lean git history. https:\/\/github.com\/leanprover\/lean4\/commits\/master\/src\/kernel\/type_checker.cpp."},{"key":"e_1_3_2_1_5_1","unstructured":"libbpf. https:\/\/github.com\/libbpf\/libbpf."},{"volume-title":"https:\/\/github.com\/aya-rs\/aya\/issues\/521. (Feb","year":"2023","key":"e_1_3_2_1_6_1","unstructured":"missing btf func_info whilst using bpf_loop(). https:\/\/github.com\/aya-rs\/aya\/issues\/521. (Feb. 2023)."},{"key":"e_1_3_2_1_7_1","unstructured":"nanoda_lib. https:\/\/github.com\/ammkrn\/nanoda_lib\/."},{"key":"e_1_3_2_1_8_1","unstructured":"ptrace(2) - Linux manual page. https:\/\/man7.org\/linux\/man-pages\/man2\/ptrace.2.html."},{"key":"e_1_3_2_1_9_1","unstructured":"Windows Subsystem for Linux. https:\/\/github.com\/microsoft\/WSL."},{"volume-title":"December","year":"2017","key":"e_1_3_2_1_10_1","unstructured":"CVE-2017-17864. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2017-17864, December 2017."},{"volume-title":"October","year":"2018","key":"e_1_3_2_1_11_1","unstructured":"CVE-2018-18445. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2018-18445, October 2018."},{"volume-title":"February","year":"2020","key":"e_1_3_2_1_12_1","unstructured":"CVE-2020-8835. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2020-8835, February 2020."},{"volume-title":"April","year":"2021","key":"e_1_3_2_1_13_1","unstructured":"CVE-2021-3490. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-3490, April 2021."},{"key":"e_1_3_2_1_14_1","unstructured":"Alden D. A new type of spinlock for the BPF subsystem. https:\/\/lwn.net\/Articles\/1016674\/."},{"key":"e_1_3_2_1_15_1","unstructured":"Alden D. Formally verifying the BPF verifier. https:\/\/lwn.net\/Articles\/1020664\/."},{"key":"e_1_3_2_1_16_1","unstructured":"Alden D. Verifying the BPF verifier's path-exploration logic. https:\/\/lwn.net\/Articles\/1021825\/."},{"key":"e_1_3_2_1_17_1","first-page":"3","article-title":"A survey of symbolic execution techniques","volume":"51","author":"Baldoni R.","year":"2018","unstructured":"Baldoni, R., Coppa, E., D'Elia, D. C., Demetrescu, C., and Finocchi, I. A survey of symbolic execution techniques. ACM Comput. Surv. 51, 3 (2018).","journal-title":"ACM Comput. Surv."},{"key":"e_1_3_2_1_18_1","volume-title":"bpf: compress maglev per service lut into flat slot id array. https:\/\/github.com\/cilium\/cilium\/commit\/bfaef16f34851aada5189df2eaebce351dd2543e. (Sept","author":"Borkmann D.","year":"2020","unstructured":"Borkmann, D. bpf: compress maglev per service lut into flat slot id array. https:\/\/github.com\/cilium\/cilium\/commit\/bfaef16f34851aada5189df2eaebce351dd2543e. (Sept. 2020)."},{"key":"e_1_3_2_1_19_1","volume-title":"bpf: Fix alu32 const subreg bound tracking on bitwise operations. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=049c4e13714ecbca567b4d5f6d563f05d431c80e. (May","author":"Borkmann D.","year":"2021","unstructured":"Borkmann, D. bpf: Fix alu32 const subreg bound tracking on bitwise operations. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=049c4e13714ecbca567b4d5f6d563f05d431c80e. (May. 2021)."},{"key":"e_1_3_2_1_20_1","volume-title":"bpf: Fix check_return_code to only allow [0, 1] in trace_iter progs. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2ec0616e870f0f2aa8353e0de057f0c2dc8d52d5. (May","author":"Borkmann D.","year":"2020","unstructured":"Borkmann, D. bpf: Fix check_return_code to only allow [0, 1] in trace_iter progs. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2ec0616e870f0f2aa8353e0de057f0c2dc8d52d5. (May. 2020)."},{"key":"e_1_3_2_1_21_1","unstructured":"Borkmann D. bpf: Fix incorrect verifier pruning due to missing register precision taints. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=71b547f561247897a0a14f3082730156c0533fed. (Apr. 2023)."},{"key":"e_1_3_2_1_22_1","volume-title":"bpf: Fix pointer arithmetic mask tightening under state pruning. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=e042aa532c84d18ff13291d00620502ce7a38dda. (Jul","author":"Borkmann D.","year":"2021","unstructured":"Borkmann, D. bpf: Fix pointer arithmetic mask tightening under state pruning. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=e042aa532c84d18ff13291d00620502ce7a38dda. (Jul. 2021)."},{"key":"e_1_3_2_1_23_1","volume-title":"bpf: Fix verifier jmp32 pruning decision logic. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=fd675184fc7abfd1e1c52d23e8e900676b5a1c1a. (Feb","author":"Borkmann D.","year":"2021","unstructured":"Borkmann, D. bpf: Fix verifier jmp32 pruning decision logic. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=fd675184fc7abfd1e1c52d23e8e900676b5a1c1a. (Feb. 2021)."},{"key":"e_1_3_2_1_24_1","volume-title":"bpf: Undo incorrect___reg_bound_offset32 handling. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=f2d67fec0b43edce8c416101cdc52e71145b5fef. (Mar","author":"Borkmann D.","year":"2020","unstructured":"Borkmann, D. bpf: Undo incorrect___reg_bound_offset32 handling. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=f2d67fec0b43edce8c416101cdc52e71145b5fef. (Mar. 2020)."},{"key":"e_1_3_2_1_25_1","volume-title":"bpf, verifier: further improve search pruning. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=07016151a446d25397b24588df4ed5cf777a69bb. (Aug","author":"Borkmann D.","year":"2016","unstructured":"Borkmann, D. bpf, verifier: further improve search pruning. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=07016151a446d25397b24588df4ed5cf777a69bb. (Aug. 2016)."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_27_1","first-page":"369","volume-title":"2024 USENIX Annual Technical Conference (USENIX ATC 24)","author":"Cao X.","year":"2024","unstructured":"Cao, X., Patel, S., Lim, S. Y., Han, X., and Pasquier, T. FetchBPF: Customizable prefetching policies in linux with eBPF. In 2024 USENIX Annual Technical Conference (USENIX ATC 24) (2024), pp. 369--378."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_3_2_1_29_1","volume-title":"bpf: Fix incorrect state pruning for <8B spill\/fill. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=345e004d023343d38088fdfea39688aa11e06ccf. (Dec","author":"Chaignon P.","year":"2021","unstructured":"Chaignon, P. bpf: Fix incorrect state pruning for <8B spill\/fill. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=345e004d023343d38088fdfea39688aa11e06ccf. (Dec. 2021)."},{"key":"e_1_3_2_1_30_1","volume-title":"System deadlocks. ACM Computing Surveys (CSUR) 3, 2","author":"Coffman E. G.","year":"1971","unstructured":"Coffman, E. G., Elphick, M., and Shoshani, A. System deadlocks. ACM Computing Surveys (CSUR) 3, 2 (1971), 67--78."},{"key":"e_1_3_2_1_31_1","unstructured":"Corbet J. A JIT for packet filters. https:\/\/lwn.net\/Articles\/437981\/."},{"key":"e_1_3_2_1_32_1","volume-title":"bpf\/verifier: fix bounds calculation on BPFRSH. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=4374f256ce8182019353c0c639bb8d0695b4c941. (Dec","author":"Cree E.","year":"2017","unstructured":"Cree, E. bpf\/verifier: fix bounds calculation on BPFRSH. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=4374f256ce8182019353c0c639bb8d0695b4c941. (Dec. 2017)."},{"key":"e_1_3_2_1_33_1","volume-title":"bpf\/verifier: track liveness for pruning. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=dc503a8ad98474ea0073a1c5c4d9f18cb8dd0dbf. (Aug","author":"Cree E.","year":"2017","unstructured":"Cree, E. bpf\/verifier: track liveness for pruning. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=dc503a8ad98474ea0073a1c5c4d9f18cb8dd0dbf. (Aug. 2017)."},{"key":"e_1_3_2_1_34_1","volume-title":"bpf\/verifier: track signed and unsigned min\/max values. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=b03c9f9fdc37dab81ea04d5dacdc5995d4c224c2. (Aug","author":"Cree E.","year":"2017","unstructured":"Cree, E. bpf\/verifier: track signed and unsigned min\/max values. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=b03c9f9fdc37dab81ea04d5dacdc5995d4c224c2. (Aug. 2017)."},{"key":"e_1_3_2_1_35_1","volume-title":"bpf\/verifier: when pruning a branch, ignore its write marks. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=63f45f840634ab5fd71bbc07acff915277764068. (Aug","author":"Cree E.","year":"2017","unstructured":"Cree, E. bpf\/verifier: when pruning a branch, ignore its write marks. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=63f45f840634ab5fd71bbc07acff915277764068. (Aug. 2017)."},{"key":"e_1_3_2_1_36_1","first-page":"885","volume-title":"2022 USENIX Annual Technical Conference (USENIX ATC 22)","author":"Curtsinger C.","year":"2022","unstructured":"Curtsinger, C., and Barowy, D. W. Riker:Always-Correct and fast incremental builds from simple specifications. In 2022 USENIX Annual Technical Conference (USENIX ATC 22) (2022), pp. 885--898."},{"key":"e_1_3_2_1_37_1","volume-title":"Minor tweaks to make the verifier's job easier. https:\/\/github.com\/aya-rs\/aya\/commit\/2ac433449cdea32f10c8fc88218799995946032d. (Jul","author":"Decina A.","year":"2022","unstructured":"Decina, A. Minor tweaks to make the verifier's job easier. https:\/\/github.com\/aya-rs\/aya\/commit\/2ac433449cdea32f10c8fc88218799995946032d. (Jul. 2022)."},{"key":"e_1_3_2_1_38_1","volume-title":"bpf: Fix state pruning for STACK_DYNPTR stack slots. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=d6fefa1105dacc8a742cdcf2f4bfb501c9e61349. (Jan","author":"Dwivedi K. K.","year":"2023","unstructured":"Dwivedi, K. K. bpf: Fix state pruning for STACK_DYNPTR stack slots. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=d6fefa1105dacc8a742cdcf2f4bfb501c9e61349. (Jan. 2023)."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695950"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2506375"},{"key":"e_1_3_2_1_42_1","volume-title":"SysXCHG: Refining Privilege with Adaptive System Call Filters. In ACM Conference on Computer and Communications Security (CCS)","author":"Gaidis A.J.","year":"2023","unstructured":"Gaidis, A.J., Atlidakis, v., and Kemerlis, V. P. SysXCHG: Refining Privilege with Adaptive System Call Filters. In ACM Conference on Computer and Communications Security (CCS) (2023)."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477113.3487267"},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI'21)","author":"Ghigoff Y.","year":"2021","unstructured":"Ghigoff, Y., Sopena, J., Lazri, K., Blin, A., and Muller, G. BMC: Accelerating Memcached using Safe In-kernel Caching and Pre-stack Processing. In Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI'21) (Apr. 2021)."},{"key":"e_1_3_2_1_45_1","volume-title":"bpf: Fix verifier error when writing to skbcb[0]. https:\/\/github.com\/cilium\/cilium\/commit\/1e25adb69b44573ecaea42803fff7312fbfe9372. (May","author":"Graf T.","year":"2023","unstructured":"Graf, T. bpf: Fix verifier error when writing to skbcb[0]. https:\/\/github.com\/cilium\/cilium\/commit\/1e25adb69b44573ecaea42803fff7312fbfe9372. (May. 2023)."},{"key":"e_1_3_2_1_46_1","volume-title":"2011 USENIX Annual Technical Conference (USENIX ATC 11)","author":"Guo P. J.","year":"2011","unstructured":"Guo, P. J., and Engler, D. CDE: Using system call interposition to automatically create portable software packages. In 2011 USENIX Annual Technical Conference (USENIX ATC 11) (2011)."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_6"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483542"},{"key":"e_1_3_2_1_49_1","unstructured":"IO Visor Project. BPF Compiler Collection (BCC). https:\/\/github.com\/iovisor\/bcc."},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of the 2025 USENIX Annual Technical Conference (USENIX ATC'25) (July","author":"Jia J.","year":"2025","unstructured":"Jia, J., Qin, R., Craun, M., Lukiyanov, E., Bansal, A., Phan, M., Le, M. V., Franke, H., Jamjoom, H., Xu, T., and Williams, D. Rex: Closing the Language-Verifier Gap with Safe and Usable Kernel Extensions. In Proceedings of the 2025 USENIX Annual Technical Conference (USENIX ATC'25) (July 2025)."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593856.3595892"},{"key":"e_1_3_2_1_52_1","unstructured":"Jose E. Marchesi. eBPF support for GCC. https:\/\/gcc.gnu.org\/legacy-ml\/gcc-patches\/2019-08\/msg01987.html."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483548"},{"key":"e_1_3_2_1_54_1","first-page":"139","volume-title":"2013 USENIX Annual Technical Conference (USENIX ATC 13)","author":"Kim T.","year":"2013","unstructured":"Kim, T., and Zeldovich, N. Practical and effective sandboxing for non-root users. In 2013 USENIX Annual Technical Conference (USENIX ATC 13) (2013), pp. 139--144."},{"key":"e_1_3_2_1_55_1","first-page":"207","volume-title":"SOSP '09","author":"Klein G.","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., and Winwood, S. sel4: formal verification of an os kernel. SOSP '09, Association for Computing Machinery, p. 207--220."},{"key":"e_1_3_2_1_56_1","unstructured":"Koong J. bpf: Add bpf_loop helper. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=e6f2dd0f80674e9d5960337b3e9c2a242441b326."},{"key":"e_1_3_2_1_57_1","volume-title":"bpf: Add verifier support for dynptrs. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=97e03f521050c092919591e668107b3d69c5f426. (May","author":"Koong J.","year":"2022","unstructured":"Koong, J. bpf: Add verifier support for dynptrs. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=97e03f521050c092919591e668107b3d69c5f426. (May. 2022)."},{"key":"e_1_3_2_1_58_1","volume-title":"Set Theory an Introduction to Independence Proofs","author":"Kunen K.","year":"2014","unstructured":"Kunen, K. Set Theory an Introduction to Independence Proofs, vol. 102. Elsevier, 2014."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_1_60_1","volume-title":"bpf: Support <8-byte scalar spill and refill. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=354e8f1970f821d4952458f77b1ab6c3eb24d530. (Sep","author":"Lau M. K.","year":"2021","unstructured":"Lau, M. K. bpf: Support <8-byte scalar spill and refill. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=354e8f1970f821d4952458f77b1ab6c3eb24d530. (Sep. 2021)."},{"key":"e_1_3_2_1_61_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress","author":"Leroy X.","year":"2016","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., and Ferdinand, C. Compcert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress (2016)."},{"key":"e_1_3_2_1_62_1","unstructured":"Linux Developers. BPF Kernel Functions (kfuncs). https:\/\/docs.kernel.org\/bpf\/kfuncs.html."},{"key":"e_1_3_2_1_63_1","unstructured":"Linux Kernel. Softlockup detector and hardlockup detector (aka nmi_watchdog). https:\/\/docs.kernel.org\/admin-guide\/lockup-watchdogs.html."},{"key":"e_1_3_2_1_64_1","unstructured":"LLVM Project. LLVM 3.7 Release Notes. https:\/\/releases.llvm.org\/3.7.0\/docs\/ReleaseNotes.html#non-comprehensive-list-of-changes-in-this-release."},{"key":"e_1_3_2_1_65_1","volume-title":"bpf: Allow variable-offset stack access. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=01f810ace9ed37255f27608a0864abebccf0aab3. (Dec","author":"Matei A.","year":"2023","unstructured":"Matei, A. bpf: Allow variable-offset stack access. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=01f810ace9ed37255f27608a0864abebccf0aab3. (Dec. 2023)."},{"key":"e_1_3_2_1_66_1","volume-title":"bpf: Fix verification of indirect var-off stack access. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=a833a17aeac73b33f79433d7cee68d5cafd71e4f. (Dec","author":"Matei A.","year":"2023","unstructured":"Matei, A. bpf: Fix verification of indirect var-off stack access. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=a833a17aeac73b33f79433d7cee68d5cafd71e4f. (Dec. 2023)."},{"key":"e_1_3_2_1_67_1","volume-title":"bpf: Protect against int overflow for stack access size. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=ecc6a2101840177e57c925c102d2d29f260d37c8. (Mar","author":"Matei A.","year":"2024","unstructured":"Matei, A. bpf: Protect against int overflow for stack access size. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=ecc6a2101840177e57c925c102d2d29f260d37c8. (Mar. 2024)."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_69_1","volume-title":"The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX Winter Conference","author":"McCanne S.","year":"1993","unstructured":"McCanne, S., and Jacobson, V. The BSD Packet Filter: A New Architecture for User-level Packet Capture. In USENIX Winter Conference (1993)."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.001"},{"key":"e_1_3_2_1_71_1","unstructured":"Molnar I. and van de Ven A. Runtime locking correctness validator. https:\/\/www.kernel.org\/doc\/Documentation\/locking\/lockdep-design.txt."},{"key":"e_1_3_2_1_72_1","first-page":"625","volume-title":"S. The lean 4 theorem prover and programming language. In Automated Deduction - CADE 28 (Cham","author":"Moura L.","year":"2021","unstructured":"Moura, L. d., and Ullrich, S. The lean 4 theorem prover and programming language. In Automated Deduction - CADE 28 (Cham, 2021), A. Platzer and G. Sutcliffe, Eds., Springer International Publishing, pp. 625--635."},{"key":"e_1_3_2_1_73_1","unstructured":"Nakryiko A. bpf: add support for open-coded iterator loops. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=06accc8779c1d558a5b5a21f2ac82b0c95827ddd."},{"key":"e_1_3_2_1_74_1","volume-title":"bpf: decouple prune and jump points. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=bffdeaa8a5af7200b0e74c9d5a41167f86626a36. (Dec","author":"Nakryiko A.","year":"2022","unstructured":"Nakryiko, A. bpf: decouple prune and jump points. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=bffdeaa8a5af7200b0e74c9d5a41167f86626a36. (Dec. 2022)."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_76_1","volume-title":"Linux Plumbers Conference","author":"Nelson L.","year":"2021","unstructured":"Nelson, L., Wang, X., and Torlak, E. A proof-carrying approach to building correct and flexible in-kernel verifiers. In Linux Plumbers Conference (2021)."},{"key":"e_1_3_2_1_77_1","unstructured":"Nikita Shirokov and Ranjeeth Dasineni. Open-sourcing Katran a scalable network load balancer. https:\/\/engineering.fb.com\/2018\/05\/22\/open-source\/open-sourcing-katran-a-scalable-network-load-balancer\/."},{"key":"e_1_3_2_1_78_1","volume-title":"bpf, test: Fix verifier issues in IPv6 BPF tests when running locally. https:\/\/github.com\/cilium\/cilium\/commit\/ceaa4c42b0101c69d82407046e8437942237edcb. (May","author":"Reimerink D.","year":"2023","unstructured":"Reimerink, D. bpf, test: Fix verifier issues in IPv6 BPF tests when running locally. https:\/\/github.com\/cilium\/cilium\/commit\/ceaa4c42b0101c69d82407046e8437942237edcb. (May. 2023)."},{"key":"e_1_3_2_1_79_1","unstructured":"snarky developers. Ocaml dsl for verifiable computation. https:\/\/github.com\/o1-labs\/snarky."},{"key":"e_1_3_2_1_80_1","unstructured":"Song Y. bpf: Add bpf_for_each_map_elem() helper. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=69c087ba6225b574afb6e505b72cb75242a3d844."},{"key":"e_1_3_2_1_81_1","volume-title":"bpf: Fix a verifier failure with xor. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2921c90d471889242c24cff529043afb378937fa. (Aug","author":"Song Y.","year":"2020","unstructured":"Song, Y. bpf: Fix a verifier failure with xor. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2921c90d471889242c24cff529043afb378937fa. (Aug. 2020)."},{"key":"e_1_3_2_1_82_1","volume-title":"bpf: Provide better register bounds after jmp32 instructions. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=581738a681b6faae5725c2555439189ca81c0f1f. (Nov","author":"Song Y.","year":"2019","unstructured":"Song, Y. bpf: Provide better register bounds after jmp32 instructions. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=581738a681b6faae5725c2555439189ca81c0f1f. (Nov. 2019)."},{"key":"e_1_3_2_1_83_1","volume-title":"bpf: add search pruning optimization to verifier. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=f1bca824dabba4ffe8582f87ca587780befce7ad. (Sept","author":"Starovoitov A.","year":"2014","unstructured":"Starovoitov, A. bpf: add search pruning optimization to verifier. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=f1bca824dabba4ffe8582f87ca587780befce7ad. (Sept. 2014)."},{"key":"e_1_3_2_1_84_1","volume-title":"bpf: fix callees pruning callers. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=eea1c227b9e9bad295e8ef984004a9acf12bb68c. (Jun","author":"Starovoitov A.","year":"2019","unstructured":"Starovoitov, A. bpf: fix callees pruning callers. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=eea1c227b9e9bad295e8ef984004a9acf12bb68c. (Jun. 2019)."},{"key":"e_1_3_2_1_85_1","unstructured":"Starovoitov A. bpf: introduce bounded loops. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2589726d12a1b12eaaa93c7f1ea64287e383c7a5."},{"key":"e_1_3_2_1_86_1","volume-title":"bpf: introduce bpf_spin_lock. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=d83525ca62cf8ebe3271d14c36fb900c294274a2. (Jan","author":"Starovoitov A.","year":"2019","unstructured":"Starovoitov, A. bpf: introduce bpf_spin_lock. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=d83525ca62cf8ebe3271d14c36fb900c294274a2. (Jan. 2019)."},{"key":"e_1_3_2_1_87_1","volume-title":"bpf: verifier (add docs). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=51580e798cb61b0fc63fa3aa6c5c975375aa0550. (Sept","author":"Starovoitov A.","year":"2014","unstructured":"Starovoitov, A. bpf: verifier (add docs). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=51580e798cb61b0fc63fa3aa6c5c975375aa0550. (Sept. 2014)."},{"key":"e_1_3_2_1_88_1","volume-title":"precise scalar_value tracking. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=b5dc0163d8fd78e64a7e21f309cf932fda34353e. (Jun","author":"Starovoitov A.","year":"2019","unstructured":"Starovoitov, A. precise scalar_value tracking. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=b5dc0163d8fd78e64a7e21f309cf932fda34353e. (Jun. 2019)."},{"key":"e_1_3_2_1_89_1","volume-title":"Lazy Abstraction Refinement with Proof. In Linux Plumbers Conference (LPC'24)","author":"Sun H.","year":"1939","unstructured":"Sun, H., and Su, Z. Lazy Abstraction Refinement with Proof. In Linux Plumbers Conference (LPC'24). https:\/\/lpc.events\/event\/18\/contributions\/1939\/. (Sept. 2024)."},{"key":"e_1_3_2_1_90_1","unstructured":"The Cilium Authors. Cilium: eBPF-based Networking Observability Security. https:\/\/cilium.io\/."},{"key":"e_1_3_2_1_91_1","first-page":"9","author":"The Rocq Development Team","year":"2025","unstructured":"The Rocq Development Team. The Rocq Prover Reference Manual. Inria, 2025. Version 9.0.0.","journal-title":"The Rocq Prover Reference Manual. Inria"},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547640"},{"key":"e_1_3_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_12"},{"key":"e_1_3_2_1_94_1","volume-title":"Linux Plumbers Conference","author":"Williams D.","year":"2023","unstructured":"Williams, D., and Sahu, R. When bpf programs need to die: exploring the design space for early bpf termination. In Linux Plumbers Conference (2023)."},{"key":"e_1_3_2_1_95_1","first-page":"291","volume-title":"2025 USENIX Annual Technical Conference (USENIX ATC 25)","author":"Yelam A.","year":"2025","unstructured":"Yelam, A., Wu, K., Guo, Z., Yang, S., Shashidhara, R., Xu, W., Novakovic, S., Snoeren, A. C., and Keeton, K. PageFlex: Flexible and efficient user-space delegation of linux paging policies with eBPF. In 2025 USENIX Annual Technical Conference (USENIX ATC 25) (2025), pp. 291--306."},{"key":"e_1_3_2_1_96_1","first-page":"375","volume-title":"USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhong Y.","year":"2022","unstructured":"Zhong, Y., Li, H., Wu, Y. J., Zarkadas, I., Tao, J., Mesterhazy, E., Makris, M., Yang, J., Tai, A., Stutsman, R., et al. XRP: In-Kernel Storage Functions with eBPF. In USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2022), pp. 375--393."},{"key":"e_1_3_2_1_97_1","volume-title":"bpf: Relax allowlist for css_task iter. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=3091b667498b0a212e760e1033e5f9b8c33a948f. (Oct","author":"Zhou C.","year":"2023","unstructured":"Zhou, C. bpf: Relax allowlist for css_task iter. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=3091b667498b0a212e760e1033e5f9b8c33a948f. (Oct. 2023)."},{"key":"e_1_3_2_1_98_1","first-page":"1391","volume-title":"20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23)","author":"Zhou Y.","year":"2023","unstructured":"Zhou, Y., Wang, Z., Dharanipragada, S., and Yu, M. Electrode: Accelerating distributed protocols with eBPF. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23) (2023), pp. 1391--1407."},{"key":"e_1_3_2_1_99_1","volume-title":"21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24)","author":"Zhou Y.","year":"2024","unstructured":"Zhou, Y., Xiang, X., Kiley, M., Dharanipragada, S., and Yu, M. DINT: Fast In-Kernel distributed transactions with eBPF. In 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24) (Santa Clara, CA, Apr. 2024), USENIX Association, pp. 401--417."},{"key":"e_1_3_2_1_100_1","volume-title":"bpf: correct loop detection for iterators convergence. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2a0992829ea3864939d917a5c7b48be6629c6217. (Oct","author":"Zingerman E.","year":"2023","unstructured":"Zingerman, E. bpf: correct loop detection for iterators convergence. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2a0992829ea3864939d917a5c7b48be6629c6217. (Oct. 2023)."},{"key":"e_1_3_2_1_101_1","volume-title":"bpf: exact states comparison for iterator convergence checks. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2793a8b015f7f1caadb9bce9c63dc659f7522676. (Oct","author":"Zingerman E.","year":"2023","unstructured":"Zingerman, E. bpf: exact states comparison for iterator convergence checks. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=2793a8b015f7f1caadb9bce9c63dc659f7522676. (Oct. 2023)."},{"key":"e_1_3_2_1_102_1","volume-title":"bpf: Fix for use-after-free bug in inline_bpf_loop. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=fb4e3b33e3e7f13befdf9ee232e34818c6cc5fb9. (Jun","author":"Zingerman E.","year":"2022","unstructured":"Zingerman, E. bpf: Fix for use-after-free bug in inline_bpf_loop. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=fb4e3b33e3e7f13befdf9ee232e34818c6cc5fb9. (Jun. 2022)."}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Seoul Republic of Korea","acronym":"SOSP '25"},"container-title":["Proceedings of the 13th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3764860.3768336","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768336","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768336","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:20:12Z","timestamp":1763054412000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764860.3768336"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,13]]},"references-count":102,"alternative-id":["10.1145\/3764860.3768336","10.1145\/3764860"],"URL":"https:\/\/doi.org\/10.1145\/3764860.3768336","relation":{},"subject":[],"published":{"date-parts":[[2025,10,13]]},"assertion":[{"value":"2025-10-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}