Category: Uncategorized
-
Towards a sound DPDK eBPF validator?
The eBPF validator within DPDK exists to do one job: never let an unsafe program execute on the data plane. A soundness bug in it may lead to a security exploit. Last year, Konstantin Ananyev, Marat Khalili, and I were chatting about good targets for formal verification, and lib/bpf/bpf_validate.c was the obvious one. We then…
-
My EuroSys 2026 paper is obsolete
My team and I have a paper appearing at EuroSys 2026 on applying formal methods to cloud infrastructure. We found critical bugs, documented the effort, and published practical guidance for adoption. I’m proud of this work. And it’s already obsolete.