Speaker
Description
First presented to the community at Linux Plumbers 2023 [1], Agni is a tool designed to formally verify the correctness of the verifier's range analysis. Agni automatically converts the verifier's source code into an SMT problem, which is then fed into the Z3 solver to check the soundness of the range analysis logic.
This talk will provide an update on Agni's recent developments. In particular, a year ago, Agni would need several hours to several weeks to verify the soundness of the range analysis for all instructions. Thanks to a new, modular verification mode, Agni's runtime has been reduced to minutes in most cases.
This significant improvement allowed us to build a CI where Agni is regularly run against various kernel versions (including bpf-next). Finally, we will discuss the remaining milestones before we can consider a better integration of Agni with the BPF CI.
1 - https://lpc.events/event/17/contributions/1590/