Формальная проверка: разрыв между идеальным кодом и реальностью

Осенью 2017 года я взял 6.826 Массачусетского технологического института - «Принципы компьютерных систем», преподаваемую лауреатом премии Тьюринга Батлером Лампсоном, Николаем Зельдовичем и Франсом Каашоком. Несмотря на свое рудиментарное название, это класс для создания официально проверенных систем. Используя язык доказательства Coq, мы написали спецификации, реализации и доказательства toy-структур: переизданный диск, атомную пару блоков и реплицированный диск. Мы также читаем немало работ из самых современных формальных методов.

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

Попробуйте - осмельтесь

Во-первых, давайте поговорим о том, как мы получаем систему, которую мы можем штамповать как «официально подтвержденную».

Симуляционные доказательства

Существует два широких способа написания официально подтвержденной системы. Первый, более традиционный способ включает в себя тщательное построение спецификаций поведения системы, внедрение системы, а затем вручную написание доказательств, что реализация соответствует спецификации. Все это написано на языке доказательства теоремы, таком как Coq, а затем извлечено в OCaml или Haskell для выполнения исполняемой версии.

Из личного опыта с 6,826 лабораториями это кошмар.

Во-первых, доказательная нагрузка огромна - для файловой системы FSCQ MIT, разработанной около 1,5 лет с использованием Coq, полная система была в 10 раз больше кода, чем аналогичная непроверенная файловая система. Представьте себе, что - 2000 строк реализации станут 20 000 строк доказательств! Частично это объясняется тем, что Coq - очень общий язык для рассуждений о математической логике, и он имеет мало встроенных механизмов для специализированных приложений, таких как сложные компьютерные системы. Таким образом, нам нужно строить инфраструктуру с нуля, а также определять наши системы с нуля - от бит и байтов до целых дисков.

Лаборатории были в значительной степени избавлены от этой смешной бремени бремени из-за большого количества автоматизации и инфраструктуры, предоставляемых инструкторами. Действительно, 2700 строк Coq (LoC) посвящены доказательной инфраструктуре, а в случае игрушечной дисковой лаборатории - еще 1500 строк для реальной системы.

Откуда берутся все эти накладные расходы? Ну, нам нужно поддерживать так называемое «симуляционное доказательство». В этом стиле доказательств мы проходим через каждую процедуру в нашей системе и показываем, что каждое достижимое состояние в нашей реализации имеет соответствующее состояние в нашей спецификации. Наша спецификация для каждой процедуры содержит три условия - предварительное условие , постусловие и условие сбоя , которое верно, если наш код внезапно падает. Тогда наше доказательство включает в себя несколько вещей:

  1. Установить, что предварительное условие нашей процедуры
  2. Докажите, что каждая строка / ветвь процедуры является допустимым переходом
  3. Если в конце выполнения нет сбоев, докажите, что условие постусловия
  4. Если сбои произошли до завершения выполнения, то докажите, что условие сбоя выполняется перед каждым сбоем, процедура восстановления после сбоя является допустимым переходом, а посткондиционирование заканчивается

Вот диаграмма одного перехода, показывающая соответствие между состоянием кода и состоянием спецификации. Двойные стрелки - это то, что нам нужно доказать.

spec semantics

forall state ===================> exists state'

^ ^^

| ||

V code semantics VV

forall w -----------------------> forall w'

В коде FSCQ 6000 из 32 000 LoC были предназначены только для этой инфраструктуры.

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

Есть ли другой способ, спросите вы, прежде чем стрелять в себя?

Кнопочные документы

Другой способ - это «кнопочный» стиль, который формулирует состояния спецификации и реализации как символические уравнения SMT, которые могут быть переданы решателю, например Z3. Это позволяет Z3 автоматически проверять систему, не записывая никаких ручных доказательств. Z3 может, например, проверить, удовлетворяет ли каждая операция кода формулой, определяющей взаимосвязь между состояниями кода и спецификации.

Основное усилие здесь - продуманное проектирование набора проверяемых спецификаций, который фактически масштабируется. Трудно определить, является ли проблема приемлемой для Z3, и вы должны играть всевозможные трюки, чтобы заставить ее работать. Например, авторы Yggdrasil, проверенной файловой системы с кнопочной проверкой, провели 4 месяца, изучая способы масштабирования проверки, 2-3 месяца, построив свою систему, и по крайней мере еще 6 месяцев экспериментировали с оптимизацией . В конце концов, среди других диких трюков, они полагаются на стек пятислойных абстракций, поэтому решатель должен только рассуждать о одном слое за раз и не застревает.

