runtimeverification/kernel-c-to-rust-spikeУкрепление C-парсеров ядра с помощью переписывания на Rust + дифференциального фаззинга + формальной верификации. Первая цель: UVC (CVE-2024-53104).
Можно ли укрепить критичный для безопасности парсер ядра Linux на C, переписав его на Rust, показав эквивалентность переписанной версии оригиналу и затем формально её верифицировав? Этот эксперимент проходит полный цикл на одной цели: парсере дескрипторов видео UVC (uvc_parse_format/uvc_parse_frame из drivers/media/usb/uvc/, v7.2-rc2), выбранном потому, что он нёс две независимые CVE, связанные с безопасностью памяти, с разницей в шестнадцать лет (CVE-2008-3496, CVE-2024-53104, последняя входит в каталог CISA KEV).
Извлечение C-листа (c/). Логика разбора скопирована из ядра байт в байт; заглушено только окружение (// SPIKE-STUB). Компилируется в библиотеку с C-ABI. Извлечённый лист включает проход подсчёта и выделение нужного размера, поэтому класс ошибок CVE-2024-53104 (разбор пишет за пределы того, что выделил подсчёт) достижим, а не абстрагирован.
Переписывание на Rust (rust/). Тот же лист разбора на безопасном Rust, тот же C-ABI и структура результата. Каждое отклонение от C помечено // DEVIATION и задокументировано.
Дифференциальный фаззинг (fuzz/). Стенд LibAFL на стабильном rustc прогоняет обе реализации на одном входе и сравнивает выходы поле за полем. Результат: после исправления одного расхождения при портировании в месте знакового переполнения, зависящего от компилятора, — ноль расхождений на 54 019 исполнениях при 93% покрытии рёбер. На точном коде v7.2-rc2 выход за границы недостижим (обе CVE исправлены). Опциональный негативный контроль (--features vuln, зеркально в обоих языках) возвращает несоответствие CVE-2024-53104: на одном и том же входе C выполняет запись за границы кучи (ASan), а Rust безопасно паникует. Подробности: fuzz/RESULTS.md.
Формальная верификация (verify/). Точный Rust-лист извлекается через Charon и Aeneas в Lean 4 без sorry в сгенерированном коде и без блокировки из-за объединений (в отличие от эксперимента с Binder). Две теоремы, в verify/VERIFY-REPORT.md и ROADMAP.md:
ok / контролируемый fail / незавершение, но никогда исход неопределённого поведения): доказана, без sorry. Это делает явным, в виде проверенного утверждения, свойство безопасности памяти, которого нет у C.sorry, вместе с двумя переиспользуемыми принципами рассуждения о циклах Aeneas и отсутствием деления для 5 структурно завершающихся циклов. Остаток сводится к именованному ядру функциональной корректности позиционного обхода (четыре сформулированные леммы); см. ROADMAP.md.Цикл продемонстрирован от начала до конца на одной цели. Эквивалентность переписанной версии C показана дифференциальным фаззингом; различие в безопасности памяти сделано наглядным негативным контролем; Rust чисто извлекается в Lean, и его свойство полной безопасности проверено машиной. Для теоремы об отсутствии паники инвариант подсчёта (ядро CVE-2024-53104) доказан без sorry, а оставшаяся работа сведена к именованному ядру функциональной корректности, сформулированному, но ещё не доказанному. Полный статус доказательств и открытые леммы — в ROADMAP.md.
c/ — извлечённый C-лист и его заглушкиrust/ — переписанная версия на безопасном Rustfuzz/ — дифференциальный фаззер LibAFL, результаты и контроль класса CVEverify/ — извлечение Charon/Aeneas/Lean и теоремыROADMAP.md — статус доказательств и оставшиеся открытые леммыOPEN_CHALLENGES.md — конкретные задачи, которые может взять участник*/README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — детали по каждому этапуЯдро v7.2-rc2 (эталон только для чтения). Rust stable 1.94.0. LibAFL 0.15.
Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib
v4.31.0.