Speaker: Matan Shachnai

Bio

Location : Hill 350

Committee: 

Professor Santosh Nagarakatte

Associate Professor He Zhu

Associate Professor Srinivas Narayana

Associate Professor Rich Martin

Associate Professor Dongyoon Lee (external)

Event Type: PhD Defense

Abstract: The eBPF framework allows user-supplied programs to run inside the Linux kernel for tasks such as networking, tracing, observability, access control, load balancing, and security monitoring. Because these programs execute in a safety-critical kernel context, every eBPF program is checked by the eBPF verifier before it is loaded. The verifier uses static analysis to prove properties such as termination, safe memory access, and well-defined arithmetic behavior. Its analysis must therefore be sound, precise enough to accept useful safe programs, and efficient enough for use in a production kernel. This dissertation focuses on the verifier's value-tracking logic, a central part of its static analysis, where bugs have led to serious kernel vulnerabilities.Specifically, we develop formal techniques for reasoning about the soundness and precision of the eBPF verifier's value-tracking logic as implemented in the Linux kernel. We first introduce a divide-and-conquer verification strategy for implementation-level soundness checking. Rather than verifying each full abstract operator together with the shared reduction operator as one monolithic proof obligation, we separate instruction-specific reasoning from shared reduction reasoning and compose the results. This significantly reduces repeated solver time across operators and kernel versions, while also exposing latent unsoundness in several bitwise operators that were previously masked by the shared reduction operator.We then introduce differential synthesis, an SMT-based method for turning failed soundness checks into executable eBPF witness programs. When a soundness check fails, the SMT solver produces a counterexample that may involve abstract inputs that never arise during verifier analysis, so differential synthesis searches for bounded instruction sequences that reach the relevant abstract values from valid initial verifier inputs. The resulting programs demonstrate reachable mismatches between concrete execution and the verifier's abstract analysis, making verification failures reproducible and useful for debugging and regression testing. Finally, we extend this synthesis framework from soundness to precision; we develop a precision-comparison framework for comparable abstract operators in the verifier. Our framework checks whether one operator is at least as precise as another for all abstract inputs and, when their precision differs, searches for real eBPF programs that illustrate the difference. We use this framework to evaluate precision-improving kernel patches, measure the precision gained from the shared reduction operator, and develop a more precise multiplication operator that has been upstreamed to the Linux kernel.

Organization: 

Contact  Professor Santosh Nagarakatte