Using LLM-based Verification to Eliminate Bugs in Linux's Network Stack

Summary

LLMs have grown alarmingly capable at finding bugs in production software. This accentuates an already severe risk: much of our critical infrastructure is mediated by software, and every bug in that software is a potential exploit. Formal verification offers the potential to mitigate this risk by producing proofs that entire classes of bugs are impossible, but it has seen limited real-world use because it demands scarce, expensive, specialist expertise. Fortunately, LLMs are increasingly capable of verification too, pointing toward a future where critical software infrastructure is secure by construction.lean-zip, a formally verified zlib implementation written by loosely supervised AI agentsIn this blog post, we report on results from LLM-guided verification experiments at Basis. Our target was a key component of Linux’s network stack: the nftables firewall compiler and optimizer, which we set out to verify in the Rocq theorem prover. nftables is one such piece of critical infrastructure. It filters the traffic of almost every Linux machine, and vulnerabilities in it are treated with the highest severity, since a firewall that misfilters exposes every machine it was meant to protect.In the process of verifying nftables, we uncovered two critical bugs affecting every version of Linux since 2022 (these have been disclosed to maintainers). Our verified implementation was proven to be free of these semantics-altering bugs, and a secondary experiment showed that the more severe of the two would not be found via a naive LLM bug search.Our experiments suggest that the effort involved in producing proofs and constructing robust verified systems is increasingly automatable. The rest of this post gives an overview of nftables, the bugs we found, and our process for using LLMs to verify critical networking software.A quick primer on nftables and its bugsnftables is one of the firewall mechanisms provided by the Linux operating system. Every packet your OS receives passes thro...