Granite: как формальная верификация процессоров борется с утечками через временные побочные каналы

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

Если программа не зависит от секретов по времени выполнения, процессор, проверенный через Granite, гарантированно не сольёт эти секреты через архитектурные побочные каналы — даже если в конвейере есть спекулятивное исполнение и прерывания.

Проблема, которую все знают, но мало кто решает

Тема аппаратных утечек через побочные каналы — давняя головная боль индустрии. Процессоры устроены сложнее, чем предписывает их ISA (набор команд): конвейер, предсказание ветвлений, спекулятивное исполнение, буферы — всё это создаёт нюансы в тайминге, которые можно использовать для извлечения секретной информации. Классические атаки Spectre и Meltdown это наглядно продемонстрировали.

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

Что такое Granite

Именно сюда приходят авторы новой работы — Стелла Лау, Андрес Эрбсен и Адам Хлипала, — публикуя на arXiv техническую статью «Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts». Партнёрский альянс MIT, Google и Вашингтонского университета не случаен: здесь соединились компетенции в формальной верификации, промышленном hardware-дизайне и системной безопасности.

Granite — это методология модульной верификации RTL-процессоров, которая проверяет одновременно две вещи:

• Функциональную корректность — процессор действительно выполняет инструкции в соответствии со спецификацией ISA.
• Отсутствие утечек (nonleakage) — процессор не выдаёт секретную информацию через временные побочные каналы.

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

Как это работает

Центральный результат работы звучит так: тактовая точность пайплайнизированного RISC-дизайна — со спекуляцией, точными прерываниями и вводом-выводом — определяется исключительно наблюдаемыми величинами, указанными в контракте утечек ISA.

Если перевести это на человеческий: формально доказано, что никакие скрытые микроархитектурные детали (кроме тех, что явно объявлены в спецификации) не влияют на видимое программе поведение процессора по времени.

Для программ, следующих принципу криптографической константности времени (cryptographic constant-time discipline) — то есть написанных так, чтобы время их выполнения не зависело от секретных данных — этот результат полностью исключает утечку информации через известные и неизвестные временные побочные каналы.

Представьте себе: если вы написали код так, что он не ветвится по секретам и не обращается к памяти по секретным адресам, то RTL-реализация процессора, проверенная через Granite, гарантированно не скомпрометирует ваши данные через тайминг. Это не эвристический аргумент и не результат тестирования — это математическое доказательство.

Почему это важно на практике

У Granite есть несколько практических следствий, которые стоит выделить:

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

Формальная верификация вместо тестирования. Напомним: тестирование может показать наличие бага, но не может доказать его отсутствие. Формальная верификация, наоборот, даёт доказательство. Granite предлагает инструмент, который способен масштабироваться на реальные RISC-процессоры.

Модульность как путь к масштабированию. Предыдущие работы в области формальной верификации hardware часто страдали от проблемы «не проходит на реальном размере». Модульный подход Granite позволяет верифицировать отдельные блоки конвейера, а потом собирать доказательство — это открывает дорогу к применению на более сложных дизайнах.

Оговорки и перспективы

Стоит отметить несколько нюансов. Во-первых, Granite работает с RISC-архитектурами — а они заведомо проще CISC-процессоров. Распространить подход на, скажем, x86 с его сложнейшей микроархитектурой — задача совершенно другого порядка.

Во-вторых, гарантия Granite работает в связке с программным обеспечением, написанным по принципу константности времени. Если код не соблюдает эту дисциплину — скажем, использует зависимые от секрета ветвления — то и формальная верификация железа не спасёт.

В-третьих, статья пока опубликована на arXiv (июль 2026) и проходит рецензирование. Технические детали доказательств потребуют времени на проверку сообществом, но сам факт участия Google в исследовании намекает на практическую значимость результатов.

Для индустрии, которая после атак Spectre в 2018 году до сих пор занимается בעיקר паллиативными мерами в виде патчей и отключений фич, Granite — это попытка подойти к проблеме фундаментально. Не исправлять утечки постфактум, а доказать их отсутствие на этапе проектирования. Идея не новая, но её реализация на уровне RTL с модульной верификацией — шаг вперёд, который заслуживает внимания.