Posts by Natalie Klaus
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.
