runtimeverification/kernel-c-to-rust-spikeIndurimento dei parser C del kernel tramite riscrittura in Rust, fuzzing differenziale e verifica formale. Primo obiettivo: UVC (CVE-2024-53104).
Un parser C del kernel Linux critico per la sicurezza può essere irrobustito riscrivendolo in Rust, con la riscrittura dimostrata equivalente all'originale e poi formalmente verificata? Questo spike esegue l'intero ciclo su un unico obiettivo: il parser dei descrittori video UVC (uvc_parse_format/uvc_parse_frame da drivers/media/usb/uvc/, v7.2-rc2), scelto perché ha portato due CVE indipendenti di sicurezza della memoria a sedici anni di distanza (CVE-2008-3496, CVE-2024-53104, quest'ultima nel catalogo CISA KEV).
Estrazione della foglia C (c/). La logica di parsing copiata byte per byte dal kernel; solo l'ambiente è stubbato (// SPIKE-STUB). Compila in una libreria con ABI C. La foglia estratta include la passata di conteggio e l'allocazione dimensionata, così la classe di bug di CVE-2024-53104 (il parsing che scrive oltre quanto allocato dal conteggio) è raggiungibile, non astratta.
Riscrittura in Rust (rust/). La stessa foglia di parsing in Rust sicuro, stessa ABI C e stessa struct di risultato. Ogni deviazione dal C è contrassegnata con // DEVIATION e documentata.
Fuzzing differenziale (fuzz/). Un harness LibAFL su rustc stabile pilota entrambe le implementazioni da un unico input e confronta gli output campo per campo. Risultato: dopo aver corretto una discrepanza di porting in un punto di overflow con segno dipendente dal compilatore, zero divergenze su 54.019 esecuzioni con copertura degli edge al 93%. Sul codice fedele v7.2-rc2 nessun accesso fuori dai limiti è raggiungibile (entrambe le CVE sono corrette). Un controllo negativo opt-in (--features vuln, rispecchiato in entrambi i linguaggi) reintroduce la discrepanza di CVE-2024-53104: sullo stesso input il C esegue una scrittura fuori dai limiti sull'heap (ASan), il Rust va in panic in modo sicuro. Dettagli: fuzz/RESULTS.md.
Verifica formale (verify/). La foglia Rust fedele viene estratta tramite Charon e Aeneas in Lean 4 senza sorry nel codice generato, e senza blocco dovuto alle union (a differenza dello spike su Binder). Due teoremi, in verify/VERIFY-REPORT.md e ROADMAP.md:
ok / fail controllato / non terminazione, mai un esito di comportamento indefinito): dimostrato, senza sorry. Questo rende esplicita, come affermazione verificata, la proprietà di sicurezza della memoria che il C non possiede.sorry, insieme a due principi riutilizzabili di ragionamento sui cicli di Aeneas e all'assenza di divisioni per i 5 cicli che terminano strutturalmente. Il resto si riduce a un nucleo di correttezza funzionale denominato positional-walk (quattro lemmi enunciati); vedi ROADMAP.md.Il ciclo è dimostrato end-to-end su un unico obiettivo. La riscrittura è dimostrata equivalente al C tramite fuzzing differenziale; la differenza in sicurezza della memoria è resa concreta dal controllo negativo; il Rust si estrae in modo pulito in Lean e la sua proprietà di sicurezza totale è verificata automaticamente. Per il teorema di assenza di panic, l'invariante di conteggio (il nucleo di CVE-2024-53104) è dimostrato senza sorry e il lavoro rimanente è ridotto a un nucleo di correttezza funzionale denominato, enunciato ma non ancora dimostrato. Lo stato completo delle dimostrazioni e i lemmi aperti sono in ROADMAP.md.
c/ — la foglia C estratta e i suoi stubrust/ — la riscrittura in Rust sicurofuzz/ — il fuzzer differenziale LibAFL, i risultati e il controllo della classe CVEverify/ — estrazione Charon/Aeneas/Lean e teoremiROADMAP.md — stato delle dimostrazioni e lemmi aperti rimanentiOPEN_CHALLENGES.md — attività concrete che un contributore può intraprendere*/README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — dettagli per faseKernel v7.2-rc2 (riferimento in sola lettura). Rust stabile 1.94.0. LibAFL 0.15.
Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib
v4.31.0.