Speaker
Description
This talk will present our approach to enhancing the eBPF verifier's precision: lazy abstraction refinement with proof. We will begin by discussing the fundamental sources of imprecision in the current verifier and reviewing relevant efforts towards these issues. Next, we will show how a proof-based approach can potentially improve precision without introducing much complexity. We achieve this by (1) utilizing the existing abstract interpretation as much as possible to benefit from its efficiency, i.e., being lazy, (2) refining the abstraction with a more precise technique when it is too coarse-grained, allowing the verifier to continue the validation, (3) encoding the refinement in a machine-checkable proof, which is accepted only after linear-time validation. In essence, proofs generated in user space and validated in kernel space ensure minimal overhead.
This work is in its early stages, and we look forward to sharing our central idea and receiving valuable feedback.