Article

Verifying the Verifier: eBPF Range Analysis Verification

Authors:

Harishankar Vishwanathan,

Matan Shachnai,

Srinivas Narayana,

Santosh NagarakatteAuthors Info & Claims

Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III

Pages 226 - 251

https://doi.org/10.1007/978-3-031-37709-9_12

Published: 17 July 2023 Publication History

Abstract

This paper proposes an automated method to check the correctness of range analysis used in the Linux kernel ’s 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 ’s 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.

References

[1]

bpf: fix incorrect sign extension in check_alu_op(). Accessed 14 Jan 2020. https://github.com/torvalds/linux/commit/95a762e2c8c942780948091f8f2a4f32fce1ac6f

[2]

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

[3]

CVE-2017-16996 Mishandling of register truncation. Accessed 22 Jan 2023. https://nvd.nist.gov/vuln/detail/CVE-2017-16996

[4]

CVE-2017-17852 Mishandling of 32-bit ALU ops. Accessed 22 Jan 2023. https://nvd.nist.gov/vuln/detail/CVE-2017-17852

[5]

CVE-2017-17853 Mishandling of 32-bit ALU ops. Accessed 22 Jan 2023. https://nvd.nist.gov/vuln/detail/CVE-2017-17853

[6]

CVE-2017-17864 Mishandled comparison between pointer and unknown data types. Accessed 14 Jan 2020. https://nvd.nist.gov/vuln/detail/CVE-2017-17864

[7]

CVE-2018-18445 Mishandling of 32-bit RSH op. Accessed 22 Jan 2023. https://nvd.nist.gov/vuln/detail/CVE-2018-18445

[8]

CVE-2020-8835 Mishandling of bounds tracking for 32-bit JMPs. Accessed 22 Jan 2023. https://nvd.nist.gov/vuln/detail/CVE-2020-8835

[9]

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

[10]

Facebook’s Katran load balancer: Kernel XDP program. Accessed 14 Jan 2020. https://github.com/facebookincubator/katran/blob/master/katran/lib/bpf/balancer_kern.c

[11]

Linux BPF verifier. Accessed 14 Jan 2020. https://github.com/torvalds/linux/blob/master/kernel/bpf/verifier.c

[12]

Netconf 2018 day 1. Accessed 19 Jan 2020. https://lwn.net/Articles/757201/

[13]

BPF instruction set. Accessed 14 Jan 2020. https://github.com/iovisor/bpf-docs/blob/master/eBPF.md (2017)

[14]

Linux verifier’s abstract u64 addition (kernel v6.0). Accessed 08 Nov 2022. https://github.com/torvalds/linux/blob/v6.0/kernel/bpf/verifier.c#L8333 (2022)

[15]

Linux verifier’s 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)

[16]

Linux verifier’s 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)

[17]

LLVM’s MemorySSA. Accessed 27 Jan 2023. https://llvm.org/docs/MemorySSA.html (2023)

[18]

Verifying the Verifier: eBPF Range Analysis Verification (2023).

[19]

Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84–93 (2018).

[20]

Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. SIGOPS Oper. Syst. Rev. 40(5), 394–403 (2006).

[21]

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)

[22]

Biere A, Cimatti A, Clarke E, and Zhu Y Cleaveland WR Symbolic model checking without BDDs Tools and Algorithms for the Construction and Analysis of Systems 1999 Heidelberg Springer 193-207

[23]

Borkmann, D.: bpf: Fix scalar32_min_max_or bounds tracking. Accessed 6 Nov 2022. https://github.com/torvalds/linux/commit/5b9fbeb75b6a98955f628e205ac26689bcb1383e (2020)

[24]

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)

[25]

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)

[26]

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)

[27]

Bradley AR Jhala R and Schmidt D SAT-based model checking without unrolling Verification, Model Checking, and Abstract Interpretation 2011 Heidelberg Springer 70-87

[28]

Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. Electr. Proceed. Theoret. Comput. Sci. 129, 325–336 (2013).

