runtimeverification/kernel-c-to-rust-spikeEndurecimiento de parsers C del kernel mediante reescritura en Rust + fuzzing diferencial + verificación formal. Primer objetivo: UVC (CVE-2024-53104).
¿Se puede endurecer un analizador C del kernel de Linux crítico para la seguridad reescribiéndolo en Rust, demostrando que la reescritura es equivalente al original y luego verificándola formalmente? Este spike ejecuta el ciclo completo sobre un objetivo: el analizador de descriptores de vídeo UVC (uvc_parse_format/uvc_parse_frame de drivers/media/usb/uvc/, v7.2-rc2), elegido porque acumuló dos CVE independientes de seguridad de memoria con dieciséis años de diferencia (CVE-2008-3496, CVE-2024-53104, este último en el catálogo KEV de la CISA).
Extraer la hoja C (c/). La lógica de análisis copiada byte a byte del kernel; solo el entorno está simulado (// SPIKE-STUB). Compila como una biblioteca con ABI de C. La hoja extraída incluye la pasada de conteo y la asignación dimensionada, de modo que la clase de error de CVE-2024-53104 (el análisis escribiendo más allá de lo que asignó el conteo) es alcanzable, no abstraída.
Reescribir en Rust (rust/). La misma hoja de análisis en Rust seguro, con la misma ABI de C y la misma estructura de resultado. Cada desviación respecto al C está etiquetada con // DEVIATION y documentada.
Fuzzing diferencial (fuzz/). Un arnés LibAFL sobre rustc estable ejecuta ambas implementaciones desde una misma entrada y compara las salidas campo por campo. Resultado: tras corregir una discrepancia de portado en un punto de desbordamiento con signo dependiente del compilador, cero divergencias en 54.019 ejecuciones con un 93% de cobertura de aristas. Sobre el código fiel de v7.2-rc2 no es alcanzable ningún acceso fuera de límites (ambos CVE están parcheados). Un control negativo opcional (--features vuln, replicado en ambos lenguajes) reintroduce la discrepancia de CVE-2024-53104: con la misma entrada, el C realiza una escritura fuera de límites en el heap (ASan) y el Rust entra en pánico de forma segura. Detalles: fuzz/RESULTS.md.
Verificación formal (verify/). La hoja Rust fiel se extrae mediante Charon y Aeneas a Lean 4 sin ningún sorry en el código generado, y sin bloqueo por uniones (a diferencia del spike de Binder). Dos teoremas, en verify/VERIFY-REPORT.md y ROADMAP.md:
ok / fail controlado / no terminación, nunca un resultado de comportamiento indefinido): demostrado, sin sorry. Esto hace explícita, como afirmación comprobada, la propiedad de seguridad de memoria de la que carece el C.sorry, junto con dos principios reutilizables de razonamiento de bucles de Aeneas y la ausencia de división para los 5 bucles que terminan estructuralmente. El resto se reduce a un núcleo de corrección funcional de recorrido posicional con nombre (cuatro lemas enunciados); véase ROADMAP.md.El ciclo se demuestra de extremo a extremo sobre un objetivo. La reescritura se muestra equivalente al C mediante fuzzing diferencial; la diferencia en seguridad de memoria se hace concreta con el control negativo; el Rust se extrae limpiamente a Lean y su propiedad de seguridad total está comprobada por máquina. Para el teorema de ausencia de pánico, el invariante de conteo (el núcleo de CVE-2024-53104) está demostrado sin sorry y el trabajo restante se reduce a un núcleo de corrección funcional con nombre, enunciado pero aún no demostrado. El estado completo de las demostraciones y los lemas abiertos están en ROADMAP.md.
c/ — la hoja C extraída y sus stubsrust/ — la reescritura en Rust segurofuzz/ — el fuzzer diferencial LibAFL, los resultados y el control de clase CVEverify/ — la extracción Charon/Aeneas/Lean y los teoremasROADMAP.md — estado de las demostraciones y los lemas abiertos restantesOPEN_CHALLENGES.md — tareas concretas que un colaborador puede asumir*/README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — detalle por etapaKernel v7.2-rc2 (referencia de solo lectura). Rust estable 1.94.0. LibAFL 0.15. Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib v4.31.0.