Позволит ли формальная верификация кода микроядра создавать сверхнадежные ОС
В 2015 году американская компания Rockwell Collins совместно с Boeing и 3D-Robotics провела испытания устойчивых ко взлому квадрокоптера Iris и беспилотного вертолёта Little Bird со «сверхнадежной» операционной системой.
Разработка защищённых от взлома дронов ведётся по заказу Агентства перспективных оборонных проектов (DARPA) Министерства обороны США, которое заинтересовано в защите перспективных беспилотных и опционально пилотируемых летательных аппаратах от возможных уязвимостей.
Существует как минимум три способа взлома беспилотных летательных аппаратов: первый — получение доступа к управлению посредством взлома канала связи или подмены данных авторизации, второй — использование уязвимостей программного обеспечения, третий — использование интерфейсов и каналов данных оригинального программного обеспечения для загрузки вредоносного кода.
Разработанная Rockwell Collins операционная система на базе микроядра seL4 устойчива ко всем трём типам взлома. Операционная система на базе seL4 изначально ориентирована в первую очередь на безопасность. По-английски это называется красивым словосочетанием «hackproof» (взломоустойчивая).
Её особенностью является устойчивое к подменам кода ядро, которое использует математические алгоритмы и контрольные суммы для проверки запущенных служб, а также обеспечивает раздельное выполнение процессов.
Система позволяет запустить виртуальную машину, в которой гостевая программа не получает доступа к основным процессам или аппаратной части. При запуске программы сообщают ядру контрольные суммы, на основе которых производится исправление ошибок или закрытие несанкционированных процессов.
Испытания прошли успешно: специалистам по кибербезопасности не удалось запустить вредоносный код на беспилотных аппаратах с защищённой операционной системой, а также перехватить управление дроном или вызвать системный сбой.
Микроядро seL4 используется не только в авиации, но и в медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев.
Важная особенность архитектуры seL4 — вынос частей для управления ресурсами ядра в пространство пользователя и применения для этих ресурсов тех же средств разграничения доступа, что и для ресурсов пользовательских. Микроядро не предоставляет готовых высокоуровневых абстракций для управления файлами, процессами, сетевыми соединениями и так далее.
Вместо этого оно предоставляет лишь минимальные механизмы для управления доступом к физическому адресному пространству, прерываниям и ресурсам процессора.
Высокоуровневые абстракции и драйверы для взаимодействия с оборудованием реализуются отдельно — поверх микроядра в форме задач, выполняемых на пользовательском уровне. Доступ таких задач к имеющимся у микроядра ресурсам организуется через определение правил.
Для программистов существует компоненто-ориентированная платформа разработки приложений CAmkES, позволяющая моделировать и создавать системы на основе seL4 в виде коллекции взаимодействующих между собой компонентов.
С seL4 генетически связан проект L4.verified — формально верифицированное ядро на архитектуре L4.
L4 — микроядро второго поколения, разработанное Йохеном Лидтке в 1993 году.Архитектура микроядра L4 оказалась успешной. Было создано множество реализаций ABI и API микроядра L4. Все реализации стали называть «семейством микроядер L4». Так появился и seL4. А реализация Лидтке неофициально была названа «L4/x86».
Основная идея L4.verified, как и seL4, — математически доказать корректность реализации ядра. Дело в том, что микроядра в отличие от монолитно-модульных монстров типа GNU/Linux, весьма миниатюрные по размеру. А раз так, то они могут быть формально верифицированы. Каждой строчке кода ставится в соответствие математическое утверждение, которое нужно доказать.
В микроядре L4.verified доказывается соответствие реализации модели, отсутствие вечных циклов и еще некоторых вещей. Стоимость этого исследования составила порядка $6 миллионов, а проект длился 7 лет. Объем работы достиг 25 человеко-лет.
Помимо своего основного применения (безопасность, как и у seL4) L4 используется и в других сферах. Так, фирма Qualcomm запустила реализацию микроядра L4, разработанную фирмой NICTA, на наборе микросхем, называемом «Mobile Station Modem» (MSM). Об этом в ноябре 2005 года сообщили представители фирмы NICTA, а в конце 2006 года наборы микросхем MSM поступили в продажу. Так реализация микроядра L4 оказалась в сотовых телефонах.
Вопрос создания сверхнадежного ПО стал особенно актуальным, когда подавляющее большинство приложений стало работать в сети и оперировать с большим количеством данных. А данные эти зачастую конфиденциальны.
В сети не так много материалов о роли формальной верификации в создании сверхнадежных ОС. Еще меньше обстоятельных дискуссий. Поэтому ниже приведем основные мысли и аргументы одной из бесед по поводу статьи на эту тему:
- Распространение средств верификации и грамотное их внедрение позволит избавиться от целого класса ошибок в любом программном обеспечении. Например, такая ошибка, как «переполнение буфера», может быть предотвращена, если достаточно просто организовать проверку необходимых параметров.
Баги там все-таки есть, делает вывод один из комментаторов, ссылаясь на этот материал.
- Утверждается, что код seL4 обладает некоторой степенью надежности. Если создание абсолютно защищенной от взлома ОС — утопия, то почему этим продолжают заниматься такие крутые команды, как DARPA?
- Что будет, если хакеры подсунут туда верифицированный код? Или это невозможно? Почему во всех ОС есть баги, которые обязательно могут использовать хакеры?
- Почему верификация кода обязательно должна быть связана с защитой от взлома? Что, проще нельзя? Верификация кода и защита от взлома — это две разные задачи, которые всего лишь иногда пересекаются.
Трояны, кибервымогательство, фишинг, кликджекинг — это виды атак, которые работают независимо от наличия ошибок в программном коде приложений или операционной системы в целом. А если пользователи выбирают слабые пароли? Это тоже вина разработчиков ПО?
- Эксперимент расходится с реальностью, так как доступ, который дали хакерам исследователи, в жизни им никто не откроет. В таких системах просто нужно внимательно следить за тем, чтобы запрещать вставлять код всем, кроме администратора.
- Надо же! Хорошо написанные и протестированные приложения очень трудно взломать. Кто бы мог подумать… Вообще-то, программный код и так состоит из математически верифицированных конструкций.
- Разработка верифицированного кода — роскошь, которую могут позволить себе немногие. А его сопровождение и постоянное внесение изменений — еще большая роскошь.
- С точки зрения менеджмента, программисты часто ведут себя биполярно. Когда их просишь разбить большую задачу по разработке на подзадачи, они легко соглашаются. Но когда предлагаешь им заранее подумать над возможными ошибками и планомерно их предотвращать — реакция совсем другая: «это непрактично», «всего не предусмотришь», «а как же то?», «как же это?»… Далеко не все хотят думать о качестве кода заранее.
- А что делать, если средства верификации сами содержат ошибки? Кто будет верифицировать верификаторы?
- В чистой математике нет «багов». Если есть правило, что делить на ноль нельзя, значит, случаи, когда в знаменателе оказывается ноль, просто не рассматриваются. В реальной жизни этот прием не работает. Если речь идет о разработке ПО, то там приходится работать даже с теми значениями, которые программе «не нравятся». Результат от деления на ноль — это бесконечность. И с ней нужно что-то делать, а не заявлять, что такого результата не может быть.
P.S. Конечно же, дискутировать можно бесконечно. Но если такие крупные организации, как DARPA, делают конкретные шаги по реализации этих проектов, за этой историей как минимум стоит последить и как максимум — по участвовать.
Исходный код seL4 все еще доступен на GitHub.
