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

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

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

Using LLM-based Verification to Eliminate Bugs in Linux's Network Stack Article: Yiyun Liu, Kiran Gopinathan, Nikhil Pimpalkhare

Research: Yiyun Liu

We used LLMs to verify Linux's nftables `nft` CLI utility. Along the way, we found and patched bugs that had sat in the kernel for years.

Firewall rules act like railway signals, telling each packet whether it may pass.

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 maintainers1). 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 bugs nftables is one of the firewall mechanisms provided by the Linux operating system. Every packet your OS receives passes through nftables, which determines which packets are forwarded and which are dropped. Having replaced iptables in 2014 as the default packet filter of every major Linux distribution, nftables today guards everything from home routers to container networks; if a Linux machine filters traffic, nftables almost certainly decides what gets through. Firewalls are a critical component of most network security layers, and vulnerabilities in them can compromise whole systems. A verified implementation of nftables would increase assurance in this critical layer. nftables rulesets and compilation pipeline The full architecture of nftables is shown below and consists of a userspace CLI tool and a kernel module: The architecture of nftables. The nft cli tool's compiler and optimizer turn the ruleset into bytecode; the kernel's bytecode executor runs it over every packet flowing through the machine. The optimizer (highlighted) is where the bugs we found live.This CLI tool takes as input a series of user-supplied policies, expressed as an ordered list of rules, where each rule matches on some part of the packet (its source address, its destination port, its TCP flags) and returns a verdict, i.e. accept or drop. For example, the following rules tell nftables to accept any packets where the destination address (daddr) is 192.168.50.1 or 192.168.50.2. ip daddr 192.168.50.1 accept ip daddr 192.168.50.2 accept The nft command-line tool parses these rulesets and compiles them into a compact register-based bytecode, which it then loads into the kernel. There, the kernel’s interpreter uses the bytecode to compute a verdict for every packet passing through the network stack: either accepting it through the firewall or dropping it. As this bytecode runs on every packet the system sees, it sits on a hot path of the kernel, and thus its efficiency is critical. For this reason, the CLI tool also provides an optimizer module for the source language that rewrites your input rules to run more efficiently (reducing the number of reads, or removing redundant checks). A critical security property that users rely on the optimizer to guarantee is that it preserves the semantics of its input rules. In other words, the verdict computed for a packet should be the same regardless of whether it was passed through the optimized or unoptimized ruleset. We set out to prove the correctness of the nft command-line tool, and in the process found two bugs in the...

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

Related Articles

(no title)

Scientists reverse brain aging, with a nasal spray

AI has torched the market for junior programmers

Al Vigier: Canada's AI strategy shouldn't include secret Palantir bills

The Anatomy of an AI-Native Org