Летом 2015 года команда хакеров, нанятых военными, попыталась перехватить контроль за беспилотным вертолетом Little Bird, производства Boeing. На момент начала операции хакеры уже имели частичный доступ к компьютерной системе дрону. Им нужно было лишь сломать технологию управления полетом, установленную на самом устройстве, чтобы полностью перехватить управление.
Отметим, что инструменты группировки Red Team предоставляли возможность так же легко вмешаться в управление вертолетом, как и в любую домашнюю WiFi-сеть. Если бы до этого инженеры DARPA не встроили в «птичку» новый вид защитного механизма — ПО, которое блокирует попытки перехвата управления вертолетом. Red Team имела целых 6 недель и даже доступ к компьютерной сети дрону, чтобы сломать его, но так и не пробилась через защиту Little Bird.
Кейтлин Фишер (Kathleen Fisher), профессор компьютерных наук из Университета Тафтса и менеджер проекта HACMS (High-Assurance Cyber Military Systems), объясняет важность показательного эксперимента с вертолетом:
«— Специалисты могли использовать свои инструменты, имели внутренний доступ, однако, им не удалось перехватить вертолет. Поэтому, в DARPA могут с уверенностью заявлять: они изобрели технологию, которая на самом деле защищает систему от взлома. Теперь можно устанавливать ее в важнейших военных разработках.»
Технология, что не поддалась хакеров, известная среди специалистов как формальная верификация. В отличие от большинства программных кодов, основанных только на принципе, работает или не работает программа, формальная верификация использует математический принцип доказательства. Каждое положение логически следует из предыдущего, а вся программа может быть протестирована по той же схеме, которую используют в математике для доказательства теорем. «Вы пишете математическую формулу, которая описывает заданную работу программы и используете определенный инструмент, который дает возможность проверить правильность такого утверждения», — объясняет Брайан Парно (Bryan Parno), который проводит исследования систем формальной верификации в Microsoft Research.
Инженеры стремились создать программу с формальной верификацией практически с самого начала развития компьютерных наук. Долгое время считалось, что изобрести способ для построения такого ПРОГРАММНОГО обеспечения невозможно, однако за последнее десятилетие т.с. «формальные методы» активно развивались и теперь приблизились к практическому использованию. Сегодня эксперименты с подобными технологиями проводятся в лучших условиях. Примечательно, что для надлежащей финансовой и ресурсной поддержки объединились соперники рынке: военные США и IT-сектор, представленный, в частности, Microsoft и Amazon.
Заинтересованность в создании надежно защищенных программ растет прямо пропорционально перенос в онлайн-пространство важнейших процессов. Раньше, когда компьютеры были установлены в офисах или домохозяйствах, и не были связаны между собой, определенный баг мог принести разве что бытовые неудобства. Сегодня же мы имеем сотни подключенных и соединенных между собой приборов, и малейшая ошибка может привести к уязвимости всей системы. При таких условиях кто с надлежащими знаниями и навыками сможет извне получить контроль не только за приборами, но и за информацией.
Эндрю Аппель (Andrew Appel), профессор из Принстонского университета, руководит программой исследований верификации, объясняет: «В прошлом веке программный баг означал, что программа не будет работать должным образом. Что же, так и будет. Но в XXI веке баг практически включает «зеленый свет» злоумышленникам для кражи ваших персональных данных или вывода из строя сети. С приемлемой ошибки в программе баг превратился в фактор уязвимого места в системе. А это уже намного хуже и непередбачуваніше.»
Мечта о совершенные программы
Кейтлин Фишер руководит экспериментальным проектом HACMS
В октябре 1973 года Едсґейр Дайкстра (Edsger Dijkstra), голландский ученый в области компьютерных наук, увлекся разработкой безошибочного кода, который не будет допускать внешнего вмешательства. Идея привнести в программирование больше математических правил пришла к ученому неожиданно: как вспоминал сам Дайкстра, он проснулся посреди ночи и более часа непрерывно записывал свою теорию. Материал стал основой для книги «Дисциплина программирования» (1976 г.), которая в свою очередь, основала новый принцип разработки программ. Вместе с трудами сэра Тони Хоара (Tony Hoare) эта книга сформулировала концепцию доказательства правильности работы кода, которые должны быть вписаны в саму программу. Оба ученых получили Премию Т’юрінга за свою деятельность в области компьютерных технологий.
Однако концепция, которую сформировали ученые, долгое время не применялась в компьютерной науке. Профессиональное сообщество считала невозможным четко описать функции и работу программы, используя математические правила формальной логики.
Формальная спецификация — это способ описать, что именно делает программа, а формальная верификация — способ доказать, что программный код полностью соответствует заданной спецификации. Представим процесс написания программы для беспилотного автомобиля, который должен доставить пассажира до супермаркета. На операционном уровне, разработчику нужно определить перечень действий, которые может выполнять машина, чтобы выполнить поставленную задачу: повороты влево/ вправо, ускорение или уменьшение скорости, остановка транспорта в пункте назначения.Программа, которую встроят в компьютер машины, будет представлять собой комбинацию всех возможных действий в той последовательности, которая обеспечит прибытие пассажира именно туда, куда нужно — в супермаркет, а не на вокзал.
Самый простой способ проверить работоспособность программы — провести тестирование. Обычно разработчики проводят большое количество модульных тестов с различными исходными данными. Так можно получить программный продукт, который работает должным образом почти в 100% случаев — показатель, вполне приемлемый для большинства программ. Но модульное, или автономное, тестирование не может гарантировать, что программа будет работать должным образом каждый раз, потому что невозможно предсказать и проверить выполнения действия во всех комбинациях дополнительных условий. Даже если вы проверили способность беспилотного авто довести вас до супермаркета в нескольких десятках различных условиях, не исключено, что в нестандартной ситуации, которая не попала в программу тестов, машинное управления даст сбой и приведет к ошибке в системе безопасности. Например, в целевой программе может проявиться незначительная ошибка: алгоритм копирует чуть больший объем данных, чем был задан, и через это в памяти компьютера одни данные записываются на другие.Эту ошибку трудно выявить и ликвидировать, однако она дает возможность хакерам получить доступ к всей системы — все равно, что оставить открытой боковую дверь к защищенной крепости.
«Одно слабое звено в программе превращается в уязвимость защитной системы. А заранее проверить все возможные варианты исходных данных просто нереально», — констатирует Парно. Фактические спецификации для ПО, как правило, более требовательны пример, приведенный выше. Например, нужно написать программу для патентного бюро, которая будет удостоверять документы и присваивать им дату в том порядке, в котором они поступили в базу.В спецификации следует указать, что номера должны присваиваться в порядке возрастания (самые маленькие — старше файлам, а самые большие номера — более новым поступлением), а также, что программа должна хранить ключ для удостоверения документов.
Все это довольно легко можно передать словами, но трудно перевести на формальный язык, которую поймет компьютер — в этом и заключается основная сложность в процессе написания ПО. Парно разъясняет: «Легко приказать кому не разглашать мой пароль. Но чтобы превратить такую команду на математическое определение нужно хорошо напрячься.»
Возьмем другой пример: нужно написать программу для сортировки списка чисел. Разработчик пытается уточнить запрос для будущего кода в формуле:
Убедиться, что каждое число j в перечне соответствует утверждению j ≤ j+1
Однако это условие, что каждое число в списке должно быть меньше или равно следующему числу — также содержит ошибку: разработчик предполагает, что программа просто выполнит перестановку чисел в заданном списке, согласно спецификации. Однако, программа может выдать упорядоченный список с числами, которых не было в исходных данных, но они соответствуют требованию и поэтому были добавлены в список.
Другими словами, в формальной спецификации трудно описать все те требования, при этом, предусмотреть допустимые, но ненужные в конкретном случае значения. Пример с сортировкой чисел довольно понятный, но бывают абстрактные спецификации, тот же защиту пароля. Как объяснить это условие с математической точки зрения? Чтобы четко поставить задачу, придется составить математическое определение понятия «хранить в секрете», в контексте пароля, а также описать, как определяется надежность алгоритма шифрования. «Мы долго искали ответа на подобные вопросы, как и много других специалистов. Но четкие определения найти крайне трудно», — замечает Парно.
Безопасность на основе блоков
Программа с прописанной формальной верификацией, в кодовом определении, может быть в 5 раз длиннее за традиционную, которая была написана для выполнения того же действия. Причина заключается в том, что первые имеют в себе не только спецификации, но и дополнительные аннотации, необходимые для правильной имплементации задачи. Этого осложнения можно избавиться с помощью соответствующих инструментов — языков программирования и систем автоматического доказательства теорем. Они созданы специально, чтобы инженеры могли построить устойчивый к внешним угрозам код. Но в 1970-х годах таких средств еще не изобрели. Профессор Аппель сегодня возглавляет группу разработчиков DeepSpec, которые работают с формально верифицированными системами.Он объясняет, что из-за незрелости компьютерных наук и технологий в 1980 году большинство специалистовпрекратили поиски математического решения вопросов безопасности в коде.
Дальнейшее совершенствование технологий не решило всех вопросов, появилась новая серьезная помеха: исследователи не были уверены в беспрекословном необходимости верификации программ. В то время как энтузиасты формального метода описывали маленький баг в коде, как потенциальную катастрофу, все остальные разработчики видели только системы, которые вполне нормально работали. Конечно, иногда программы «падали», но это приводило лишь к потере последних несохраненных данных, а решением был перезапуск системы.Ради исправления таких незначительных ошибок не хотелось тратить время чтобы тщательно, знак за знаком, переводить каждый фрагмент кода на язык формальной логики. Постепенно даже сторонники метода верификации программ начали сомневаться в его целесообразности. В 1990-х даже Тони Хоар, чья именная «логика Хоара» стала научным фундаментом для конструирования корректных программ, признавал, что трудоемкий процесс определения спецификаций в коде программ может быть сложным решением для проблемы, которой вообще не существует. В 1995 году он написал:
— 10 лет назад исследователи формального метода (среди которых был и я) ошибочно утверждали, что программисты будущего будут благодарны за ту помощь в работе, которую обещал нам метод формализации написания кода… Но оказалось, что никто на самом деле не озабочен проблемой, которую мы так упорно взялись решать с помощью формальной верификации.»
А тут появился интернет, который позволил программным ошибкам в коде распространиться по всему миру. Эффект можно сравнить с распространением инфекционных заболеваний между континентами, благодаря развитию авиационного сообщения. Когда каждый отдельный компьютер по единой Сети подключен к другому, неудобная, но терпимая» ошибка в коде может вызвать цепную реакцию падения систем безопасности данных по всему миру.
«Тогда мы не учли факта, что некоторые системы защиты информации имеют более важную роль, потому что обеспечивают внешнюю защиту от хакеров, — признается Аппель. — И неточность в такой программе гарантированно вызывает уязвимость всей системы безопасности». Когда же специалисты осознали степень угрозы данным в интернете, настало время для возвращения к методу верификации программ. В первую очередь, специалисты взялись за разработку вспомогательных технологий для формальных методов:
- совершенствование систем автоматического доказательства теорем, вроде Coq и Isabelle;
- развитие новых логических систем (теории зависимого типа данных), которые устанавливают пределы поля для разработки кода;
- модернизация т.с. «операционной семантики» — по сути, это язык, в котором есть все необходимые слова для описания того, что должна выполнять программа.
«Если вы беретесь за определение спецификации на английском языке, условно, вы работаете с неопределенной или же многозначительной спецификацией», — разъясняет Жанет Винг (Jeannette Wing), корпоративный вице-президент Microsoft Research. «Любой естественный язык является, по своей сути, многозначной, неконкретной. Используя формальную спецификацию, вы описываете четкие характеристики, базирующиеся на математическом объяснении правильной работы программы.»
В Microsoft Research Жанет Винг работает над созданием протокола формальной верификации для интернета
Кроме вышеуказанных изменений в технологиях, ученые также пересмотрели собственные цели, с которыми разрабатывали формальный метод. В 1970-1980-х гг. они пытались добиться создания полностью проверенных компьютерных систем, от этапа написания схемы управления к конечной программы. Теперь исследователи формального метода сфокусировались на меньших, но наиболее уязвимых до внешнего вмешательства, или же важнейших для безопасности данных фрагментах. В таких критически важных программ относятся операционные системы, криптографические протоколы и тому подобное. Винг уточняет, что исследователи уже понимают: невозможно гарантировать корректной работы программы на 100% в каждом звене написанного кода.
«— Сегодня мы четче осознаем собственные возможности — что мы можем и что не можем сделать.»
Проект HACMS стал доказательством того, как можно усилить безопасность системы, установив особую спецификацию для отдельного фрагмента программы. Первоначально, в рамках проекта планировали создать несокрушимый квадрокоптер. Программное обеспечение тех дронов, которые уже доступны на массовом рынке, было неделимым — если хакеру удастся взломать один из фрагментов кода, он получит доступ ко всей системе. Так, в течение двух лет команда HACMS работала над разделением системы управления аппаратом на отдельные фрагменты. Кроме того, была переписана архитектура ПО — по словам проектного менеджера Фишер, программисты начали использовать т.с. «высоконадежные строительные блоки», которые позволяют подтвердить правильность передачи информации написанным кодом. Один из таких строительных блоков гарантирует, что хакер, получив доступ к одной части программы, не сможет использовать аналогичные инструменты для взлома других составляющих системы.
Именно такое распределенный на части ПО было установлено на вертолет Little Bird. Хакеры из Red Team получили от разработчиков доступ к одной из составляющих частей программы — они управляли камерой беспилотника, но не его основными функциями. Программисты сделали математический расчет, согласно которому хакеры точно не смогут добраться до других фрагментов программы. Практический эксперимент подтвердил верность применения математического подхода. «Это не стало для нас неожиданностью, — констатирует Кейтлин Фишер, — но всегда лучше получить наглядное подтверждение теории.»
За год, прошедший со времени успешных испытаний Little Bird, специалисты DARPA установили разработки HACMS в другие военные системы, спутники и беспилотные грузовики. Появление новых проектов согласуется с значительным прорывом в исследовании формальной верификации, который произошел за последнее десятилетие. И каждая новая разработка подбадривает следующую команду специалистов работать в том же направлении.
Фишер заключает: « Теперь уже никто не может оправдываться тем, что системы формальной верификации — слишком сложны.»
Проверка интернета
Безопасность и надежность — два показателя, на которые ориентируются разработчики формальных методов в программировании. Ежедневно необходимость в усилении надежной защиты информации становится все более очевидной. В 2014 году ошибка в криптографическом программном обеспечении OpenSSL (Heartbleed), теоретически, могла вызвать глобальный сбой в работе Сети. Однако встроенный механизм формальной спецификации смог бы заблаговременно обнаружить этот баг. А 2015-го IT-сообщество пораженно наблюдала, как энтузиасты онлайн-безопасности дистанционно перехватили управление автомобилем Jeep Cherokee.
Цена ошибки в системах безопасности постоянно растет, вместе с увеличением роли онлайн-технологий в современном мире. Поэтому некоторые разработчики, в частности Аппель и команда DeepSpec, снова возвращаются к идее создания гарантированно безопасной системы, от исходного кода до конечного продукта. На этот раз, в отличие от попыток 1970-х годов, специалисты работают над аналогом безопасного веб-сервера, в котором объединятся разрозненные методы формальной верификации, действенность которых уже доказана экспериментально, вроде упомянутой выше программы в вертолете. Главная задача, стоящая перед исследователями сегодня, — создание специфицированного единого интерфейса для всех трудоспособных технологий верификации. Шансы на успех проекта достаточно убедительны, несмотря на тот факт, что Национальный научный фонд США выделил на реализацию замысла грант в размере $10 млн.
В Microsoft Research строят собственные планы на дальнейшую разработку формальной верификации. Один из проектов носит название Everest и заключается в создании верифікованої версии HTTPS. Жанет Винг считает этот протокол Ахиллесовой пятой интернету, а потому его усиление является стратегически важным шагом. Другое направление деятельности специалистов — разработка верифицированных спецификаций для систем, управляемых аппаратами. Дополнительные осложнения вызваны тем, что алгоритм, который управляет тем же дроном, использует машинное обучение. Эта технология отвечает за принятие решений относительно маршрута беспилотника, на основе данных об условиях окружающей среды, которые поступают в режиме реального времени. Все алгоритмы нужно защитить от внешнего вмешательства, и Винг, которая руководит исследованиями, уверена в способности современных инструментов гарантировать безопасность данных. Ведь за последнее десятилетие формальные методы значительно прогрессировали, и все больше первоклассных специалистов развивают это направление.
По материалам: Quanta Magazine
