Hardening Linux's C Code: A Rewrite-and-Verify Loop

This post continues our work on verifying the Linux kernel. Our previous post covered our work on the Binder driver, Android's IPC mechanism, which is written in Rust.

In this post we describe two things:

• the approach we developed for verifying the parts of the Linux kernel that are written in C
• the defect we found in the kernel's C, and how we joined the work on fixing it

Parsers and decoders are where the dragons are, and we came hunting armed with a high-powered fuzzer and a proof assistant.

They are once again our area of interest, because they handle untrusted bytes from devices, userspace and the network, and that is where there is a good chance of finding vulnerabilities. Rewriting that code in a memory-safe language removes an entire class of them by construction. But a rewrite is only trustworthy if you can show two things: that the new code behaves like the old code, and that the new code is actually free of the bugs you set out to remove. This post describes a loop that does both, run end to end on one real target.

The target: one parser, two CVEs

We chose the UVC video descriptor parser. CVE-2008-3496 was a buffer overflow. CVE-2024-53104 was an out-of-bounds write, and it reached the CISA Known Exploited Vulnerabilities catalog after being used in a phone-unlock chain. Two CVEs of the same class in one function, sixteen years apart, make this a realistic target rather than a toy.

The question we focused on: can we rewrite this parser in safe Rust, show the rewrite behaves like the original, and then formally verify that it is free of the bug class, all on real kernel code? The work is at github.com/runtimeverification/kernel-c-to-rust-spike.

The loop

Our rewrite loop contains the following four stages, in order. Each needs the output of the one before it. We used LLMs at every step.

1. Extract the C leaf. We copied the parsing logic out of the kernel byte for byte, stubbed only the surrounding environment, and compiled it as a standalone C library with a C ABI. We kept the counting pass and the sized allocation rather than handing the parser an oversized buffer, because CVE-2024-53104 lives in the gap between the count that sizes the allocation and the parse that writes into it. Abstract that away and you are proving the absence of a bug that cannot occur.

2. Rewrite in safe Rust. The same parsing leaf in idiomatic safe Rust, behind the same C ABI, producing the same result structure. Every place where the Rust departs from the C is tagged and documented, so the diff between the two is auditable.

3. Differential fuzzing: does the Rust behave like the C? A rewrite that is safe but wrong is useless. We built a differential fuzzer (LibAFL, stable Rust) that feeds one input to both implementations and compares the outputs field by field. After fixing one porting mismatch, the run reached zero divergences over 54,019 executions at 93% edge coverage.

A mismatch in behavior between the original C and the Rust rewrite, caught by the fuzzer, led us to a real defect. One buffer size is computed as bits-per-pixel times width times height, divided by 8, and the product is evaluated in 32-bit signed arithmetic, where it can wrap. The kernel builds with -fno-strict-overflow, which makes that wraparound defined. Our harness had compiled the extracted C without the flag, so clang optimized it differently. Rebuilding the oracle with the kernel's flags removed the divergence. The equivalence claim is against the C as the kernel compiles it.

To be precise, this is not a live memory-safety hole in the kernel. On the unmodified code we extracted, no out-of-bounds access is reachable, and both CVEs are fixed. To show the harness can catch the CVE class at all, we added an opt-in negative control (--features vuln) that reintroduces the CVE-2024-53104 counting-versus-writing mismatch in both languages. On the same input the C performs a heap out-of-bounds write, caught by AddressSanitizer, while the Rust panics safely.

What the loop turned up

We stopped comparing the two implementations and looked at the value they both produced. It is wrong.

The three operands come straight from the descriptor, and the product can exceed what the type holds. The driver then records a frame buffer size that is much too small, and for some descriptors exactly zero. Every compiler stores the same number here, so this is not a compiler question. It is also not a memory-safety hole: we traced the consumers, and every copy path takes its bound from the memory actually allocated. The zero case is the sharper one, because a zero-sized buffer makes queue setup fail, and on kernels built to treat warnings as fatal that is not a graceful failure. A malformed descriptor is enough to reach it. A one-command reproducer is at uvc-frame-size-overflow.

