-
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…
-
What bugs really matter?
A hierarchy of incorrectness A couple of months ago, I watched this video where Byron Cook is interviewed alongside Carina Hong. Around minute 4, Byron describes his work as one where “an incorrect answer is a crime”.The phrase stuck. I started thinking about how the idea generalizes beyond crime and proofs to all the forms…
-
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.
Claudia Cauli
Software Correctness & Provable Reliability