Amazon проверяет Rust-код AWS формальным верификатором Verus

Amazon Science опубликовала пост о Verus, открытом автоматическом верификаторе программ для Rust. Компания напоминает: Rust предотвращает целый класс ошибок (например, программа аварийно остановится при выходе за границы массива вместо неопределённого поведения, как в C), но это не гарантирует, что код вычисляет именно то, что задумано, и не утекают ли через него секреты. Verus закрывает этот разрыв: разработчик формулирует математическую спецификацию поведения кода, и инструмент механически проверяет, что код соответствует ей для всех возможных входных данных, в отличие от обычного тестирования, которое проверяет лишь отдельные случаи и может пропустить пограничные ситуации.

Спецификации и доказательства пишутся прямо в исходных файлах Rust, Rust-подобным синтаксисом: precondition задаётся ключевым словом "requires" (условия перед выполнением функции), postcondition, "ensures" (условия после). На примере бинарного поиска: precondition требует отсортированный массив, а postcondition уточняет, что если функция вернула Some(index), значение по этому индексу совпадает с искомым, а если вернула None, искомого значения в массиве вообще нет (без этого уточнения спецификации формально удовлетворяла бы и функция, всегда возвращающая None). Обычный компилятор Rust аннотации Verus игнорирует, поэтому такой код совместим с обычной сборкой через Cargo и может использоваться и в верифицированных, и в неверифицированных проектах.

Verus также умеет доказывать корректность "небезопасного" (unsafe) Rust-кода, того, где компилятор перестаёт механически проверять соблюдение правил безопасности, восстанавливая для него машинно проверяемые гарантии. Для конкурентного кода Verus позволяет навешивать на блокировки (locks) инвариант: любой, кто захватывает блокировку, получает значение, удовлетворяющее этому свойству, и обязан доказать, что оно сохраняется при освобождении блокировки; поддерживаются и доказательства корректности самой реализации блокировки.

Amazon, один из основателей Rust Foundation и больше десяти лет занимается автоматическими рассуждениями (automated reasoning); использует Rust в Firecracker (на нём работают AWS Lambda и AWS Fargate), в распределённой SQL-базе и в Nitro Isolation Engine, компоненте, который обеспечивает изоляцию виртуальных машин для гипервизора Nitro, управляющего распределением виртуальных машин в AWS. По словам компании, с помощью Verus уже доказана корректность ключевых примитивов Nitro Isolation Engine и ряда других критических внутренних компонентов; подробности обещаны в будущих постах. Verus способен верифицировать проекты из тысяч строк кода и доказательств за время, за которое некоторые прежние автоматические верификаторы проверяли лишь отдельные функции; разработчики обычно получают обратную связь по коду и доказательствам менее чем за секунду, что позволяет работать в интерактивном режиме прямо в редакторе (включая подсветку ошибок вроде "красных загогулин" в VS Code). Amazon отмечает, что многие рутинные, низкоуровневые шаги построения доказательства Verus автоматизирует сам, а высокоуровневые шаги (например, построение индуктивного доказательства или подсказка инварианта цикла) в последнее время всё чаще может брать на себя ИИ, при этом конкретные инструменты или модели для этого в посте не названы.

Помимо Amazon, Verus используется в ряде открытых проектов: Vest (генерирует Rust-код для парсинга и сериализации бинарных форматов данных с доказательствами корректности и безопасности), Verdict (библиотека проверки сертификатов x.509 с поддержкой пользовательских политик валидации), CapybaraKV (верифицирует корректность и устойчивость к сбоям логов в энергонезависимой памяти), микроядро Atmosphere, Anvil (доказывает корректность и "живучесть" контроллеров Kubernetes, что при разумных допущениях они приводят систему в стабильное состояние) и CortenMM (система управления памятью с транзакционным интерфейсом и масштабируемыми протоколами блокировок). Сам Verus, бесплатный проект с открытым исходным кодом, который развивает распределённое сообщество академических и индустриальных исследователей. Как и у любого верификатора программ, гарантии Verus опираются на корректность самого инструмента, на верхнеуровневые спецификации, на допущения о нижележащей рантайм-среде (например, о стандартной библиотеке Rust) и на цепочку инструментов компиляции; Amazon обещает в будущих постах подробнее рассказать, как повышает уверенность именно в этих компонентах.

Ключевые факты

