18–20 Sept 2024
Europe/Vienna timezone

Lazy Abstraction Refinement with Proof for an Enhanced Verifier

19 Sept 2024, 12:30
30m
"Hall N1" (Austria Center)

"Hall N1"

Austria Center

180
eBPF Track eBPF Track

Speaker

Hao Sun (ETH Zurich)

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.

Primary author

Hao Sun (ETH Zurich)

Presentation materials