ИИ-агенты помогли формально верифицировать ядро xv6 вплоть до уровня железа

Франс Каашук и Николай Зельдович представили MachCSL — фреймворк для формальной верификации системного программного обеспечения поверх низкоуровневой семантики RISC-V-компьютера. В основе лежит официальная семантика Sail RISC-V.

Рассуждения на уровне железа

Ключевая идея MachCSL — приспособить конкурентную сепарационную логику (на базе Iris) к рассуждениям о работе оборудования на субинструкционном уровне. Речь идёт о тех деталях, которые обычно прячутся за абстракциями: трансляция таблиц страниц, TLB, уровни привилегий, конфигурационные регистры, цикл выборки-декодирования-исполнения инструкций, ловушки и прерывания, DMA, разделяемая память и даже сбои питания. Доказательство на таком уровне детализации гарантирует, что системный код корректно управляет всеми тонкостями железа.

Верификация на столь низком уровне абстракции утомительна для человека — но, как отмечают авторы, с рассуждениями о подобных мелочах неплохо справляются агенты на основе больших языковых моделей. Именно они взяли на себя значительную часть рутинной работы.

Случай xv6

В качестве показательного примера исследователи верифицировали учебное ядро xv6 — 6657 строк на C и ассемблере. Это ядро предоставляет традиционный Unix-интерфейс системных вызовов (процессы, файловая система, файловые дескрипторы, вытесняющее планирование) и содержит заметную внутреннюю конкурентность: поддержку многоядерности с мелкогранулярными блокировками, разделяемую память, прерывания, DMA.

В ходе работы обнаружилось 11 ошибок в самой реализации xv6, а также по одной ошибке в семантике Sail RISC-V и в её извлечении в Lean. Весь труд занял 102 дня — включая время на разработку самого фреймворка MachCSL.

Теорема про echo

Поверх верифицированного ядра авторы доказали теорему о поведении на уровне консоли. Если пользователь набирает на UART-консоли echo hello world, то единственный вывод, который может произвести система, — это hello world (при отсутствии сбоев и прочих ошибок). Теорема охватывает не только ядро, но и бинарники init, sh, echo, cat, grep, sync и seccomp из начального образа файловой системы.

Источник: Lobsters