{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T18:35:26Z","timestamp":1763058926310,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,6,22]],"date-time":"2023-06-22T00:00:00Z","timestamp":1687392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-2236966","CNS-1956007"],"award-info":[{"award-number":["CNS-2236966","CNS-1956007"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,6,22]]},"DOI":"10.1145\/3593856.3595892","type":"proceedings-article","created":{"date-parts":[[2023,6,22]],"date-time":"2023-06-22T22:20:41Z","timestamp":1687472441000},"page":"150-157","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Kernel extension verification is untenable"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-0837-4677","authenticated-orcid":false,"given":"Jinghao","family":"Jia","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Illinois Urbana-Champaign, Urbana, IL, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5160-0362","authenticated-orcid":false,"given":"Raj","family":"Sahu","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Virginia Tech, Blacksburg, VA, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1310-547X","authenticated-orcid":false,"given":"Adam","family":"Oswald","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Virginia Tech, Blacksburg, VA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1537-0525","authenticated-orcid":false,"given":"Dan","family":"Williams","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Virginia Tech, Blacksburg, VA, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5000-6393","authenticated-orcid":false,"given":"Michael V.","family":"Le","sequence":"additional","affiliation":[{"name":"IBM Research, Yorktown Heights, NY, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4443-8170","authenticated-orcid":false,"given":"Tianyin","family":"Xu","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, United States of America"}]}],"member":"320","published-online":{"date-parts":[[2023,6,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"CVE-2021-29154. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2021-29154."},{"key":"e_1_3_2_1_2_1","unstructured":"CVE-2021-31440. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2021-31440."},{"key":"e_1_3_2_1_3_1","unstructured":"CVE-2021-45402. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2021-45402."},{"key":"e_1_3_2_1_4_1","unstructured":"CVE-2022-23222. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2022-23222."},{"key":"e_1_3_2_1_5_1","unstructured":"CVE-2022-2785. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2022-2785."},{"key":"e_1_3_2_1_6_1","unstructured":"ERC Project \"RustBelt\". https:\/\/plv.mpi-sws.org\/rustbelt\/."},{"key":"e_1_3_2_1_7_1","unstructured":"RAII - Rust By Example. https:\/\/doc.rust-lang.org\/rust-by-example\/scope\/raii.html."},{"key":"e_1_3_2_1_8_1","unstructured":"Rust for Linux - GitHub. https:\/\/github.com\/Rust-for-Linux."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102980.3103006"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224077"},{"key":"e_1_3_2_1_11_1","volume-title":"May","author":"Bhat S.","year":"2022","unstructured":"Bhat, S., and Shacham, H. Formal Verification of the Linux Kernel eBPF Verifier Range Analysis. https:\/\/sanjit-bhat.github.io\/assets\/pdf\/ebpf-verifier-range-analysis22.pdf, May 2022."},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI'20)","author":"Boos K.","year":"2020","unstructured":"Boos, K., Liyanage, N., Ijaz, R., and Zhong, L. Theseus: An Experiment in Operating System Structure and State Management. In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI'20) (Nov. 2020)."},{"key":"e_1_3_2_1_13_1","volume-title":"Dec.","author":"Borkmann D.","year":"2021","unstructured":"Borkmann, D. bpf: Fix kernel address leakage in atomic cmpxchg's r0 aux reg. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=a82fe085f344ef20b452cd5f481010ff96b5c4cd, Dec. 2021."},{"key":"e_1_3_2_1_14_1","volume-title":"Dec.","author":"Borkmann D.","year":"2021","unstructured":"Borkmann, D. bpf: Fix kernel address leakage in atomic fetch. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=7d3baf0afa3aa9102d6a521a8e4c41888bb79882, Dec. 2021."},{"key":"e_1_3_2_1_15_1","volume-title":"July","author":"Borkmann D.","year":"2022","unstructured":"Borkmann, D. bpf: Fix insufficient bounds propagation from adjust_scalar_min_max_vals. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=3844d153a41adea718202c10ae91dc96b37453b5, July 2022."},{"key":"e_1_3_2_1_16_1","volume-title":"May","author":"Corbet J.","year":"2021","unstructured":"Corbet, J. Calling kernel functions from BPF. https:\/\/lwn.net\/Articles\/856005\/, May 2021."},{"key":"e_1_3_2_1_17_1","volume-title":"June","author":"Corbet J.","year":"2022","unstructured":"Corbet, J. A BPF-specific memory allocator. https:\/\/lwn.net\/Articles\/899274\/, June 2022."},{"key":"e_1_3_2_1_18_1","volume-title":"July","author":"Corbet J.","year":"2022","unstructured":"Corbet, J. The BPF panic function. https:\/\/lwn.net\/Articles\/901284\/, July 2022."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314590"},{"key":"e_1_3_2_1_20_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_21_1","unstructured":"Gregg B. Linux Extended BPF (eBPF) Tracing Tools. https:\/\/www.brendangregg.com\/ebpf.html."},{"key":"e_1_3_2_1_22_1","volume-title":"Oct.","author":"Gupta P.","year":"2021","unstructured":"Gupta, P. bpf: Disallow unprivileged bpf by default. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=8a03e56b253e9691c90bc52ca199323d71b96204, Oct. 2021."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281443"},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI'13)","author":"Howell J.","year":"2013","unstructured":"Howell, J., Parno, B., and Douceur, J. R. Embassies: Radically Refactoring the Web. In Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI'13) (Apr. 2013)."},{"key":"e_1_3_2_1_26_1","volume-title":"Programmable System Call Security with eBPF. arXiv:2302.10366 (Feb","author":"Jia J.","year":"2023","unstructured":"Jia, J., Zhu, Y., Williams, D., Arcangeli, A., Canella, C., Franke, H., Feldman-Fitzthum, T., Skarlatos, D., Gruss, D., and Xu, T. Programmable System Call Security with eBPF. arXiv:2302.10366 (Feb. 2023)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492321.3519582"},{"key":"e_1_3_2_1_28_1","volume-title":"Sept.","author":"Kroah-Hartman G.","year":"2019","unstructured":"Kroah-Hartman, G. Cves are dead, long live the cve! https:\/\/kernel-recipes.org\/en\/2019\/talks\/cves-are-dead-long-live-the-cve\/, Sept. 2019."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492321.3519562"},{"key":"e_1_3_2_1_30_1","first-page":"1","author":"Li H.","year":"2022","unstructured":"Li, H., Gu, J., Xia, Y., Zang, B., and Chen, H. Memory Isolation Mechanism of eBPF Based on PKS Hardware Feature. In Journal of Software (China) (2022), pp. 1--18.","journal-title":"BPF Based on PKS Hardware Feature. In Journal of Software (China) ("},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458336.3465277"},{"key":"e_1_3_2_1_32_1","volume-title":"Nov.","author":"Li Y.","year":"2022","unstructured":"Li, Y. bpf: Fix wrong reg type conversion in release_reference(). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=f1db20814af532f85e091231223e5e4818e8464b, Nov. 2022."},{"key":"e_1_3_2_1_33_1","volume-title":"MOAT: Towards Safe BPF Kernel Extension. arXiv:2301.13421 (Mar","author":"Lu H.","year":"2023","unstructured":"Lu, H., Wang, S., Wu, Y., He, W., and Zhang, F. MOAT: Towards Safe BPF Kernel Extension. arXiv:2301.13421 (Mar. 2023)."},{"key":"e_1_3_2_1_34_1","volume-title":"Mar.","author":"Marchevsky D.","year":"2021","unstructured":"Marchevsky, D. bpf: Refcount task stack in bpf_get_task_stack. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=06ab134ce8ecfa5a69e850f88f81c8a4c3fa91df, Mar. 2021."},{"key":"e_1_3_2_1_35_1","volume-title":"June","author":"Maxwell J.","year":"2022","unstructured":"Maxwell, J. bpf: Fix request_sock leak in sk lookup helpers. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=3046a827316c0e55fc563b4fb78c93b9ca5c7c37, June 2022."},{"key":"e_1_3_2_1_36_1","volume-title":"July","author":"Nakryiko A.","year":"2022","unstructured":"Nakryiko, A. bpf: fix potential 32-bit overflow when accessing ARRAY map element. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=87ac0d600943994444e24382a87aa19acc4cd3d4, July 2022."},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (Nov.","author":"Narayanan V.","year":"2020","unstructured":"Narayanan, V., Huang, T., Detweiler, D., Appel, D., Li, Z., Zellweger, G., and Burtsev, A. RedLeaf: Isolation and Communication in a Safe Operating System. In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (Nov. 2020)."},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI'20)","author":"Nelson L.","year":"2020","unstructured":"Nelson, L., Van Geffen, J., Torlak, E., and Wang, X. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI'20) (Nov. 2020)."},{"key":"e_1_3_2_1_39_1","volume-title":"Linux Plumbers Conference (Sept.","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 (Sept. 2021)."},{"key":"e_1_3_2_1_40_1","volume-title":"Automatic Rust verification tools","author":"Reid A.","year":"2021","unstructured":"Reid, A. Automatic Rust verification tools (2021). https:\/\/alastairreid.github.io\/automatic-rust-verification-tools-2021\/, June 2021."},{"key":"e_1_3_2_1_41_1","volume-title":"Fuzzing for ebpf jit bugs in the linux kernel. https:\/\/scannell.io\/posts\/ebpf-fuzzing\/","author":"Scannell S.","year":"2021","unstructured":"Scannell, S. Fuzzing for ebpf jit bugs in the linux kernel. https:\/\/scannell.io\/posts\/ebpf-fuzzing\/, 2021."},{"key":"e_1_3_2_1_42_1","volume-title":"Jan.","author":"Singh K.","year":"2021","unstructured":"Singh, K. bpf: Local storage helpers should check nullness of owner ptr passed. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=1a9c72ad4c26821e215a396167c14959cf24a7f1, Jan. 2021."},{"key":"e_1_3_2_1_43_1","volume-title":"Sept.","author":"Singh K.","year":"2022","unstructured":"Singh, K. BPF Signing and IMA integration. https:\/\/lpc.events\/event\/16\/contributions\/1357\/, Sept. 2022."},{"key":"e_1_3_2_1_44_1","volume-title":"May","author":"Starovoitov A.","year":"2015","unstructured":"Starovoitov, A. bpf: allow bpf programs to tail-call other bpf programs. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=04fd61ab36ec065e194ab5e74ae34a5240d992bb, May 2015."},{"key":"e_1_3_2_1_45_1","volume-title":"Dec.","author":"Starovoitov A.","year":"2017","unstructured":"Starovoitov, A. bpf: introduce function calls (verification). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=f4d7e40a5b7157e1329c3c5b10f60d8289fc2941, Dec. 2017."},{"key":"e_1_3_2_1_46_1","volume-title":"May","author":"Starovoitov A.","year":"2018","unstructured":"Starovoitov, A. bpf: Prevent memory disambiguation attack. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=af86ca4e3088fe5eacf2f7e58c01fa68ca067672, May 2018."},{"key":"e_1_3_2_1_47_1","volume-title":"Jan.","author":"Starovoitov A.","year":"2018","unstructured":"Starovoitov, A. bpf: prevent out-of-bounds speculation. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=b2157399cc9898260d6031c5bfe45fe137c1fbe7, Jan. 2018."},{"key":"e_1_3_2_1_48_1","volume-title":"Jan.","author":"Starovoitov A.","year":"2019","unstructured":"Starovoitov, A. bpf: introduce bpf_spin_lock. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/?id=d83525ca62cf8ebe3271d14c36fb900c294274a2, Jan. 2019."},{"key":"e_1_3_2_1_49_1","volume-title":"July","author":"Vernet D.","year":"2022","unstructured":"Vernet, D. Long-lived kernel pointers in BPF. https:\/\/lwn.net\/Articles\/900749\/, July 2022."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO53902.2022.9741267"},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14)","author":"Wang X.","year":"2014","unstructured":"Wang, X., Lazar, D., Zeldovich, N., Chlipala, A., and Tatlock., Z. Jitk: A trustworthy in-kernel interpreter infrastructure. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14) (Oct. 2014)."},{"key":"e_1_3_2_1_52_1","volume-title":"Proceedings of 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI'22)","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., and Cidon, A. XRP: In-Kernel storage functions with eBPF. In Proceedings of 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI'22) (July 2022)."},{"key":"e_1_3_2_1_53_1","volume-title":"Proceedings of the 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 Proceedings of the 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI'23) (Apr. 2023)."},{"key":"e_1_3_2_1_54_1","volume-title":"June","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\/stable\/linux.git\/commit\/?id=fb4e3b33e3e7f13befdf9ee232e34818c6cc5fb9, June 2022."}],"event":{"name":"HotOS '23: 19th Workshop on Hot Topics in Operating Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Providence RI USA","acronym":"HOTOS '23"},"container-title":["Proceedings of the 19th Workshop on Hot Topics in Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3593856.3595892","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3593856.3595892","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3593856.3595892","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:50Z","timestamp":1750178870000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3593856.3595892"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,22]]},"references-count":53,"alternative-id":["10.1145\/3593856.3595892","10.1145\/3593856"],"URL":"https:\/\/doi.org\/10.1145\/3593856.3595892","relation":{},"subject":[],"published":{"date-parts":[[2023,6,22]]},"assertion":[{"value":"2023-06-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}