We took it to the maintainers and suggested a patch. But it turned out the same issue had been reported ten days earlier (were we disappointed? no! well, maybe. a little), and that patch is the better fix, so we withdrew ours and were invited to review it instead. The review turned into more than an ack: one route to a zero size survived that patch, and Ricardo Ribalda (one of the uvcvideo contributors) asked us to carry a three-patch series. That series is on the list now, reviewed by Ricardo and tested on a UVC gadget by Noam Ben Shimon, the original reporter:

https://lore.kernel.org/linux-media/20260820111556.232652-1-natalie.klaus@runtimeverification.com/

We will write it up properly once it lands.

4. Formal verification: is the Rust free of the bug class? Differential fuzzing gives empirical confidence; a proof settles it for every input. We extract the Rust leaf through Charon and Aeneas into Lean 4 and prove properties there. Unlike the Binder work, there was no union blocker, and the parser extracts cleanly.

We state two properties. Total safety on all inputs says every outcome is a normal return, a controlled failure, or non-termination, and never undefined behaviour. This is proved. For safe Rust much of it holds by construction; stating it in Lean makes it a machine-checked fact rather than an assumption. No panic on well-formed input is the substantive one: when the input satisfies the parser's own validation invariants, parsing completes without panicking. A panic on malformed input is the intended safe behaviour, the thing that replaces an out-of-bounds write. At the core of this property is the relationship between the counting pass and the write indices, and violating it is exactly CVE-2024-53104.

We proved that core sorry-free: the counting pass never under-counts what the parse pass writes. We also proved division-freeness for the 5 structurally-terminating loops out of 11, and built two reusable principles for reasoning about the loops Aeneas generates. What remains for the full theorem is a positional-walk invariant tying the parser's byte walk to the descriptor structure, reduced to four named lemmas. As it stands today: the loop is demonstrated end to end, the CVE-2024-53104 core is machine-checked, and the full theorem is scoped down to a named remainder in progress.

The work is at github.com/runtimeverification/kernel-c-to-rust-spike.

Where it got hard

We want to report on what was difficult here as well.

Reasoning about extracted loops. Aeneas lowers loops into Lean as fixpoint combinators, not ordinary recursive functions, so naive induction does not apply. The working idiom turned out to be a partial-correctness loop invariant, admissible because it holds vacuously at the non-terminating case. We packaged it as a reusable principle and applied it across the counting proof. Termination needed a second, measure-based principle. Neither is exotic once found, but finding the right idiom was the single biggest time sink.

An AI prover disproving our own lemma. We discharge proof obligations with AI provers (Aleph from Logical Intelligence, Aristotle from Harmonic), but every proof is checked by the Lean kernel, so the AI cannot compromise soundness. The most useful thing the prover did was not to close a goal but to refute one. Our first statement of the counting lemma looked obviously true, and Aleph found a counterexample: an unbounded accumulator that could overflow, making the lemma false as written. We corrected the statement with the bounds that input validity already guarantees. A false "obvious" property caught before anything was built on it is what formal verification is for, and neither testing nor intuition would have surfaced it.

Why this scales, and what is next

The point of running the loop on one target was never the one target. It was to show that the loop closes, and to build the parts that make the next target cheaper: the fuzzing harness, the loop-reasoning principles, and a repeatable recipe. Extract, rewrite, differential-fuzz for conformance, verify the property that matters.

Next is closing the positional-walk invariant to finish the no-panic theorem, then pointing the same loop at further parsers of untrusted input: the USB, virtio and descriptor-parsing surfaces where the same shape recurs. We have also published a map of the kernel's Rust and the toolchain's reach across it, with open challenges for anyone who wants to take a target: kernel-rust-coverage-map.

If you maintain code that parses untrusted input and you want to know what a machine-checked property for it would look like, or where this loop would land on your codebase, we would like to hear from you.