[29]

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–112 (1994).

[30]

Cousot P Wilhelm R Abstract interpretation based formal methods and future challenges Informatics 2001 Heidelberg Springer 138-156

[31]

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)

[32]

Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, Paris, France, pp. 106–130. Dunod (1976)

[33]

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–252. POPL 1977, Association for Computing Machinery, New York, NY, USA (1977).

[34]

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–282. POPL 1979, Association for Computing Machinery, New York, NY, USA (1979).

[35]

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)

[36]

de Moura L and Bjørner N Ramakrishnan CR and Rehof J Z3: an efficient SMT solver Tools and Algorithms for the Construction and Analysis of Systems 2008 Heidelberg Springer 337-340

[37]

Duplyakin, D., et al.: The design and operation of cloudLab. In: Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference, pp. 1–14. USENIX ATC 2019, USENIX Association, USA (2019)

[38]

Fabre, A.: L4Drop: XDP DDoS mitigations. Accessed 19 Jan 2020. https://blog.cloudflare.com/l4drop-xdp-ebpf-based-ddos-mitigations/

[39]

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–1084. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019).

[40]

Granger P Shyamasundar R Improving the results of static analyses of programs by local decreasing iterations Foundations of Software Technology and Theoretical Computer Science 1992 Heidelberg Springer 68-79

[41]

Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. SIGPLAN Not. 46(6), 62–73 (2011).

[42]

Gurfinkel A, Kahsai T, Komuravelli A, and Navas JA Kroening D and Păsăreanu CS The SeaHorn verification framework Computer Aided Verification 2015 Cham Springer International Publishing 343-361

[43]

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

[44]

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)

[45]

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)

[46]

Kroening D and Tautschnig M Ábrahám E and Havelund K CBMC – C bounded model checker Tools and Algorithms for the Construction and Analysis of Systems 2014 Heidelberg Springer 389-391

[47]

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–86. IEEE (2004).

[48]

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)

[49]

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)

[50]

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

[51]

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

[52]

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–126. ASPLOS II, Association for Computing Machinery, New York, NY, USA (1987).

[53]

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

[54]

Merz F, Falke S, and Sinz C Joshi R, Müller P, and Podelski A LLBMC: bounded model checking of C and C++ programs using a compiler IR Verified Software: Theories, Tools, Experiments 2012 Heidelberg Springer 146-161

[55]

Miné, 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

[56]

Miné, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends® Programm. Lang. 4(3–4), 120–372 (2017).

[57]

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–36 (2007).

[58]

Mukherjee, M., Kant, P., Liu, Z., Regehr, J.: Dataflow-based pruning for speeding up superoptimization. Proc. ACM Program. Lang. 4, 3428245 (OOPSLA) (2020).

[59]

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–242. SOSP 2019, Association for Computing Machinery, New York, NY, USA (2019).

[60]

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)

[61]

Onderka J and Ratschan S Finkbeiner B and Wies T Fast three-valued abstract bit-vector arithmetic Verification, Model Checking, and Abstract Interpretation 2022 Cham Springer 242-262

[62]

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

[63]

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–310. ASPLOS 2016, Association for Computing Machinery, New York, NY, USA (2016).

[64]

Rakamarić Z and Emmi M Biere A and Bloem R SMACK: decoupling source language details from verifier implementations Computer Aided Verification 2014 Cham Springer 106-113

[65]

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–43. LCTES 2006, Association for Computing Machinery, New York, NY, USA (2006).

[66]

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

[67]

Sasnauskas, R., Chen, Y., Collingbourne, P., Ketema, J., Taneja, J., Regehr, J.: Souper: a synthesizing superoptimizer. CoRR abs/1711.04422 (2017).

[68]

Singh, G., Püschel, M., Vechev, M.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 46–59. POPL 2017, Association for Computing Machinery, New York, NY, USA (2017).

[69]

Van Geffen J, Nelson L, Dillig I, Wang X, and Torlak E Lahiri SK and Wang C Synthesizing JIT compilers for in-Kernel DSLs Computer Aided Verification 2020 Cham Springer 564-586

