{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:42:52Z","timestamp":1760056972788,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,8]]},"DOI":"10.1145\/3748355.3748368","type":"proceedings-article","created":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T13:47:07Z","timestamp":1755611227000},"page":"55-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Kernel Extension DSLs Should Be Verifier-Safe!"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-0416-1203","authenticated-orcid":false,"given":"Franco","family":"Solleza","sequence":"first","affiliation":[{"name":"Brown University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4046-534X","authenticated-orcid":false,"given":"Justus","family":"Adam","sequence":"additional","affiliation":[{"name":"Brown University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6626-141X","authenticated-orcid":false,"given":"Akshay","family":"Narayan","sequence":"additional","affiliation":[{"name":"Brown University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5066-6332","authenticated-orcid":false,"given":"Malte","family":"Schwarzkopf","sequence":"additional","affiliation":[{"name":"Brown University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8544-0982","authenticated-orcid":false,"given":"Andrew","family":"Crotty","sequence":"additional","affiliation":[{"name":"Northwestern University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0416-7022","authenticated-orcid":false,"given":"Nesime","family":"Tatbul","sequence":"additional","affiliation":[{"name":"MIT & Intel"}]}],"member":"320","published-online":{"date-parts":[[2025,9,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Soheil Hassas Yeganeh, and Van Jacobson","author":"Cardwell Neal","year":"2016","unstructured":"Neal Cardwell, Yuchung Cheng, C. Stephen Gunn, Soheil Hassas Yeganeh, and Van Jacobson. 2016. BBR: Congestion-Based Congestion Control. In ACM Queue."},{"unstructured":"Zhongjie Chen Qingkai Meng ChonLam Lao Yifan Liu Fengyuan Ren Minlan Yu and Yang Zhou. 2025. eTran: Extensible Kernel Transport with eBPF. In NSDI. https:\/\/www.usenix.org\/conference\/nsdi25\/presentation\/chen-zhongjie","key":"e_1_3_2_1_2_1"},{"key":"e_1_3_2_1_3_1","volume-title":"d.]. sched_ext. ([n. d.]). https:\/\/github.com\/sched-ext\/scx Last accessed","author":"Linux","year":"2025","unstructured":"Linux community. [n. d.]. sched_ext. ([n. d.]). https:\/\/github.com\/sched-ext\/scx Last accessed July 16, 2025."},{"key":"e_1_3_2_1_4_1","volume-title":"d.]. eBPF backend. ([n. d.]). https:\/\/p4lang.github.io\/p4c\/ebpf_backend.html Last accessed","author":"C","year":"2025","unstructured":"P4C community. [n. d.]. eBPF backend. ([n. d.]). https:\/\/p4lang.github.io\/p4c\/ebpf_backend.html Last accessed July 16, 2025."},{"unstructured":"Jonathan Corbet. 2023. Reconsidering BPF ABI stability. (2023). https:\/\/lwn.net\/Articles\/921088\/","key":"e_1_3_2_1_5_1"},{"key":"e_1_3_2_1_6_1","volume-title":"Linux Symposium.","author":"Desnoyers Mathieu","year":"2008","unstructured":"Mathieu Desnoyers and Michel Dagenais. 2008. LTTng: Tracing across execution layers, from the Hypervisor to user-space. In Linux Symposium."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/3694715.3695950"},{"unstructured":"The Linux Foundation. 2024. The State of eBPF. (2024).","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation. 487--501","author":"Ghigoff Yoann","year":"2021","unstructured":"Yoann Ghigoff, Julien Sopena, Kahina Lazri, Antoine Blin, and Gilles Muller. 2021. 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. 487--501."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1145\/3544216.3544221"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/3477132.3483542"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 2025 USENIX Annual Technical Conference. 325--342","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. 2025. Rex: Closing the language-verifier gap with safe and usable kernel extensions. In Proceedings of the 2025 USENIX Annual Technical Conference. 325--342."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1145\/3477132.3483548"},{"key":"e_1_3_2_1_14_1","volume-title":"d.]. BPF Design Q & A. ([n. d.]). https:\/\/www.kernel.org\/doc\/html\/latest\/bpf\/bpf_design_QA.html Last accessed","author":"The","year":"2025","unstructured":"The kernel development community. [n. d.]. BPF Design Q & A. ([n. d.]). https:\/\/www.kernel.org\/doc\/html\/latest\/bpf\/bpf_design_QA.html Last accessed January 4, 2025."},{"key":"e_1_3_2_1_15_1","volume-title":"d.]. Kernel crash when loading lttng-tracing module with IBT enabled. https:\/\/bugs.lttng.org\/issues\/1408. ([n. d.]). Last accessed","author":"Khalfella Mohamed","year":"2025","unstructured":"Mohamed Khalfella. [n. d.]. Kernel crash when loading lttng-tracing module with IBT enabled. https:\/\/bugs.lttng.org\/issues\/1408. ([n. d.]). Last accessed May 23, 2025."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1145\/3492321.3519562"},{"unstructured":"Martin KaFai Lau. 2020. bpf: tcp: Support tcp_congestion_-ops in bpf. (2020). https:\/\/github.com\/torvalds\/linux\/commit\/0baf26b0fcd74bbfcef53c5d5e8bad2b99c8d0d2","key":"e_1_3_2_1_17_1"},{"key":"e_1_3_2_1_18_1","volume-title":"bpftrace. (2024). https:\/\/github.com\/bpftrace\/bpftrace Last accessed","author":"Maintainers Trace","year":"2025","unstructured":"BPFTrace Maintainers. 2024. bpftrace. (2024). https:\/\/github.com\/bpftrace\/bpftrace Last accessed January 4, 2025."},{"key":"e_1_3_2_1_19_1","volume-title":"The Dhall configuration language. ([n.d.]). https:\/\/dhall-lang.org Last accessed 22","author":"Maintainers Dhall","year":"2025","unstructured":"Dhall Maintainers. [n.d.]. The Dhall configuration language. ([n.d.]). https:\/\/dhall-lang.org Last accessed 22. May 2025."},{"key":"e_1_3_2_1_20_1","volume-title":"a dynamic tracer for Linux. (2024). https:\/\/github.com\/bpftrace\/bpftrace Last accessed","author":"Maintainers Ply","year":"2025","unstructured":"Ply Maintainers. 2024. Ply, a dynamic tracer for Linux. (2024). https:\/\/github.com\/bpftrace\/bpftrace Last accessed January 4, 2025."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1145\/3371927.3371929"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1109\/TNSM.2021.3055676"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1145\/3503222.3507769"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1145\/3230543.3230553"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.1145\/3555050.3569117"},{"volume-title":"Welcome to osquery. (2024). https:\/\/osquery.readthedocs.io\/en\/stable\/ Last accessed","year":"2025","unstructured":"osquery Maintainers. 2024. Welcome to osquery. (2024). https:\/\/osquery.readthedocs.io\/en\/stable\/ Last accessed January 4, 2025.","key":"e_1_3_2_1_26_1"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation. https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/phothilimthana","author":"Phothilimthana Phitchaya Mangpo","year":"2018","unstructured":"Phitchaya Mangpo Phothilimthana, Ming Liu, Antoine Kaufmann, Simon Peter, Rastislav Bodik, and Thomas Anderson. 2018. Floem: A Programming System for NIC-Accelerated Network Applications. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation. https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/phothilimthana"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1145\/3544216.3544259"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_29_1","DOI":"10.14778\/3485450.3485454"},{"key":"e_1_3_2_1_30_1","volume-title":"The Biennial Conference on Innovative Data Systems Research.","author":"Soul\u00e9 Robert","year":"2025","unstructured":"Robert Soul\u00e9, George Neville-Neil, Stelios Kasouridis, Alex Yuan, Avi Silberschatz, and Peter Alvaro. 2025. OSDB: Exposing the Operating System's Inner Database. In The Biennial Conference on Innovative Data Systems Research."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_31_1","DOI":"10.1145\/3452296.3472914"},{"key":"e_1_3_2_1_32_1","first-page":"751","article-title":"Total Functional Programming","volume":"10","author":"Turner David A.","year":"2004","unstructured":"David A. Turner. 2004. Total Functional Programming. Journal of Universal Computer Science 10, 7 (2004), 751--768.","journal-title":"Journal of Universal Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Harishankar Vishwanathan Matan Shachnai Srinivas Narayana and Santosh Nagarakatte. 2023. Verifying the Verifier: eBPF Range Analysis Verification. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham 226--251.","key":"e_1_3_2_1_33_1","DOI":"10.1007\/978-3-031-37709-9_12"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1145\/3452296.3472929"},{"key":"e_1_3_2_1_35_1","volume-title":"2025 USENIX Annual Technical Conference. 291--306","author":"Yelam Anil","year":"2025","unstructured":"Anil Yelam, Kan Wu, Zhiyuan Guo, Suli Yang, Rajath Shashidhara, Wei Xu, Stanko Novakovi\u0107, Alex C Snoeren, and Kimberly Keeton. 2025. PageFlex: Flexible and Efficient User-space Delegation of Linux Paging Policies with eBPF. In 2025 USENIX Annual Technical Conference. 291--306."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.1145\/3689031.3717497"},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. 375--393","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, et al. 2022. XRP: In-Kernel Storage Functions with eBPF. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. 375--393."}],"event":{"sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"],"acronym":"SIGCOMM '25","name":"SIGCOMM '25: ACM SIGCOMM 2025 Conference","location":"Coimbra Portugal"},"container-title":["Proceedings of the 3rd Workshop on eBPF and Kernel Extensions"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3748355.3748368","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T14:11:29Z","timestamp":1760019089000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3748355.3748368"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,8]]},"references-count":37,"alternative-id":["10.1145\/3748355.3748368","10.1145\/3748355"],"URL":"https:\/\/doi.org\/10.1145\/3748355.3748368","relation":{},"subject":[],"published":{"date-parts":[[2025,9,8]]},"assertion":[{"value":"2025-09-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}