Aeneas-based verification of Linux kernel Rust, a related approach

[klausnat]

Hi all. We've been running a verification effort with a similar spirit to verify-rust-std, but targeting Rust in the Linux kernel, and thought it might be of interest here, and useful to compare approaches.

Where your campaign uses Kani/CBMC and model checking on the std library, we use a deductive path: Charon + Aeneas extract the Rust into Lean 4, where we state and prove properties. Two results so far:

Verifying existing kernel Rust. We proved a no-panic property for the Binder driver's deserializer of userspace input (Android IPC), machine-checked end to end, sorry-free. The interesting obstacle was union types, the deserializer is built on C-style type-punning, which Aeneas doesn't yet support; we filed it upstream and re-model the union as a byte array pinned to the real layout by compile-time assertions.

A C-to-Rust hardening loop. For a kernel C parser with a real CVE (UVC, CVE-2024-53104), we rewrite the C in safe Rust, use differential fuzzing to establish the rewrite matches the original C, then verify. The counting-vs-writes invariant whose violation is the CVE is proved sorry-free.

One thing that resonated with the "how can the verifications themselves be trusted?" discussions here: our proof obligations are discharged with AI provers, but every proof is checked by the Lean kernel, and our automated prover actually disproved our first too-strong statement of the counting lemma before we corrected it. The AI proposes; the kernel decides.

Repos, if useful:

Binder: https://github.com/runtimeverification/kernel-rust-verification-spike
Coverage map (whole kernel Rust tree through the toolchain): https://github.com/runtimeverification/kernel-rust-coverage-map
C-to-Rust spike: https://github.com/runtimeverification/kernel-c-to-rust-spike

Different toolchain, overlapping goals, would be glad to compare notes on where each approach hits walls (loops, unsafe, scaling).