Verifying the eBPF Verifier in the Linux Kernel with Agni

This project is building a collection of techniques and tools to automatically verify the implementation of the static analysis algorithms used by the eBPF verifier in the Linux Kernel. Our eventual goal is to provide strong proofs of correctness guarantees for the entire eBPF verifier in the Linux Kernel.

As part of this project, we have developed new algorithms for abstract multiplication of two tnum abstract domain values, which has been upstreamed to the Linux Kernel.

We have developed a prototype to automatically generate verification conditions for the Kernel's abstract operators directly from the Linux Kernel's source code. When these verification conditions are checked with our soundness specifications, we can discover potential unsoundness in the abstract operators. Our prototype, Agni is currently used as part of the CI of the Linux kernel.

Participants

• Harishankar Vishwanathan (PhD student)
• Matan Shachnai (PhD student)
• Srinivas Narayana (faculty)
• Santosh Nagarakatte (faculty)

Patches Upstreamed to the Linux Kernel

• July 2025: Hari's patch to improve the precision of the BPF_ADD and BPF_SUB operators upstreamed in to the Linux Kernel.
• Jan 2025: Matan's patch to improve the precision of the multiplication abstract operator in the eBPF verifier upstreamed to the mainline Linux Kernel.
• March 2024: Our patch to the eBPF verifier in the Linux kernel to make the abstract operators sound (BPF_OR, BPR_AND, and BPF_XOR).
• June 2021: Our Linux kernel patch with a new algorithm for sound and precise multiplication of tnums (an abstract domain in the eBPF verifier).

Code

• Agni Prototype for checking the soundness of abstract operators in the in Linux Kernel
• Vayu prototype for synthesizing eBPF verifier's abstract operators.

Talks

• June 2025: Daroc Alden wrote an article in the Linux Weekly News summarizing the talk by Prof. Santosh Nagarakatte on "Formally Verifying the eBPF verifier" at LSFMM+BPF Summit.
• June 2025: Daroc Alden wrote an article in the Linux Weekly News summarizing the talk by Prof. Srinivas Narayana on "Verifying the BPF verifier's path-exploration logic" at LSFMM+BPF Summit.
• June 2025: Prof. Santosh Nagarakatte talked about our eBPF verification work at the Distinguished Webinar Series in Artificial Intelligence and Cyber Security. See here for a recording.
• October 2024: Prof. Santosh Nagarakatte's talk at SAS 2024 on "Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel".
• November 2023: Harishankar Vishwanathan's talk on Agni at the Linux Plumbers Conference is available here.

Publications

• Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis. [preprint]
  Matan Shachnai, Harishankar Vishwanathan, Srinivas Narayana, and Santosh Nagarakatte.
  Proceedings of the 32nd Static Analysis Symposium (SAS 2025), Singapore, October 2025.
  
  
• Automatic Synthesis of Abstract Operators for eBPF. [preprint]
  Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte.
  Proceedings of the Proceedings of the 2025 SIGCOMM Workshop on eBPF and kernel extensions (eBPF-2025), Coimbra, Portugal, September 2025.
  
  
• Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel. [preprint]
  Matan Shachnai, Harishankar Vishwanathan, Srinivas Narayana, and Santosh Nagarakatte.
  Proceedings of the 31st Static Analysis Symposium (SAS 2024), Pasadena, California, USA, October 2024.
  
  
• Verifying the Verifier: eBPF Range Analysis Verification. [preprint]
  Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte
  Proceedings of the 35th International Conference on Computer Aided Verification (CAV-2023), Paris, France, July 17-22, 2023.
  Acceptance rate: 26% (68 out of 262 submissions)
  
  
• Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers [preprint]
  Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte
  Proceedings of the International Symposium on Code Generation and Optimization (CGO-2022), Seoul, South Korea, April, 2022.
  Acceptance rate: 27% (27 out of 99 submissions)
  CGO 2022 Distinguished Paper Award
  
  
• Semantics, Verification, and Efficient Implementations for Tristate Numbers [pdf]
  Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte
  Department of Computer Science, Rutgers University Technical Report DCS-TR-755, May 2021
  
  

Funding:

• The eBPF Foundation Research Gift, $50,000. Verified Path Exploration for eBPF Static Analysis.. 2024-2025.
• NSF, FMiTF Track II, $150,000, FMitF: Track II: Formally-Verified eBPF Verifier in the Linux Kernel, 2024-2026.
• NSF FMiTF Track I, $749,356, Formally Verified Sandboxing for Packet-Processing Programs , 2020-2024.
• Facebook Networking Systems Research Award, $50,000, Safe and Efficient Packet Processing with Verification of eBPF Programs, 2019.