{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T15:55:01Z","timestamp":1775145301652,"version":"3.50.1"},"publisher-location":"Cham","reference-count":74,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377082","type":"print"},{"value":"9783031377099","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper proposes an automated method to check the correctness of range analysis used in the Linux kernel \u2019s eBPF verifier. We provide the specification of soundness for range analysis performed by the eBPF verifier. We automatically generate verification conditions that encode the operation of the eBPF verifier directly from the Linux kernel \u2019s C source code and check it against our specification. When we discover instances where the eBPF verifier is unsound, we propose a method to generate an eBPF program that demonstrates the mismatch between the abstract and the concrete semantics. Our prototype automatically checks the soundness of 16 versions of the eBPF verifier in the Linux kernel versions ranging from 4.14 to 5.19. In this process, we have discovered new bugs in older versions and proved the soundness of range analysis in the latest version of the Linux kernel.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_12","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"226-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["Verifying the\u00a0Verifier: eBPF Range Analysis Verification"],"prefix":"10.1007","author":[{"given":"Harishankar","family":"Vishwanathan","sequence":"first","affiliation":[]},{"given":"Matan","family":"Shachnai","sequence":"additional","affiliation":[]},{"given":"Srinivas","family":"Narayana","sequence":"additional","affiliation":[]},{"given":"Santosh","family":"Nagarakatte","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"12_CR1","unstructured":"bpf: fix incorrect sign extension in check_alu_op(). Accessed 14 Jan 2020. https:\/\/github.com\/torvalds\/linux\/commit\/95a762e2c8c942780948091f8f2a4f32fce1ac6f"},{"key":"12_CR2","unstructured":"bpf, x32: Fix bug with ALU64 LSH, RSH, ARSH BPF_X shift by 0. Accessed 14 Apr 2021. https:\/\/github.com\/torvalds\/linux\/commit\/68a8357ec15bdce55266e9fba8b8b3b8143fa7d2"},{"key":"12_CR3","unstructured":"CVE-2017-16996 Mishandling of register truncation. Accessed 22 Jan 2023. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-16996"},{"key":"12_CR4","unstructured":"CVE-2017-17852 Mishandling of 32-bit ALU ops. Accessed 22 Jan 2023. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-17852"},{"key":"12_CR5","unstructured":"CVE-2017-17853 Mishandling of 32-bit ALU ops. Accessed 22 Jan 2023. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-17853"},{"key":"12_CR6","unstructured":"CVE-2017-17864 Mishandled comparison between pointer and unknown data types. Accessed 14 Jan 2020. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-17864"},{"key":"12_CR7","unstructured":"CVE-2018-18445 Mishandling of 32-bit RSH op. Accessed 22 Jan 2023. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2018-18445"},{"key":"12_CR8","unstructured":"CVE-2020-8835 Mishandling of bounds tracking for 32-bit JMPs. Accessed 22 Jan 2023. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2020-8835"},{"key":"12_CR9","unstructured":"CVE-2021-3490 The eBPF ALU32 bounds tracking for bitwise ops (AND, OR and XOR) in the Linux kernel did not properly update 32-bit bounds. Accessed 22 Jan 2023. CVE-2021-3490"},{"key":"12_CR10","unstructured":"Facebook\u2019s Katran load balancer: Kernel XDP program. Accessed 14 Jan 2020. https:\/\/github.com\/facebookincubator\/katran\/blob\/master\/katran\/lib\/bpf\/balancer_kern.c"},{"key":"12_CR11","unstructured":"Linux BPF verifier. Accessed 14 Jan 2020. https:\/\/github.com\/torvalds\/linux\/blob\/master\/kernel\/bpf\/verifier.c"},{"key":"12_CR12","unstructured":"Netconf 2018 day 1. Accessed 19 Jan 2020. https:\/\/lwn.net\/Articles\/757201\/"},{"key":"12_CR13","unstructured":"BPF instruction set. Accessed 14 Jan 2020. https:\/\/github.com\/iovisor\/bpf-docs\/blob\/master\/eBPF.md (2017)"},{"key":"12_CR14","unstructured":"Linux verifier\u2019s abstract u64 addition (kernel v6.0). Accessed 08 Nov 2022. https:\/\/github.com\/torvalds\/linux\/blob\/v6.0\/kernel\/bpf\/verifier.c#L8333 (2022)"},{"key":"12_CR15","unstructured":"Linux verifier\u2019s abstract u64 bitwise AND (kernel v6.0). Accessed 08 Nov 2022. https:\/\/github.com\/torvalds\/linux\/blob\/v6.0\/kernel\/bpf\/verifier.c#L8513 (2022)"},{"key":"12_CR16","unstructured":"Linux verifier\u2019s top-level function for value-tracking in scalar for alu instructions (kernel v6.0): adjust_scalar_min_max_vals: Accessed 27 Jan 2023. https:\/\/github.com\/torvalds\/linux\/blob\/90aaef4e35c4a74b0f1593d06e39eda867ef13d3\/kernel\/bpf\/verifier.c#L10524 (2023)"},{"key":"12_CR17","unstructured":"LLVM\u2019s MemorySSA. Accessed 27 Jan 2023. https:\/\/llvm.org\/docs\/MemorySSA.html (2023)"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Verifying the Verifier: eBPF Range Analysis Verification (2023). https:\/\/doi.org\/10.5281\/zenodo.7931901","DOI":"10.5281\/zenodo.7931901"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84\u201393 (2018). https:\/\/doi.org\/10.1145\/3208071","DOI":"10.1145\/3208071"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. SIGOPS Oper. Syst. Rev. 40(5), 394\u2013403 (2006). https:\/\/doi.org\/10.1145\/1168917.1168906","DOI":"10.1145\/1168917.1168906"},{"key":"12_CR21","unstructured":"Bhat, S., Shacham, H.: Formal verification of the linux kernel eBPF verifier range analysis. Accessed 27 Jan 2023. https:\/\/sanjit-bhat.github.io\/assets\/pdf\/ebpf-verifier-range-analysis22.pdf (2022)"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"12_CR23","unstructured":"Borkmann, D.: bpf: Fix scalar32_min_max_or bounds tracking. Accessed 6 Nov 2022. https:\/\/github.com\/torvalds\/linux\/commit\/5b9fbeb75b6a98955f628e205ac26689bcb1383e (2020)"},{"key":"12_CR24","unstructured":"Borkmann, D.: bpf: Undo incorrect __reg_bound_offset32 handling. Accessed 6 Nov 2022. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/netdev\/net-next.git\/commit\/?id=f2d67fec0b43edce8c416101cdc52e71145b5fef (2020)"},{"key":"12_CR25","unstructured":"Borkmann, D.: bpf: Fix alu32 const subreg bound tracking on bitwise operations. Accessed 6 Nov 2022. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/bpf\/bpf.git\/commit\/?id=049c4e13714ecbca567b4d5f6d563f05d431c80e (2021)"},{"key":"12_CR26","unstructured":"Borkmann, D.: bpf: Fix signed_sub, add32_overflows type handling. Accessed 6 Nov 2022. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=bc895e8b2a64e502fbba72748d59618272052a8b (2021)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. Electr. Proceed. Theoret. Comput. Sci. 129, 325\u2013336 (2013). https:\/\/doi.org\/10.4204\/eptcs.129.19","DOI":"10.4204\/eptcs.129.19"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). In: Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL1994), pp. 95\u2013112 (1994). https:\/\/doi.org\/10.1109\/ICCL.1994.288389","DOI":"10.1109\/ICCL.1994.288389"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-44577-3_10","volume-title":"Informatics","author":"P Cousot","year":"2001","unstructured":"Cousot, P.: Abstract interpretation based formal methods and future challenges. In: Wilhelm, R. (ed.) Informatics. LNCS, vol. 2000, pp. 138\u2013156. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44577-3_10"},{"key":"12_CR31","unstructured":"Cousot, P.: Lecture 13 notes: MIT 16.399, abstract interpretation. Accessed 16 Apr 2021. http:\/\/web.mit.edu\/afs\/athena.mit.edu\/course\/16\/16.399\/www\/lecture_13-abstraction1\/Cousot_MIT_2005_Course_13_4-1.pdf (2005)"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, Paris, France, pp. 106\u2013130. Dunod (1976)","DOI":"10.1145\/390018.808314"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. POPL 1977, Association for Computing Machinery, New York, NY, USA (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. p. 269\u2013282. POPL 1979, Association for Computing Machinery, New York, NY, USA (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"12_CR35","unstructured":"Cree, E.: bpf\/verifier: fix bounds calculation on BPF_RSH. Accessed 6 Nov 2022. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=4374f256ce8182019353c0c639bb8d0695b4c941 (2017)"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"12_CR37","unstructured":"Duplyakin, D., et al.: The design and operation of cloudLab. In: Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference, pp. 1\u201314. USENIX ATC 2019, USENIX Association, USA (2019)"},{"key":"12_CR38","unstructured":"Fabre, A.: L4Drop: XDP DDoS mitigations. Accessed 19 Jan 2020. https:\/\/blog.cloudflare.com\/l4drop-xdp-ebpf-based-ddos-mitigations\/"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Gershuni, E., et al.: Simple and precise static analysis of untrusted Linux Kernel extensions. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1069\u20131084. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3314221.3314590","DOI":"10.1145\/3314221.3314590"},{"key":"12_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-56287-7_95","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P Granger","year":"1992","unstructured":"Granger, P.: Improving the results of static analyses of programs by local decreasing iterations. In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 68\u201379. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-56287-7_95"},{"key":"12_CR41","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. SIGPLAN Not. 46(6), 62\u201373 (2011). https:\/\/doi.org\/10.1145\/1993316.1993506","DOI":"10.1145\/1993316.1993506"},{"key":"12_CR42","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 343\u2013361. Springer International Publishing, Cham (2015)"},{"key":"12_CR43","unstructured":"Horn, J.: Arbitrary read+write via incorrect range tracking in ebpf. Accessed 19 Jan 2020. https:\/\/bugs.chromium.org\/p\/project-zero\/issues\/detail?id=1454"},{"key":"12_CR44","unstructured":"Horn, J.: BPF: fix 32-bit ALU op verification. Accessed 6 Nov 2022. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=468f6eafa6c44cb2c5d8aad35e12f06c240a812a (2017)"},{"key":"12_CR45","unstructured":"Horn, J.: bpf: 32-bit RSH verification must truncate input before the ALU op. Accessed 6 Nov 2022. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=b799207e1e1816b09e7a5920fbb2d5fcf6edd681 (2018)"},{"key":"12_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"12_CR47","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.: Llvm: a compilation framework for lifelong program analysis & transformation. In: International symposium on code generation and optimization, 2004. CGO 2004, pp. 75\u201386. IEEE (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"12_CR48","unstructured":"Linux eBPF maintainers: bounds syncing for abstract registers. Accessed 31 Jan 2023. https:\/\/github.com\/torvalds\/linux\/blob\/v6.0\/kernel\/bpf\/verifier.c#L1565 (2023)"},{"key":"12_CR49","unstructured":"Linux eBPF maintainers: using bounds syncing at end of alu operations. Accessed 31 Jan 2023. https:\/\/github.com\/torvalds\/linux\/blob\/v6.0\/kernel\/bpf\/verifier.c#L9016 (2023)"},{"key":"12_CR50","unstructured":"Lucas Leong: ZDI-20-1440: An incorrect calculation bug in the Linux Kernel eBPF verifier. Accessed 22 Jan 2023. https:\/\/www.zerodayinitiative.com\/blog\/2021\/1\/18\/zdi-20-1440-an-incorrect-calculation-bug-in-the-linux-kernel-ebpf-verifier"},{"key":"12_CR51","unstructured":"Manfred Paul: CVE-2020-8835: Linux kernel privilege escalation via improper eBPF program verification. Accessed 22 Jan 2023. https:\/\/www.zerodayinitiative.com\/blog\/2020\/4\/8\/cve-2020-8835-linux-kernel-privilege-escalation-via-improper-ebpf-program-verification"},{"key":"12_CR52","doi-asserted-by":"publisher","unstructured":"Massalin, H.: Superoptimizer: A look at the smallest program. In: Proceedings of the Second International Conference on Architectual Support for Programming Languages and Operating Systems, pp. 122\u2013126. ASPLOS II, Association for Computing Machinery, New York, NY, USA (1987). https:\/\/doi.org\/10.1145\/36206.36194","DOI":"10.1145\/36206.36194"},{"key":"12_CR53","unstructured":"McCanne, S., Jacobson, V.: The BSD packet filter: a new architecture for user-level packet capture. In: USENIX Winter 1993 Conference (USENIX Winter 1993 Conference). USENIX Association, San Diego, CA (1993). https:\/\/www.usenix.org\/conference\/usenix-winter-1993-conference\/bsd-packet-filter-new-architecture-user-level-packet"},{"key":"12_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146\u2013161. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_12"},{"key":"12_CR55","unstructured":"Min\u00e9, A.: Abstract domains for bit-level machine integer and floating-point operations. In: WING2012 - 4th International Workshop on invariant Generation, p. 16. Manchester, United Kingdom (2012). https:\/\/hal.science\/hal-00748094"},{"key":"12_CR56","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends\u00ae Programm. Lang. 4(3\u20134), 120\u2013372 (2017). https:\/\/doi.org\/10.1561\/2500000034","DOI":"10.1561\/2500000034"},{"key":"12_CR57","doi-asserted-by":"publisher","unstructured":"Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: Proceedings of the 7th ACM & IEEE international conference on Embedded software, pp. 30\u201336 (2007). https:\/\/doi.org\/10.1145\/1289927.1289937","DOI":"10.1145\/1289927.1289937"},{"key":"12_CR58","doi-asserted-by":"publisher","unstructured":"Mukherjee, M., Kant, P., Liu, Z., Regehr, J.: Dataflow-based pruning for speeding up superoptimization. Proc. ACM Program. Lang. 4, 3428245 (OOPSLA) (2020). https:\/\/doi.org\/10.1145\/3428245","DOI":"10.1145\/3428245"},{"key":"12_CR59","doi-asserted-by":"publisher","unstructured":"Nelson, L., Bornholt, J., Gu, R., Baumann, A., Torlak, E., Wang, X.: Scaling symbolic evaluation for automated verification of systems code with serval. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles, pp. 225\u2013242. SOSP 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3341301.3359641","DOI":"10.1145\/3341301.3359641"},{"key":"12_CR60","unstructured":"Nelson, L., Van Geffen, J., Torlak, E., 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. OSDI2020, USENIX Association, USA (2020)"},{"key":"12_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-030-94583-1_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Onderka","year":"2022","unstructured":"Onderka, J., Ratschan, S.: Fast three-valued abstract bit-vector arithmetic. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 242\u2013262. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_12"},{"key":"12_CR62","unstructured":"Palmiotti, V.: Kernel pwning with eBPF: a love story. Accessed 31 August 2021. https:\/\/www.graplsecurity.com\/post\/kernel-pwning-with-ebpf-a-love-story"},{"key":"12_CR63","doi-asserted-by":"publisher","unstructured":"Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Scaling up superoptimization. In: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 297\u2013310. ASPLOS 2016, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2872362.2872387","DOI":"10.1145\/2872362.2872387"},{"key":"12_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7"},{"key":"12_CR65","doi-asserted-by":"publisher","unstructured":"Regehr, J., Duongsaa, U.: Deriving abstract transfer functions for analyzing embedded software. In: Proceedings of the 2006 ACM SIGPLAN\/SIGBED Conference on Language, Compilers, and Tool Support for Embedded Systems, pp. 34\u201343. LCTES 2006, Association for Computing Machinery, New York, NY, USA (2006). https:\/\/doi.org\/10.1145\/1134650.1134657","DOI":"10.1145\/1134650.1134657"},{"key":"12_CR66","unstructured":"Rick Larabee: eBPF and Analysis of the get-rekt-linux-hardened.c Exploit for CVE-2017-16995. Accessed 22 Jan 2023. https:\/\/ricklarabee.blogspot.com\/2018\/07\/ebpf-and-analysis-of-get-rekt-linux.html"},{"key":"12_CR67","doi-asserted-by":"publisher","unstructured":"Sasnauskas, R., Chen, Y., Collingbourne, P., Ketema, J., Taneja, J., Regehr, J.: Souper: a synthesizing superoptimizer. CoRR abs\/1711.04422 (2017). https:\/\/doi.org\/10.48550\/arXiv.1711.04422","DOI":"10.48550\/arXiv.1711.04422"},{"key":"12_CR68","doi-asserted-by":"publisher","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 46\u201359. POPL 2017, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3009837.3009885","DOI":"10.1145\/3009837.3009885"},{"key":"12_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-030-53291-8_29","volume-title":"Computer Aided Verification","author":"J Van Geffen","year":"2020","unstructured":"Van Geffen, J., Nelson, L., Dillig, I., Wang, X., Torlak, E.: Synthesizing JIT compilers for in-Kernel DSLs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 564\u2013586. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_29"},{"key":"12_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-61739-6_53","volume-title":"Static Analysis","author":"A Venet","year":"1996","unstructured":"Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 366\u2013382. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61739-6_53"},{"key":"12_CR71","doi-asserted-by":"publisher","unstructured":"Vishwanathan, H., Shachnai, M., Narayana, S., Nagarakatte, S.: Sound, precise, and fast abstract interpretation with tristate numbers. In: Proceedings of the 20th IEEE\/ACM International Symposium on Code Generation and Optimization, pp. 254\u2013265. CGO 2022, IEEE Press (2022). https:\/\/doi.org\/10.1109\/CGO53902.2022.9741267","DOI":"10.1109\/CGO53902.2022.9741267"},{"key":"12_CR72","doi-asserted-by":"crossref","unstructured":"Vishwanathan, H., Shachnai, M., Narayana, S., Nagarakatte, S.: Agni: verifying the Verifier (eBPF Range Analysis Verification). Accessed 29 May 2023. https:\/\/github.com\/bpfverif\/ebpf-range-analysis-verification-cav23 (2023)","DOI":"10.1007\/978-3-031-37709-9_12"},{"key":"12_CR73","unstructured":"Wang, X., Lazar, D., Zeldovich, N., Chlipala, A., Tatlock, Z.: Jitk: a trustworthy in-Kernel interpreter infrastructure. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, pp. 33\u201347. OSDI2014, USENIX Association, USA (2014)"},{"key":"12_CR74","doi-asserted-by":"publisher","unstructured":"Xu, Q., Wong, M.D., Wagle, T., Narayana, S., Sivaraman, A.: Synthesizing safe and efficient kernel extensions for packet processing. In: Proceedings of the 2021 ACM SIGCOMM 2021 Conference, pp. 50\u201364. SIGCOMM 2021, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3452296.3472929","DOI":"10.1145\/3452296.3472929"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37709-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,17]],"date-time":"2023-12-17T05:03:09Z","timestamp":1702789389000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}