Verus, открытый автоматический верификатор Rust-кода: разработчик пишет математическую спецификацию поведения функции, а инструмент механически доказывает, что код ей соответствует для всех возможных входных данных, а не только для протестированных случаев.
Спецификации и доказательства пишутся прямо в исходных файлах на Rust-подобном синтаксисе ("requires"/"ensures"); обычный компилятор Rust эти аннотации игнорирует, поэтому код остаётся совместимым с Cargo и обычной сборкой.
Verus умеет доказывать корректность небезопасного (unsafe) Rust-кода и конкурентного кода с блокировками, включая корректность самой реализации блокировки.
Amazon применяет Verus, чтобы доказать корректность ключевых примитивов Nitro Isolation Engine (изоляция виртуальных машин в AWS) и ряда других внутренних критических компонентов; разработчики получают обратную связь по доказательствам менее чем за секунду.
Кроме Amazon, Verus используют открытые проекты Vest, Verdict, CapybaraKV, микроядро Atmosphere, Anvil (контроллеры Kubernetes) и CortenMM.

Почему это важно

Тип-система Rust уже отсекает целый класс ошибок памяти и часть проблем параллелизма, но она не проверяет, что программа делает именно то, что задумано, и не гарантирует отсутствие утечки секретов. Verus закрывает этот пробел: он берёт формальную спецификацию поведения кода и математически доказывает, что реализация ей соответствует для всех возможных входных данных, а не только для тех случаев, что покрыты тестами. Для инфраструктуры уровня AWS, где Amazon уже применяет Verus к Nitro Isolation Engine, обеспечивающему изоляцию виртуальных машин, такая гарантия существенно надёжнее обычного тестирования и типовых проверок компилятора.

Кому это важно

В первую очередь, разработчикам на Rust, которые пишут код с высокими требованиями к безопасности и корректности: производители облачной инфраструктуры и гипервизоров, авторы криптографических и сетевых библиотек, разработчики конкурентного и небезопасного (unsafe) кода. В посте прямо названы примеры за пределами Amazon: библиотека парсинга бинарных форматов Vest, библиотека проверки x.509-сертификатов Verdict, хранилище CapybaraKV, микроядро Atmosphere, контроллеры Kubernetes в проекте Anvil и система управления памятью CortenMM.

Как это применить

Verus, бесплатный проект с открытым исходным кодом. Специфика и доказательства добавляются прямо в исходные файлы Rust Rust-подобным синтаксисом: ключевое слово "requires" задаёт условия перед выполнением функции, "ensures", условия после. Обычный компилятор Rust эти аннотации игнорирует, поэтому Verus-код можно собирать стандартным Cargo и использовать как в верифицированных, так и в обычных проектах. Обратная связь по коду и доказательствам приходит обычно менее чем за секунду, что позволяет работать в интерактивном режиме прямо в редакторе (в том числе с подсветкой ошибок вроде "красных загогулин" в VS Code); при этом Verus способен верифицировать проекты из тысяч строк кода и доказательств.

Можно ли доверять

Материал опубликован на официальном научном блоге Amazon и написан от корпоративного "мы", без указания конкретного автора. Заявления о применении Verus внутри AWS, например, о доказанной корректности примитивов Nitro Isolation Engine, исходят от самой компании и не сопровождаются независимой проверкой, конкретными датами или измеримыми показателями; сравнение с "прежними автоматическими верификаторами" дано качественно (тысячи строк за время, требовавшееся тем на отдельные функции), без цифр. При этом список сторонних открытых проектов, использующих Verus (Vest, Verdict, CapybaraKV, Atmosphere, Anvil, CortenMM), проверяем и не зависит от слов Amazon.

Риски и подводные камни

Формальная верификация доказывает лишь соответствие кода заявленной спецификации, если сама спецификация неверна или неполна, доказанная "корректность" ничего не гарантирует по существу. Как отмечает и сам пост, гарантии Verus в конечном счёте опираются на корректность самого инструмента Verus, на допущения о нижележащей рантайм-среде (включая стандартную библиотеку Rust) и на цепочку инструментов компиляции, то есть на набор доверенных компонентов, которые сами не верифицированы этим же инструментом. Упоминание, что часть высокоуровневых шагов построения доказательств "в последнее время всё чаще может автоматизировать ИИ", не раскрыто: ни конкретный инструмент, ни модель, ни степень надёжности такой автоматизации в посте не названы.