We are pleased to announce Professors Santosh Nagarakatte and Srinivas Narayana are among the five academic research groups awarded an eBPF Foundation Grant for their work on Verified Path Exploration for eBPF Static Analysis.
This project continues an existing effort in the Agni project to formally verify algorithms in the eBPF verifier. Specifically, the team will explore formal verification and proofs of soundness for a key algorithm in the verifier, namely path pruning, which enables fast safety checking for eBPF programs with a large number of static code paths. The soundness of path pruning is security-critical since incorrect pruning may result in the execution of malicious programs in the kernel. This project takes the first steps towards formal verification of path pruning, by specifying conditions for soundness, and developing systematic techniques to prove soundness and uncover bugs.
The eBPF Foundation, dedicated to advancing eBPF technology by supporting upstream development, promoting its benefits, and enhancing its security and robustness, has awarded our Rutgers team a $50,000 unrestricted grant.
To learn more:https://ebpf.foundation/ebpf-foundation-announces-250000-in-grant-awards-for-five-ebpf-academic-research-projects/
