[Перевод] Невзламываемый код существует
Специалисты по информатике могут доказать отсутствие ошибок в программе с такой же уверенностью, с какой математики могут доказывать теоремы. Эти достижения используются для повышения безопасности в разных областях, от беспилотников до интернета.
Весною 2015 года команда хакеров пыталась взломать беспилотный военный вертолёт под названием Little Bird («Птичка»). Вертолёт, схожий с пилотируемой версией любимого спецназом США летательного аппарата, находился на территории компании Boeing в Аризоне. У хакеров была фора: в начале их работы они обладали доступом к одной из подсистем управляющего компьютера. Им оставалось лишь взломать основной бортовой полётный компьютер и получить контроль над БПЛА.
В самом начале проекта команда хакеров «Red Team» могла взломать систему вертолёта почти так же просто, как ваш домашний WiFi. В последующие месяцы инженеры DARPA применили новый механизм безопасности, программную систему, не подверженную насильственной экспроприации. Ключевые параметры системы Little Bird невозможно взломать при помощи существующих технологий, а её коду можно доверять, как математическим доказательствам. И хотя команде дали шесть недель доступа к БПЛА, и доступ к компьютерной системе превышал возможности доступа реальной команды хакеров, они не смогли взломать защиту «Птички».
«Они не смогли взломать или нарушить ход операции»,- говорит Кэтлин Фишер, профессор информатики из Университета Тафтса и управляющая проектом «высоконадёжных военных киберсистем» (High-Assurance Cyber Military Systems, HACMS). «В результате представители DARPA встали и сказали, о, боже мой, вы на самом деле можем использовать такую технологию в важных системах».
Технология, противостоящая хакерам, это стиль программирования под названием формальное подтверждение. В отличие от обычного кода, написанного неформально и оцениваемого обычно только по его работоспособности, формально подтверждённое ПО выглядит, как математическое доказательство: каждое утверждение логически вытекает из предыдущего. Всю программу можно проверить с той же уверенностью, что и математическую теорему.
«Вы пишете математическую формулу, описывающую поведение программы и, используя инструмент для проверки доказательства, который проверяет правильность этого утверждения»,- говорит Брайан Парно, исследующий формальное подтверждение и безопасность в Microsoft Research.
Стремление создавать формально подтверждённые программы существовало почти так же давно, как и сама область информатики. И очень долго это оставалось невозможным, но достижения прошедших десяти лет в области «формальных методов» подвинули этот подход ближе к общепринятой практике. Сегодня формальное подтверждение ПО изучают в получающих финансирование академических группах, в военных проектах США и технологических компаниях, например, Microsoft и Amazon.
Интерес возрастает вместе с увеличением количества жизненно важных задач, проходящих через онлайн. Когда компьютеры изолированно существовали в домах и офисах, ошибки программирования были лишь неудобством. Теперь же они открывают дыры в безопасности на машинах в сети, позволяющие любым сведущим людям проникать в компьютерные системы.
«В ХХ-м веке, когда у программы была ошибка, это было плохо, она могла упасть, ну и бог с ней»,- говорит Эндрю Аппель [Andrew Appel], профессор информатик из Принстонского университета и лидер в области подтверждения программ. Но в ХХI-м веке ошибка может открыть «хакерам путь для получения контроля над программой и кражи ваших данных. Из терпимой ошибки она превратилась в уязвимость, что намного хуже»,- говорит он.
Кэтлин Фишер
В октябре 1973 года Эдсгер Дейкстра придумал идею создания кода без ошибок. Ночью, находясь в отеле на одной из конференции, он вдруг подумал о том, как сделать программирование более математическим. Объясняя идею позже, он сказал «С возбуждённым сознанием я вылез из постели в 2:30 утра, и писал более часа». Этот материал стал началом его плодотворной книги 1976 года «Дисциплина программирования», которая вместе с работами Чарльза Хоара (подобно Дейкстре, получившего премию Тьюринга), определила взгляды на использование доказательства правильности при написании программ.
Но информатика не последовала вслед за этой идеей, в основном потому, что в течение многих лет казалось непрактичным, или даже невозможным, определять функцию программы при помощи правил формальной логики.
Формальное определение — это способ определить то, что конкретно делает программа. Формальное подтверждение — способ доказать без всяких сомнений, что программный код идеально соответствует этому определению. Представьте, что вы пишете программу для робомобиля, везущего вас к продуктовому магазину. На уровне операций вы определяете движения, которыми располагает робомобиль для достижения цели — он может поворачивать, тормозить или ускоряться, включаться или выключаться в начале и конце пути. Ваша программа будет состоять из этих основных операций, построенных в нужном порядке так, чтобы в итоге вы приехали к магазину, а не в аэропорт.
Традиционный способ проверки работоспособности программы — это тестирование. Программисты дают программе много данных на вход (юнит-тесты), чтобы убедиться, что она ведёт себя, как надо. Если ваша программа задаёт алгоритм движения робомобиля, можно протестировать её поездки между множеством разных точек. Такое тестирование обеспечивает корректную работу программ в большинстве случаев, чего достаточно для большинства приложений. Но юнит-тесты не гарантируют, что ПО будет всегда работать правильно — нельзя проверить программу на всех возможных входных данных. Даже если алгоритм сработает для всех пунктов назначения, всегда есть возможность, что она поведёт себя не так в редких условиях — или, как говорят, в «граничных условиях» — и откроет дыру в безопасности. В реальных программах такие ошибки могут быть простыми, например, переполнение буфера, при котором программа копирует чуть больше данных, чем надо, и перезаписывает часть памяти компьютера. Такую по виду безвредную ошибку тяжело устранить, и она обеспечивает дыру для хакерской атаки — слабая дверная петля, открывающая путь в замок.
«Одна дыра где-либо в софте, и это уже уязвимость. Очень сложно проверить все пути для всех возможных входных данных»,- говорит Парно.
Настоящие спецификации сложнее, чем поездка в магазин. Программистам, например, может понадобиться программа, нотариально заверяющая и проставляющая дату получения документов в порядке их получения. В этом случае спецификация должна указывать, что счётчик всегда увеличивается, и что программа никогда не должна допускать утечку ключа, используемого для подписи.
На человеческом языке это описать легко. Превратить спецификацию в формальный язык, понятный компьютеру, гораздо тяжелее — что и объясняет основную проблему написания программ.
«Состряпать формальную спецификацию, понятную для компьютера, сложно по сути,- говорит Парно. — Легко на верхнем уровне сказать «не допускай утечек пароля», но нужно подумать, как превратить это в математическое определение».
Другой пример — программа, сортирующая список номеров. Программист в попытках формализовать спецификацию для неё может придумать такое:
Для каждого пункта j в списке убедиться, что j ≤ j + 1
Но и в этой формальной спецификации — убедиться, что каждый элемент в списке меньше или равен следующему — есть ошибка. Программист подразумевает, что выходные данные будут содержать изменённые входные. Если список [7, 3, 5], он ожидает, что программа вернёт [3, 5, 7]. Но вывод программы [1, 2] удовлетворит спецификации — поскольку «это тоже отсортированный список, но только не тот список, которого вы, наверное, ожидали»,- говорит Парно.
Иначе говоря, тяжело превратить идею того, что должна делать программа, в формальную спецификацию, исключающую любую неправильную интерпретацию того, чего вы хотите от программы. И приведённый пример описывает простейшую программу сортировки. Теперь представьте описание чего-то гораздо более абстрактного, например, защиту пароля. «Что это значит математически? Для такого определения может понадобиться записать математическое описание того, что означает «хранить секрет», или, что означает для алгоритма шифрования быть безопасным,- говорит Парно. — Все эти вопросы мы рассматривали, и продвинулись в их изучении, но они могут быть чрезвычайно хитры для реализации».
По сути, необходимо написать как спецификации, так и дополнительные комментарии, необходимые для того, чтобы ПО могло делать заключения о коде. Программа, включающая её формальное подтверждение, может в пять раз превышать размер обычной программы, написанной с той же целью.
Эту ношу можно немного облегчить при помощи подходящих инструментов — языков программирования и вспомогательных программ, помогающих программистам создавать пуленепробиваемые программы. Но в 1970-х их не существовало. «Многие аспекты науки и технологии тогда ещё не выросли достаточно, поэтому к 1980-м многие области информатики потеряли к этому интерес»,- говорит Аппель, ведущий исследователь группы DeepSpec, разрабатывающей формально подтверждённые компьютерные системы.
Несмотря на улучшение инструментов, на пути подтверждения программ возник ещё один барьер: не было уверенности в том, что оно вообще было нужно. Хотя энтузиасты метода говорили о том, что небольшие ошибки могут приводить к большим проблемам, остальные обращали внимание на то, что в основном компьютерные программы работают достаточно неплохо. Иногда падают, да –, но потерять немножко несохранённых данных, или иногда перезапускать систему кажется небольшой платой за отсутствие необходимости кропотливо переводить каждый кусочек программы на язык формальной логики. Со временем даже те, кто находился у истоков программного подтверждения, начали сомневаться в его пользе. В 1990-х даже Хоар признал, что спецификации могут быть трудозатратным решением несуществующей проблемы. В 1995 он писал:
Десять лет назад исследователи формальных методов (а среди них я ошибался сильнее всего) предсказывали, что мир программирования с благодарностью примет помощь формализации… Оказалось, что мир недостаточно сильно страдал от проблем, которые наше исследование пыталось решать.
Потом появился интернет, который сделал для ошибок в коде то же, что авиаперелёты сделали для инфекций: когда все компьютеры связаны друг с другом, неудобные, но терпимые ошибки могут привести к нарастающим проблемам безопасности.
«Мы вот что не полностью понимали,- говорит Аппель. — Существуют программы, открытые всем хакерам интернета, и если в такой программе есть ошибка, она может стать уязвимостью».
К тому времени, когда исследователи начали понимать серьёзность угроз для безопасности, представляемых интернетом, подтверждение программ было готово вернуться. Для начала исследователи достигли прогресса в фундаментальных частях формальных методов. Это улучшение вспомогательных программ, таких, как Coq и Isabelle; разработка логических систем (теории зависимых типов), обеспечивающих платформу разработки, помогающую компьютерам оценивать код; «операционная семантика» — язык, обладающий правильными словами, позволяющими выразить то, что требуется от программы.
«Начиная со спецификации на человеческом языке, вы сталкиваетесь с двусмысленностями,- говорит Джанетт Винг, вице-президент Microsoft Research. — Любой естественный язык содержит двусмысленности. В формальной спецификации вы записываете точное описание на основе математики, для объяснения того, что вы хотите от программы».
Джанетт Винг из Microsoft Research
Кроме того, исследователи формальных методов пересмотрели свои цели. В 1970-х и 1980-х они хотели создать полностью проверенные компьютерные системы, от электронных схем до программ. Сегодня большинство исследователей работают над небольшими, но наиболее критичными или уязвимыми частями систем — например, над операционными системами или криптографическими протоколами.
«Мы не утверждаем, что докажем корректность всей системы на 100%, вплоть до электронных схем,- говорит Винг. — Такие заявления нелепы. Мы точны в том, что мы можем или не можем сделать».
Проект HACMS показывает, как можно достичь больших гарантий безопасности, описав одну небольшую часть компьютерной системы. Первой целью проекта было создание невзламываемого квадрокоптера для развлечений. Шедшее в комплекте с квадриком ПО было монолитным — то есть, получив доступ к одной его части, хакер получал доступ ко всем остальным. Два года команда HACMS занималась разделением кода в управляющем компьютере на части.
Команда переписала архитектуру ПО, используя то, что Фишер называет «строительными блоками высокой уверенности» — инструменты, позволяющие программистом доказывать чистоту кода. Один из них обеспечивает доказательство того, что получив доступ в одну из частей, нельзя путём эскалации привилегий добраться до остальных.
Позднее программисты установили такой софт на «Птичку». В тесте с командой Red Team ей предоставили доступ в одну из частей системы, контролировавшей какую-то часть вертолёта, например, камеру –, но не основные функции. Неудача хакеров была математически гарантирована. «Они доказали машинно-проверяемым способом, что хакеры не смогут выйти за пределы раздела системы, так что это неудивительно, — говорит Фишер. — Это совпадает с теоремой, но всегда полезно провести проверку».
В последующий за проверкой год DARPA применяла инструменты и технологии проекта к другим областям военной технологии, например, к спутникам и автоматическим грузовикам. Новые инициативы совпадают с тем, как формальное подтверждение распространялось в последние десять лет: каждый успешный проект поощряет следующий. «Отговорки на тему сложности этого принципа уже не проходят»,- говорит Фишер.
Безопасность и надёжность — две основных цели, вдохновляющих формальные методы. С каждым днём необходимость в улучшениях становится всё более очевидной. В 2014-м году небольшая программная ошибка, которую формальное описание словило бы, открыло путь для ошибки Heartbleed, грозившей сломать интернет. Через год парочка «легальных» хакеров подтвердила худшие опасения по поводу автомобилей, подключённых к интернету, получив удалённый контроль над Jeep Cherokee.
С повышением ставок исследователи формальных методов ставят всё более амбициозные цели. Группа DeepSpec под руководством Аппеля (также работавшего над HACMS) пытается построить такую сложную полностью проверенную систему, как веб-сервер. В случае успеха проект, получивший грант от Государственного научного фонда в $10 миллионов, соберёт вместе множество меньших успешных проектов последнего десятилетия. Исследователи создали несколько подтверждённых безопасных компонентов вроде ядра операционной системы. «Чего пока не было сделано, так это объединения этих компонентов по имеющим спецификации интерфейсам»,- говорит Аппель.
В Microsoft Research у программистов есть два амбициозных проекта. Первый, Everest, стремится создать подтверждённую версию HTTPS, протокола, обеспечивающего безопасность веб-браузеров, который Винг называет «ахиллесовой пятой интернета».
Второй — создание подтверждённых спецификаций сложных кибер-физических систем, таких, как БПЛА. У проекта существуют значительные сложности. В то время как обычные программы работают с отдельными недвусмысленными этапами, программы, управляющие движением дронов, используют машинное обучение для принятия вероятностных решений, основанных на непрерывном потоке данных об окружении. Далеко не очевидно, как можно принимать логические решения с такой степенью неточности, или описать их в виде формальной спецификации. Но только за последние десять лет формальные методы продвинулись довольно далеко, и Винг, управляя проектом, оптимистично считает, что исследователи смогут решить все эти проблемы.
