Verification of eBPF Programs
October 2021 - Present
SRI International
- Verifying memory safety and information safety of eBPF programs (Linux Kernel extensions) in user-space
- Developing a Type System with Abstract Interpretation underneath for eBPF (Proof-Carrying code infrastructure)
- Generating proof certificates that can be passed to and trusted by the kernel, and are human-readable