Доказано ≠ безопасно: как каскады ИИ-агентов заставили меня усилить модель угроз

В первой статье я рассказал, как собрал операционную систему и доказал ее работу. Спустя время я понял, что этого недостаточно.

Всё чаще стали попадаться на глаза новости о том, как ИИ-агенты находят уязвимости в ядрах Linux за часы. Каскады ИИ-агентов - это уже не фантастика из фильмов, а реальный инструмент, который снижает стоимость и время на поиск ошибок до нуля. Я посмотрел на свою модель угроз и понял неприятную вещь: мои доказательства работают для моего понимания безопасности, но они ничего не знают о реальном мире.

Контракт может быть математически безупречным, но при этом абсолютно бесполезным, если он не покрывает то, как атакуют на самом деле. Настоящая зрелость проекта начинается не с написания кода, а с честного признания того, что именно я не могу доказать.

Ловушка «доказано, значит безопасно»

Формальная верификация - это мощный инструмент. SPARK доказывает, что код делает ровно то, что записано в контрактах. Но в контракте может быть записано Post => True. И это формально докажется. Это называется вакуумным контрактом. Он ничего не гарантирует, но математика довольна.

Реальная безопасность начинается с другого вопроса: «А какую угрозу я пытаюсь предотвратить?».

Я написал THREAT_MODEL.md. Не как формальный документ для галочки, а как рабочий инструмент. Из него следует простой, но жесткий вывод: любая непроверенная строка кода считается уже скомпрометированной. Скрытность больше не работает. Работает только формальное доказательство и изоляция на уровне ядра.

Самая сложная битва: HTTP-сервер

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

Изначально я пытался доказать весь модуль schild_http_server целиком. Но там смешалась логика разбора запросов, работа с файловой системой и формирование ответов. SPARK сходил с ума от неограниченных строковых типов, а gnatprove выдавал сотни недоказуемых условий.

Тогда я применил архитектурный прием, который теперь заложен в самой модели угроз. Я разделил код. Опасную часть, которая разбирает входящие данные от атакующего, я вынес в отдельный пакет schild_http_core и перевел его в режим SPARK_Mode => On. Вот как выглядит контракт для функции извлечения пути из запроса:

function Extract_Path (B : Request_Buffer; Request_Len : Integer) return Path_String
  with Pre => Request_Len in 5 .. Max_Request_Len;

Логика работы с файловой системой осталась в режиме Off. Но тут возникает вопрос: если вызывающий код находится в режиме Off, он не обязан соблюдать предусловия из режима On. Значит, мне пришлось самому защитить проверенный код от непроверенного. В вызывающем модуле появились жесткие рантайм-проверки. Эта битва научила меня главному: доказательство работает только тогда, когда оно окружено понятной архитектурой.

В ходе этого аудита я нашел и потенциальную проблему в отдаче больших файлов. Если файл на диске больше буфера ответа, сервер обрежет его, но оставит в заголовке Content-Length исходный размер. Клиент зависнет в ожидании данных. Классический DoS. Сейчас я переписываю этот участок, чтобы вместо обрезки отдавать корректный код ошибки. Именно такие моменты - когда математика и логика вскрывают баг, который не смогли найти тесты - и приносят самое большое удовольствие от работы. Это сродни рентгену сварного шва: ты не видишь дефект глазами, но прибор показывает, что металл внутри пористый. И ты его перевариваешь.

Как я заставил ИИ работать на надежность

Я не скрываю, что использую ИИ-агента как парного программиста. Это сильно ускоряет написание рутины. Но когда цель смещается в сторону безопасности, слепо доверять генерации кода нельзя.

Мой подход к контролю над ИИ строится на трех принципах. Сначала идет точность формулировок: я не прошу «напиши сервер», а ставлю задачу на уровне спецификаций. Потом перекрестные проверки: любой предложенный агентом код я сверяю с документацией seL4 или с исходниками ядра, чтобы убедиться, что он не выдумал несуществующий системный вызов. И главный судья - это gnatprove. Если контракт не доказывается, агент идет переделывать. Если доказывается, но нарушает мою модель угроз, я переписываю контракт.

Доказательство стало тем фильтром, который отделяет полезный сгенерированный код от опасного.

Что дальше и приглашение к разговору

Сейчас в ядре доказано 186 модулей (0 недоказанных условий). Но моя модель угроз честно говорит, что остались непроверенные части. Нет IOMMU на тестовом железе, поэтому DMA-изоляция остается открытым вопросом. И это нормально. Зрелость проекта - это не отсутствие проблем, а их четкое понимание и очерченные границы.

Теперь я хочу обратиться к сообществу. Формальная верификация дает потрясающие гарантии, но она требует дисциплины и времени. Какие неочевидные сценарии применения вы видите для такой архитектуры? Защищенные сетевые шлюзы? Изолированные среды для ИИ-агентов? Или что-то еще, о чем я пока не думал?

Буду рад услышать ваш опыт. Код, модель угроз и история коммитов открыты на GitHub: https://github.com/Nik0laic4/SchildTCB