runtimeverification/kernel-c-to-rust-spike

GitHubRepository PoCWriteup

PoC files

36 files

File viewing is interactive and short-lived. Downloads are password-protected ZIP archives using password eip.

GitHub
Analysisdeepseek-v4-pro:cloud ·

Technical assessment

The artifact is a research spike demonstrating a C-to-Rust hardening loop for the Linux kernel UVC descriptor parser. It contains a byte-for-byte C extraction, a safe Rust rewrite, a differential fuzzer, and formal verification proofs. It does not contain an exploit or scanner for CVE-2024-53104; the vulnerability is discussed and a negative control is provided to demonstrate the bug class, but the primary artifact is a technical analysis and hardening demonstration.

Backdoor review

No backdoor observed in reviewed code

The repository is a research spike demonstrating a C-to-Rust rewrite of a Linux kernel UVC descriptor parser, with differential fuzzing and formal verification. All reviewed source code is consistent with this stated purpose. The C and Rust implementations parse untrusted USB descriptor data locally; no network communication, data exfiltration, or unrelated payload execution is present. The fuzzer harness drives both implementations and compares results, saving findings to a local directory. The negative control feature (SPIKE_VULN) is clearly documented and opt-in. No concealed or materially misrepresented harmful behavior was found.

ClassificationWriteup
Model confidence95%
AuthenticationNot required
LanguagesCRustPythonLean
Target softwareLinux kernel UVC video driver
Attack typesout-of-bounds write
Evidence & reasoningClassification basis · observed behavior · safety review
Technical evidence

Classification basis and observed behavior

Classification basis

The artifact is a writeup because it is a substantive technical analysis of a vulnerability and a hardening technique, including source code for a C extraction, a Rust rewrite, a fuzzer, and formal verification. It does not contain code intended to exploit a live system (exploit) or to scan for the vulnerability (scanner). The negative control is for demonstration purposes within the research context, not a standalone exploit.

README.md:1-72c/uvc_parse.c:1-25rust/src/lib.rs:1-20

Requirements

  • The artifact is a research spike and does not exploit a vulnerability. It requires a build environment with clang, Rust, and Lean to compile and run the provided code.README.md:70-72

Observed behavior

  • The artifact provides a C extraction of the vulnerable kernel code, a safe Rust rewrite, a differential fuzzer to compare their outputs, and formal verification proofs. It includes a negative control (SPIKE_VULN) that reintroduces the CVE-2024-53104 bug class to demonstrate the safety difference between C and Rust.README.md:12-46c/uvc_parse.c:985-1002rust/src/lib.rs:682-696
Safety-review evidence

Behaviors behind the backdoor verdict

Observables

Local File Write
fuzz/src/main.rs writes findings to a local 'findings' directoryThe differential fuzzer saves discovered divergences and panics as local files for analysis, which is standard fuzzer behavior and not a backdoor.fuzz/src/main.rs:125-126fuzz/src/main.rs:175-186
Compile Time Feature
SPIKE_VULN / 'vuln' featureAn opt-in negative control that reintroduces a CVE-2024-53104-class bug for testing. It is clearly documented in README.md, c/uvc_parse.c, and rust/src/lib.rs, and is disabled by default.README.md:27-30c/uvc_parse.c:985-1002rust/src/lib.rs:682-696
Review boundaries

What the analysis did not establish

  • material evidence limitation
  • 4 binary files (fuzz corpus seeds and a finding) were not inspected; their metadata and small sizes (13-61 bytes) are consistent with fuzzer test inputs.
  • 24 unclassified files (e.g., Lean verification proofs, build scripts) were not provided for review.
Model interpretation

This review is limited to the supplied PoC code and context. It does not assert that the code works or is safe to execute.

Linked vulnerabilities

1