内核 C 到 Rust 加固探索：UVC 描述符解析器

一个安全关键的 Linux 内核 C 解析器能否通过用 Rust 重写来加固，且该重写被证明与原始版本等价，并随后经过形式化验证？本次探索在一个目标上运行完整闭环：UVC 视频描述符解析器（来自 drivers/media/usb/uvc/ 的 uvc_parse_format/uvc_parse_frame，v7.2-rc2），选择它是因为它在相隔十六年的时间里承载了两个独立的内存安全 CVE（CVE-2008-3496、CVE-2024-53104，后者被列入 CISA KEV 目录）。

闭环，以及每一步确立了什么

1. 提取 C 叶子（c/）。解析逻辑从内核逐字节复制；仅对环境做了桩替换（// SPIKE-STUB）。编译为 C-ABI 库。提取出的叶子包含计数遍历和按大小分配，因此 CVE-2024-53104 的缺陷类别（解析写入超出计数所分配的范围）是可触达的，而非被抽象掉。

2. 用 Rust 重写（rust/）。同样的解析叶子用安全 Rust 实现，相同的 C ABI 和结果结构体。每一处与 C 的偏差都标记为 // DEVIATION 并记录在案。

3. 差分模糊测试（fuzz/）。一个运行在稳定版 rustc 上的 LibAFL 测试框架用同一输入驱动两个实现，并逐字段比较输出。结果：在修复了一处依赖编译器的有符号溢出位置上的移植不匹配后，在 93% 边覆盖率的 54,019 次执行中零分歧。在忠实的 v7.2-rc2 代码上，不存在可触达的越界访问（两个 CVE 均已修补）。一个可选的负向对照（--features vuln，在两种语言中镜像实现）重新引入 CVE-2024-53104 的不匹配：在同一输入上，C 执行堆越界写入（ASan），Rust 安全地 panic。详情：fuzz/RESULTS.md。

4. 形式化验证（verify/）。忠实的 Rust 叶子通过 Charon 和 Aeneas 提取到 Lean 4，生成代码中没有 sorry，且没有 union 阻塞（不同于 Binder 探索）。两个定理，见 verify/VERIFY-REPORT.md 和 ROADMAP.md：

   • 对所有输入的全安全性（每种结果都是 ok / 受控的 fail / 不终止，绝不是未定义行为的结果）：已证明，无 sorry。这以经过检查的陈述形式，明确表达了 C 所缺乏的内存安全属性。
   • 对良构输入不 panic（panic 仅发生在畸形输入上，此时它是替代 C 的越界写入的预期安全行为）：进行中。其违反即为 CVE-2024-53104 的计数与写入不变式已无 sorry 地证明，连同两个可复用的 Aeneas 循环推理原则，以及 5 个结构上终止的循环的无除法性。剩余部分归结为一个命名的位置遍历功能正确性核心（四条陈述的引理）；见 ROADMAP.md。

状态

该闭环在一个目标上端到端演示。重写通过差分模糊测试被证明与 C 等价；内存安全差异通过负向对照变得具体；Rust 干净地提取到 Lean，其全安全性属性经过机器检查。对于不 panic 定理，计数不变式（CVE-2024-53104 的核心）已无 sorry 地证明，剩余工作归结为一个命名的功能正确性核心，已陈述但尚未证明。完整证明状态和未决引理见 ROADMAP.md。

布局

• c/ — 提取出的 C 叶子及其桩
• rust/ — 安全 Rust 重写
• fuzz/ — LibAFL 差分模糊测试器、结果和 CVE 类别对照
• verify/ — Charon/Aeneas/Lean 提取和定理
• ROADMAP.md — 证明状态和剩余未决引理
• OPEN_CHALLENGES.md — 贡献者可接取的具体任务
• */README.md、fuzz/RESULTS.md、verify/VERIFY-REPORT.md — 各阶段详情

环境

内核 v7.2-rc2（只读参考）。Rust 稳定版 1.94.0。LibAFL 0.15。Charon 909ff09a（v0.1.220，--preset=aeneas），Aeneas c2015b86，Lean/mathlib v4.31.0。