Что пошло не так?

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

Гарантии официально проверенной системы полностью зависят от допущений системы, включая ее доверенную вычислительную базу (TCB). TCB проверенной системы включает спецификации, которые вручную записываются и надеются (скрещенные пальцы!), Чтобы быть правильными, инструменты проверки (например, механизм Coq, Z3, компилятор) и инфраструктура времени выполнения (ОС, аппаратное обеспечение). Это должен быть огромный красный флаг. Например, если вы использовали Z3, вы согласитесь, что это черная магия для всех, кроме разработчиков, и мои профессора признаются, что обнаружили ошибки корректности, особенно в теориях разрешимости, которые обычно не используются.

Эмпирическое исследование

В одной из статей, которые мы читаем, «Эмпирическое исследование правильности формально проверенных распределенных систем», тщательно анализируются три недавно прошедшие официальную проверку распределенные системы - два были Coq / OCaml, а третий был Dafny / SMT. В абстракте говорится все:

Благодаря проверке и тестированию кода мы обнаружили в общей сложности 16 ошибок, многие из которых приводят к серьезным последствиям, включая аварийные серверы, возврат неверных результатов клиентам и недействительность гарантий проверки. Эти ошибки были вызваны нарушениями широкого диапазона допущений, на которые полагались проверенные компоненты.

Среди других серьезных последствий - командная инъекция и потеря данных , предположительно формально проверенные системы!

Я хочу обсудить некоторые из этих ошибок, в том числе, где и как они были найдены.

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

11 произошло то, что авторы называют слоем прокладки , интерфейсом ОС, который включает в себя системные вызовы и другие примитивы. Когда проверенные компоненты не точно моделируют реализацию ОС реального мира, возникают серьезные ошибки. Например, не избежать метасимволов или не обрабатывать все возможные коды ошибок syscall, вызвало неправильные результаты, что привело к вводу команд и потере данных. Реальные ограничения ресурсов, такие как слишком большие пакеты или исчерпание стека, также нарушили предположения и разбили или повесили распределенную систему.

Остальные ошибки были вызваны неполными или неправильными спецификациями и критическими проблемами с самими инструментами проверки. В частности, эти провайдеры не были отказоустойчивы - SIGINTsисключения или другие сбои с верификатором заставили бы проверителя сообщить, что проверка прошла успешно!

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

KRACK и CompCert

Большими новостями в октябре стала атака KRACK на защищенные WPA2 WiFi-сети. Криптограф Мэтт Грин подводит итог. Две части WPA2 - четырехстороннее рукопожатие и протокол шифрования - имеют защитные доказательства; 4-стороннее рукопожатие было даже официально подтверждено в 2005 году Тем не менее, никто не рассуждал о том, как эти две части взаимодействовали в реальном коде, что приводит к тому, что почти каждая реализация на планете уязвима для катастрофической атаки на повторное использование ключей, которая может привести к полному расшифровке и подделке трафика WiFi.

Меньшей проблемой является недавняя ошибка синтаксического анализа в CompCert, формально проверенном компиляторе C. Выпущена ошибка в любительской области, где переменная, объявленная в области forцикла, сбивает глобальную переменную с тем же именем.

Хотя в документе CompCert явно указано, что шаг синтаксического анализа, а также шаги сборки / компоновки не проверены, такая ошибка является огромным ударом по авторитету формальных методов. Это действительно заставляет задуматься о том, какие ошибки должна быть проверена формальной проверкой.

Есть надежда?

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

В эмпирическом исследовании ошибок при внедрении сложных и подверженных ошибкам распределенных протоколов (Paxos, RAFT) не обнаружено. Это показывает, что проверка может быть применена для повышения надежности. И в отчете о поиске ошибок компилятора Джона Реджера сообщалось, что CompCert не обнаружил ошибок кода неправильного кода , которые были найдены в 10 других компиляторах.

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

Суть в том, что формальные методы будут томиться в академических кругах, неспособных преодолеть разрыв с реальным, бессмысленным миром в течение долгого времени.