Posts by Natalie Klaus
Verifying the Linux kernel's isolation code: a policy bypass in io_uring's sandbox filter
A policy bypass in io_uring's sandbox filter, found by writing down what the filter should see. The bug, the reproducer, and a fix in mainline in a day.
Verifying the Linux kernel's isolation code: user namespaces, a proof, and a patch
We verified a core piece of the Linux kernel's container isolation code in Lean 4, and writing the spec turned up a parsing bug we've sent a fix for upstream. We also learned where AI speeds up proofs and where it gets the specification wrong.
The proof is in the spec
AI-written formal proofs find real bugs. But a checked proof only verifies its own model and spec — here's what that means, and how to get it right.
Hardening Linux's C Code: A Rewrite-and-Verify Loop
While testing our reusable C-to-Rust verification workflow on the Linux UVC parser, we found a real integer-overflow bug and joined the upstream fix. The workflow combines a safe Rust rewrite, differential fuzzing against the kernel C, and Lean proofs of the key safety properties behind CVE-2024-53104.
Verifying Linux's Rust Code: From Binder To Lean 4
Android's Binder driver parses attacker-controlled bytes on three billion devices. As part of our formal verification work targeting Linux kernel, we proved that its deserializer never panics on any userspace input, all machine-checked end-to-end from production Rust through Charon and Aeneas into Lean 4.
From Rust Code to Mathematical Proof: How We Verify Safety-Critical Rust
Runtime Verification applies formal methods to cryptographic and safety-critical software. We turn production Rust into machine-checked Lean 4 proofs of correctness, no sorry left behind.