[70]

Venet A Cousot R and Schmidt DA Abstract cofibered domains: Application to the alias analysis of untyped programs Static Analysis 1996 Heidelberg Springer 366-382

[71]

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–265. CGO 2022, IEEE Press (2022).

[72]

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)

[73]

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–47. OSDI2014, USENIX Association, USA (2014)

[74]

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–64. SIGCOMM 2021, Association for Computing Machinery, New York, NY, USA (2021).

Cited By

Lim SPrasad THan XPasquier TFournaris APalmieri P(2024)SafeBPF: Hardware-assisted Defense-in-depth for eBPF Kernel ExtensionsProceedings of the 2024 on Cloud Computing Security Workshop10.1145/3689938.3694781(80-94)Online publication date: 19-Nov-2024
https://dl.acm.org/doi/10.1145/3689938.3694781
Deokar MMen JCastanheira LBhardwaj ABenson T(2024)An Empirical Study on the Challenges of eBPF Application DevelopmentProceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions10.1145/3672197.3673429(1-8)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672197.3673429
Sun HXu YLiu JShen YGuan NJiang Y(2024)Finding Correctness Bugs in eBPF Verifier with Structured and Sanitized ProgramProceedings of the Nineteenth European Conference on Computer Systems10.1145/3627703.3629562(689-703)Online publication date: 22-Apr-2024
https://dl.acm.org/doi/10.1145/3627703.3629562
Show More Cited By

Recommendations

Simple and precise static analysis of untrusted Linux kernel extensions
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Extended Berkeley Packet Filter (eBPF) is a Linux subsystem that allows safely executing untrusted user-defined extensions inside the kernel. It relies on static analysis to protect the kernel against buggy and malicious extensions. As the eBPF ...
Sound, precise, and fast abstract interpretation with tristate numbers
CGO '22: Proceedings of the 20th IEEE/ACM International Symposium on Code Generation and Optimization

Extended Berkeley Packet Filter (BPF) is a language and run-time system that allows non-superusers to extend the Linux and Windows operating systems by downloading user code into the kernel. To ensure that user code is safe to run in kernel context, BPF ...
Towards Functional Verification of eBPF Programs
eBPF '24: Proceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions

eBPF is being used to implement increasingly critical pieces of system logic. eBPF's verifier raises the cost of adoption of the technology, as making programs pass the verifier can be very effortful. We observe that the guarantees provided by the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III

Jul 2023

512 pages

ISBN:978-3-031-37708-2

DOI:10.1007/978-3-031-37709-9

Editors:
Constantin Enea
LIX, Ecole Polytechnique, CNRS and Institut Polytechnique de Paris, Palaiseau, France
,
Akash Lal
Microsoft Research, Bangalore, India

© The Author(s) 2023.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 July 2023

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lim SPrasad THan XPasquier TFournaris APalmieri P(2024)SafeBPF: Hardware-assisted Defense-in-depth for eBPF Kernel ExtensionsProceedings of the 2024 on Cloud Computing Security Workshop10.1145/3689938.3694781(80-94)Online publication date: 19-Nov-2024
https://dl.acm.org/doi/10.1145/3689938.3694781
Deokar MMen JCastanheira LBhardwaj ABenson T(2024)An Empirical Study on the Challenges of eBPF Application DevelopmentProceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions10.1145/3672197.3673429(1-8)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672197.3673429
Sun HXu YLiu JShen YGuan NJiang Y(2024)Finding Correctness Bugs in eBPF Verifier with Structured and Sanitized ProgramProceedings of the Nineteenth European Conference on Computer Systems10.1145/3627703.3629562(689-703)Online publication date: 22-Apr-2024
https://dl.acm.org/doi/10.1145/3627703.3629562
Mao JDing HZhai JMa STsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Merlin: Multi-tier Optimization of eBPF Code for Performance and CompactnessProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651387(639-653)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651387

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents