runtimeverification/kernel-c-to-rust-spikeHardening kernel C parsers via Rust rewrite + differential fuzzing + formal verification. First target: UVC (CVE-2024-53104).
Can a security-critical Linux kernel C parser be hardened by rewriting it in
Rust, with the rewrite shown equivalent to the original and then formally
verified? This spike runs the full loop on one target: the UVC video descriptor
parser (uvc_parse_format/uvc_parse_frame from drivers/media/usb/uvc/,
v7.2-rc2), chosen because it carried two independent memory-safety CVEs sixteen
years apart (CVE-2008-3496, CVE-2024-53104, the latter in the CISA KEV catalog).
Extract the C leaf (c/). The parsing logic copied byte-for-byte from
the kernel; only the environment stubbed (// SPIKE-STUB). Compiles to a
C-ABI library. The extracted leaf includes the counting pass and sized
allocation, so the CVE-2024-53104 bug class (parse writing past what the
count allocated) is reachable, not abstracted away.
Rewrite in Rust (rust/). The same parsing leaf in safe Rust, same C
ABI and result struct. Every deviation from the C is tagged // DEVIATION
and documented.
Differential fuzzing (fuzz/). A LibAFL harness on stable rustc drives
both implementations from one input and compares outputs field-by-field.
Result: after fixing one porting mismatch at a compiler-dependent
signed-overflow site, zero divergences over 54,019 executions at 93% edge
coverage. On the faithful v7.2-rc2 code no out-of-bounds access is reachable
(both CVEs are patched). An opt-in negative control (--features vuln,
mirrored in both languages) reintroduces the CVE-2024-53104 mismatch: on the
same input the C does a heap out-of-bounds write (ASan), the Rust panics
safely. Details: fuzz/RESULTS.md.
Formal verification (verify/). The faithful Rust leaf extracts through
Charon and Aeneas into Lean 4 with no sorry in the generated code, and
with no union blocker (unlike the Binder spike). Two theorems, in
verify/VERIFY-REPORT.md and ROADMAP.md:
ok / controlled fail /
nontermination, never an undefined-behaviour outcome): proved, sorry-free.
This makes explicit, as a checked statement, the memory-safety property the
C lacks.sorry-free, along with two reusable Aeneas loop-reasoning principles and
div-freeness for the 5 structurally-terminating loops. The remainder reduces
to a named positional-walk functional-correctness core (four stated lemmas);
see ROADMAP.md.The loop is demonstrated end to end on one target. The rewrite is shown
equivalent to the C by differential fuzzing; the memory-safety difference is
made concrete by the negative control; the Rust extracts cleanly into Lean and
its total-safety property is machine-checked. For the no-panic theorem, the
counting invariant (the CVE-2024-53104 core) is proved sorry-free and the
remaining work is reduced to a named functional-correctness core, stated but not
yet proved. Full proof status and the open lemmas are in ROADMAP.md.
c/ — the extracted C leaf and its stubsrust/ — the safe-Rust rewritefuzz/ — the LibAFL differential fuzzer, results, and CVE-class controlverify/ — Charon/Aeneas/Lean extraction and theoremsROADMAP.md — proof status and the remaining open lemmasOPEN_CHALLENGES.md — concrete tasks a contributor can pick up*/README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — per-stage detailKernel v7.2-rc2 (read-only reference). Rust stable 1.94.0. LibAFL 0.15.
Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib
v4.31.0.