СофтХабрахабр

[Перевод] Микроядро seL4. Формальная верификация программ в реальном мире

Научная статья опубликована в журнале Communications of the ACM, октябрь 2018, том 61, номер 10, стр. 68−77, doi: 10.1145/3230627

Он летел полностью автономно. В феврале 2017 года со взлётной площадки «Боинга» в Аризоне поднялся вертолёт с обычным заданием: облёт ближайших холмов. Это был не первый автономный полёт AH-6, которого в компании называют Беспилотной Птичкой (Unmanned Little Bird, ULB). Согласно требованиям по технике безопасности Федерального управления авиации США, пилот не прикасался к органам управления. Однако на этот раз посреди полёта вертолёт подвергся кибератаке. Он так летает уже много лет. Атака поставила под угрозу некоторые подсистемы, но не смогла повлиять на безопасную эксплуатацию воздушного судна.
Бортовой компьютер атаковало вредоносное программное обеспечение видеокамеры, а также вирус, доставленный через заражённую флэшку, которую вставили во время техобслуживания.

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

Можно подумать, что военная авиация с лёгкостью отразит подобную кибератаку. В реальности же команда профессиональных пентестеров по заказу агентства DARPA в рамках программы по разработке высоконадёжных военных компьютерных систем High-Assurance Cyber Military Systems (HACMS) в 2013 году успешно взломала первую версию программного обеспечения ULB, которое изначально разрабатывалось для обеспечения безопасности полётов, а не защиты от кибератак. Хакеры получили возможность разбить вертолёт или посадить его на любое место по своему желанию. Поэтому риск таких атак с пассажиром на борту трудно переоценить, а неудачная попытка взлома в феврале 2017 года указывает на некие фундаментальные изменения в ПО.

Речь идёт о технологии, разработанной в рамках программы HACMS, направленной на обеспечение безопасной работы критических систем во враждебной киберсреде — в данном случае, нескольких автономных транспортных средств. В этой статье объясняются эти изменения и технология, которая сделала их возможными. Хотя статья не посвящена самим формальным методам, она объясняет, как использовать верификацию артефактов для защиты реальных систем на практике. Технология основана на формальной верификации программного обеспечения — это программы с автоматически проверенными математическими доказательствами, которое работает в соответствии со своей спецификацией.

Этот процесс называется «сейсмической модернизацией безопасности» (seismic security retrofit) по аналогии с сейсмической модернизацией зданий. Возможно, самый впечатляющий результат HACMS — что технологию можно распространить на существующие реальные системы, значительно улучшив их защиту от кибератак. Более того, большая часть реинжиниринга сделана инженерами компании «Боинг», а не специалистами по формальной верификации.


«Птичка» во время беспилотного испытательного полёта

Область формальной верификации ещё не готова к такому масштабу. Далеко не весь софт на вертолёте построен на математических моделях и доказательствах. Подход HACMS работает для систем, в которых желаемое свойство безопасности может быть достигнуто посредством чисто принудительного применения на уровне архитектуры. Тем не менее, программа HACMS продемонстрировала, что стратегическое применение формальных методов к наиболее важным частям общей системы значительно улучшает защиту. Оно гарантирует изоляцию между подсистемами, за исключением чётко определённых каналов связи, на которые распространяется политика безопасности системы. В его основе — наше верифицированное микроядро sel4, о котором поговорим ниже. С помощью предметно-ориентированных языков от Galois Inc. Эта изоляция гарантируется на уровне архитектуры с помощью верифицированного фреймворка CAmkES для системных компонентов. платформа CAmkES интегрируется с инструментами анализа архитектуры от Rockwell Collins и университета Миннесоты, а также с высоконадёжными программными компонентами.

Инновация в том, что формальные методы доказывают наблюдаемость интерфейсов и инкапсуляцию внутренностей модулей. Достижения HACMS основаны на старом верном друге инженера-программиста — модуляризации. Хотя инструменты пока не обеспечивают полного доказательства безопасности системы. Это гарантированное соблюдение модульности позволяет инженерам, которые не являются экспертами по формальным методам (как в компании «Боинг»), создавать новые или даже модернизировать существующие системы и достигать высокой устойчивости.

Доказательства математической корректности программ восходят, по крайней мере, к 1960-м годам, но долгое время их реальная польза для разработки программного обеспечения была ограничена масштабом и глубиной. Однако в последние годы произошёл ряд впечатляющих прорывов в формальной верификации на уровне кода реальных систем, от верифицированного компилятора C CompCert до верифицированного микроядра seL4 (см. научные статьи о нём), верифицированной системы конференц-связи CoCon, верифицированного ML-компилятора CakeML, верифицированных программ для доказательства теорем Milawa и Candle, верифицированной файловой системы с защитой от сбоев FSCQ, верифицированной распределённой системы IronFleet и верифированного фреймворка параллельного ядра CertiKOS, а также важных математических теорем, в том числе проблемы четырёх красок, автоматического доказательства гипотезы Кеплера и теоремы Фейта — Томпсона о нечётном порядке. Всё это настоящие системы. Например, CompCert — коммерческий продукт, микроядро seL4 используется в аэрокосмической и беспилотной авиации, в качестве платформы Интернета вещей, а система CoCon использовалась на многочисленных крупных научных конференциях.

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

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

Начнём с фундамента для построения доказуемо надёжных систем — ядра операционной системы (ОС). Это наиболее важная часть, которая экономически эффективно гарантирует надёжность всей системы.

В отличие от стандартных ядер, оно целенаправленно универсально и поэтому подходит для реализации ряда политик безопасности и системных требований. Микроядро seL4 предоставляет формально верифицированный минимальный набор механизмов для реализации защищённых систем.

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

1.
Рис. Изоляция и контролируемые коммуникации в seL4

Мало того, что оно обеспечивает лучшую производительность в своем классе, его 10 000 строк кода C прошли более тщательную формальную верификацию, чем любое другое общедоступное программное обеспечение в истории человечества с точки зрения не только строк доказательства, но и прочности доказанных свойств. Ядро seL4 занимает особое положение среди микроядер общего назначения. Оно гарантирует, что любое поведение ядра предсказывается его формальной абстрактной спецификацией: см. В основе лежит доказательство «функциональной корректности» реализации ядра на C. Следуя этой гарантии, мы добавили дополнительные доказательства, которые объясним после введения в основные механизмы ядра. онлайн-приложение для представления о том, как выглядят эти доказательства.

seL4 API

Ядро seL4 предоставляет минимальный набор механизмов для реализации защищённых систем: потоки, управление «способностями», виртуальные адресные пространства, межпроцессное взаимодействие (IPC), сигнализация и доставка прерываний.

Например, для каждого потока в системе существует «объект потока», хранящий информацию о шедулинге, выполнении и управлении доступом. Ядро сохраняет своё состояние в «объектах ядра». Например, поток не может запустить или остановить другой поток, если не имеет «способности» для соответствующего объекта потока. Программы пользовательского пространства могут ссылаться на объекты ядра только косвенно через так называемые «способности» или «возможности» (capabilities), которые объединяют ссылку на объект с набором прав доступа к нему.

Один поток со способностью отправки на соответствующую конечную точку может отправить сообщение другому потоку, имеющему способность получения на эту конечную точку. Потоки взаимодействуют и синхронизируются путём отправки сообщений через объекты «конечная точка» (endpoint) межпроцессного взаимодействия. Виртуальное преобразование адресов управляется объектами ядра, которые представляют каталоги страниц, таблицы страниц и объекты фреймов или тонкие абстракции над соответствующими объектами процессорной архитектуры. Объекты «уведомление» (notification) обеспечивают синхронизацию через наборы двоичных семафоров. Сами возможности управляются ядром и хранятся в объектах ядра “CNodes”, расположенных в структуре графа, который сопоставляет ссылки на объекты с правами доступа, аналогично сопоставлению виртуальных таблиц страниц с физическими адресами в памяти. У каждого потока есть определённая способность “VSpace”, которая указывает на корень дерева объектов преобразования адресов потока. Набор способностей, доступных из этого корня, мы называем «CSpace потока». У каждого потока своя способность идентификации корневого CNode. Рисунок 2 демонстрирует эти объекты ядра. Способности могут передаваться через конечные точки с передачей работы, а также их можно объявлять общими с помощью общих CSpace.

2.
Рис. Объекты ядра в системе на seL4 с двумя потоками, взаимодействующими через конечную точку

Доказательства безопасности

Благодаря своей универсальности API-интерфейсы ядра seL4 работают на низком уровне и поддерживают высокодинамичные системные архитектуры. Поэтому прямые доказательства для этих API проблематично получить.

В примере на рис. Высокоуровневая концепция политик управления доступом абстрагируется от отдельных объектов и возможностей ядра, захватывая вместо этого конфигурацию управления доступом системы с помощью набора абстрактных «субъектов» (компонентов) и полномочий, которые каждый из них имеет над другими (например, для чтения данных и отправки сообщений). 2, компоненты A и B получили полномочия над конечной точкой.

В работе Сьюэлла с коллегами доказано, что политики контроля доступа seL4 гарантируют соблюдение двух основных свойств безопасности: ограничение полномочий и целостность.

Это свойство подразумевает, что независимо от того, как развивается система, ни один компонент никогда не получит больше полномочий, чем предсказывает политика контроля доступа. Ограничение полномочий означает, что политика контроля доступа является статическим (неизменным) безопасным приближением конкретных возможностей и объектов ядра в системе для любого будущего состояния. Таким образом, компонент B никогда не сможет получить этот доступ в будущем. На рисунке 2 политика для компонента B не содержит доступа на запись к компоненту A. Это свойство подразумевает, что рассуждения на уровне политики являются безопасным приближением к рассуждениям о конкретном состоянии контроля доступа в системе.

Например, на рис. 2 единственным компонентом полномочий A над другим компонентом является право отправки данных на конечную точку, откуда получает информацию компонент B. Целостность означает, что независимо от того, что делает компонент, он никогда не сможет изменять данные в системе (включая любые системные вызовы, которые он может выполнять), которые ему явно не разрешает изменять политика контроля доступа. Он не может изменять другие части системы. Это означает, что компонент А способен изменять только своё состояние, состояние потока B и состояние буфера сообщений.

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

Ядро seL4 доступно для разных архитектур: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 и Intel x64. Дальнейшие доказательства в seL4 включают расширение функциональной корректности и, следовательно, теорем безопасности до бинарного уровня для архитектуры ARMv7 и профиль худшего времени выполнения для ядра (1, 2), необходимый для систем реального времени. На данный момент оно прошло машинную проверку на архитектуре ARMv7 для всего стека верификации, а также на ARMv7a с расширениями гипервизора для функциональной корректности.

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

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

Архитектура намеренно более сложная, чем требуется для квадрокоптера, поскольку она должна была представлять ULB и на этом уровне абстракции сходна с архитектурой ULB. На рисунке 3 показаны основные аппаратные компоненты квадрокоптера.

3.
Рис. Архитектура автономного летательного аппарата

Компьютеры связаны через внутреннюю сеть или шину CAN на квадрокоптере, Ethernet на ULB. На рисунке изображены два основных компьютера: бортовой компьютер, который взаимодействует с наземной станцией и управляет программным обеспечением на борту (например, камерой), и навигационный вычислитель для управления полётом транспортного средства, считывания данных датчиков и управления двигателями. На квадрокоптере также есть незащищённая точка WiFi, что даёт возможность продемонстрировать дополнительные методы защиты.

Для него должны исполняться четыре основных свойства: В данном примере рассмотрим бортовой компьютер.

  • правильная аутентификация команд от наземной станции;
  • приватность криптографических ключей;
  • никаких дополнительных сообщений для навигационного вычислителя;
  • ненадёжное ПО с других бортовых систем не может влиять на полёт аппарата.

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

Виртуальная машина (VM) под Linux служит контейнером для устаревшего программного обеспечения бортовых устройств, драйверов камер и точки WiFi. На рисунке 4 показано, как спроектирована архитектура квадрокоптера, которая обеспечивает эти свойства. Задача криптографического компонента — передавать (только) авторизованные сообщения в бортовой компьютер через CAN-интерфейс стека и отправлять диагностические данные обратно на наземную станцию. Изолируем модуль управления криптографией в собственном компоненте, с подключениями к шине CAN, каналу наземной станции и к виртуальной машине Linux для отправки данных на наземную станцию. Компонент радиосвязи отправляет и получает необработанные сообщения, которые шифруются и расшифровываются (с аутентификацией) криптографическим компонентом.

4.
Рис. Упрощённая архитектура бортового компьютера квадрокоптера

Если предположить правильное поведение этого компонента, ключи не могут быть скомпрометированы, так как ни один другой компонент не имеет к ним доступа. Установка желаемых свойств системы сводится исключительно к свойствам изоляции и поведению архитектуры в части информационных потоков, а также к поведению единственного доверенного криптографического компонента. В шину CAN могут попасть только авторизованные сообщения, потому что криптографический компонент — единственная связь с шиной. Канал между Linux и криптографическим компонентом на рис. 4 предназначен только для передачи сообщений и не даёт доступа к памяти. Ненадёжное ПО и WiFi, как часть виртуальной машины Linux, инкапсулируются изоляцией компонентов и могут взаимодействовать с остальной частью системы только через доверенный криптографический компонент.

Как было отмечено для систем MILS, границы компонентов в такой архитектуре — не только удобный инструмент разбиения на модули и управления кодом, но с принудительной изоляцией обеспечивают эффективные границы для формальных рассуждений о поведении системы. Легко представить, что такого рода анализ архитектуры можно в значительной степени автоматизировать с помощью проверки моделей и инструментов механических рассуждений более высокого уровня. Однако всё зависит от правильного применения границ компонентов во время выполнения в окончательной бинарной реализации системы.

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

Как доказательства безопасности упрощаются с формальными абстракциями политик безопасности, также абстракция помогает в разработке систем. Компонентная платформа Camkes работает на абстракциях seL4 поверх низкоуровневых механизмов ядра, обеспечивая коммуникационные примитивы и декомпозицию системы на функциональные единицы, как показано на рис. 5. Используя эту платформу, системные архитекторы могут проектировать и строить системы на основе seL4 с точки зрения компонентов высокого уровня, которые взаимодействуют друг с другом и с аппаратными устройствами через коннекторы, такие как удалённые вызовы процедур (RPC), датапорты и события.

5.
Рис. Рабочий процесс CAmkES

Генерация кода

Внутренне CAmkES реализует эти абстракции с помощью низкоуровневых объектов ядра seL4. Каждый компонент содержит (по крайней мере) один поток, CSpace и VSpace. Коннекторы RPC используют объекты конечной точки, и CAmkES генерирует промежуточный код для обработки сообщений и передачи их по конечным точкам IPC. Аналогичным образом, коннектор датапорта реализуется через общую память — общие фреймы, присутствующие в адресных пространствах двух компонентов — и опционально может ограничить направление передачи данных. Наконец, коннектор событий реализован с помощью механизма уведомлений seL4.

Эта спецификация становится входными данными для инициализатора seL4, который первым запускается после загрузки и выполняет необходимые операции seL4 для создания инстанса и инициализации системы. CAmkES также генерирует на языке capDL низкоуровневую спецификацию начальной конфигурации объектов и возможностей ядра системы.

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

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

Автоматические доказательства

При генерации «промежуточного» кода CAmkES производит формальные доказательства в Isabelle/HOL, выполняя валидацию в процессе трансляции и демонстрируя, что сгенерированный «промежуточный» код подчиняется спецификации высокого уровня, а сгенерированная спецификация capDL является правильным уточнением описания CAmkES. Мы также доказали, что инициализатор seL4 правильно настраивает систему в требуемой начальной конфигурации. При этом мы автоматизируем большую часть построения системы без расширения доверенной вычислительной базы.

Так же и мы предполагаем, что доказательства для промежуточного кода не нуждаются в проверке, то есть разработчики могут сосредоточиться на доказательстве корректности собственного кода. Разработчики редко смотрят на выдачу генераторов кода, их интересует только функциональность и бизнес-логика. Леммы описывают ожидаемое поведение коннекторов. Как сгенерированный CAmkES заголовок даёт разработчику API для сгенерированного кода, так и операторы леммы верхнего уровня производят API для доказательств. Чтобы сохранить абстракции, вызов $f$ должен быть эквивалентен вызову $g$. В примере промежуточного кода RPC на рис. 6 сгенерированная функция $f$ предоставляет способ вызова удалённой функции $g$ в другом компоненте. Сгенерированная системой лемма гарантирует, что $f$ из сгенерированного кода RPC ведёт себя как прямой вызов $g$.

6.
Рис. Cгенерированный код RPC

Чтобы добиться этой компонуемости, спецификация коннекторов параметризуется через предоставленные пользователем спецификации удалённых функций. Для реального использования сгенерированных системой доказательств они должны быть компонуемы с (почти) произвольными доказательствами, предоставленными пользователем, как для функции $g$, так и для контекстов, в которых используются $g$ и $f$. Таким образом, инженеры могут рассуждать о своей архитектуре, предоставляя спецификации и доказательства для своих компонентов, и полагаться на спецификации для сгенерированного кода.

Поскольку шаблоны других коннекторов (датапорты и события) значительно проще, чем RPC, будет несложно расширить генератор доказательств для поддержки этих коннекторов, что позволит создавать более разнообразные верифицированные системы. На сегодняшний день мы продемонстрировали этот процесс от начала и до конца с помощью специального коннектора CAmkES RPC (1, 2).

Чтобы доказать, что эти два описания системы — capDL и CAmkES — соответствуют друг другу, рассмотрим описание CAmkES как абстракцию для описание capDL. После кода для коммуникации CAmkES создаёт начальную конфигурацию управления доступом для применения границ архитектуры. Так мы повысим доказательство до уровня политики. Используем упомянутый ранее проверенный фреймворк, чтобы вывести полномочия одного объекта над другим объектом из описания capDL. Полученное доказательство гарантирует, что у объектов capDL, представленных в виде графа полномочий с объектами, сгруппированными по компонентам, те же границы между группами, что и в эквивалентном графе компонентов CAmkES. Кроме того, мы определили правила для вывода полномочий между компонентами в описании CAmkES. Интуитивно, такое соответствие границ означает, что анализ архитектуры политики из описания CAmkES сохранит политику из описания, сгенерированного capDL, которое, в свою очередь, гарантированно удовлетворяет требованиям ограничения полномочий, целостности и конфиденциальности, как упоминалось ранее.

В seL4 эта первая (и уникальная) пользовательская задача имеет доступ ко всей доступной памяти, используя её для создания объектов и «способностей» в соответствии с подробным описанием capDL, которое она принимает в качестве входных данных. Наконец, для доказательства корректной инициализации CAmkES использует универсальный инициализатор, который запустится как первая пользовательская задача после загрузки. Это доказательство справедливо для точной модели инициализатора, но ещё не на уровне реализации. Доказано, что состояние после выполнения инициализатора удовлетворяет состоянию, описанному в заданной спецификации. По сравнению с глубиной остальной цепи доказательств это ограничение может показаться слабым, но оно уже является более формальным доказательством, чем требуется на высшем уровне (EAL7) общих критериев оценки безопасности.

На практике трудно обеспечить разработку системы с нуля ради безопасности, поэтому решающее значение для разработки безопасных систем имеет возможность модернизации старого ПО. Наш фреймворк на базе seL4 поддерживает итеративный процесс, который мы называем «сейсмическая модернизация безопасности», как обычный архитектор модернизирует существующие здания для большей сейсмоустойчивости. Проиллюстрируем процесс на примере постепенной адаптации существующей программной архитектуры беспилотного вертолёта, перейдя от традиционного схемы тестирования к высоконадёжной системе с теоремами, подкреплёнными формальными методами. Хотя этот пример основан на реальном проекте ULB, здесь он упрощён и не включает все детали.

Его функциональность обеспечивают два отдельных компьютера: навигационный вычислитель управляет фактическим полётом, а бортовой компьютер выполняет задачи высокого уровня (такие как связь с наземной станцией и навигация по картинке с камеры). Оригинальная архитектура вертолёта совпадает с архитектурой, описанной на рис. 3. В процессе модернизации инженеры компании «Боинг» применили методы, инструменты и компоненты, предоставленные партнёрами по программе HACMS. Первоначальная версия бортового компьютера была монолитным приложением под Linux.

Шаг 1. Виртуализация

Первым шагом было принять систему как есть и запустить ее в виртуальной машине поверх безопасного гипервизора (см. рис. 7). В метафоре сейсмической модернизации это соответствует размещению системы на более подвижном фундаменте. Виртуальная машина поверх seL4 в этой системе состоит из одного компонента CAmkES, который включает монитор виртуальной машины (VMM) и гостевую операционную систему, в данном случае Linux. Ядро предоставляет абстракции оборудования виртуализации, а VMM управляет этими абстракциями для виртуальной машины. Ядро seL4 ограничивает не только гостевую ОС, но и VMM, поэтому не нужно доверять реализации VMM для обеспечения принудительной изоляции. Отказ VMM приведёт к отказу гостевой ОС, но не к отказу всей системы.

7.
Рис. Все функциональные возможности в одной виртуальной машине

В случае сквозных драйверов разработчики могут использовать системный MMU или IOMMU для предотвращения нарушения границ изоляции аппаратными устройствами и драйверами в гостевой системе. В зависимости от конфигурации системы, виртуальная машина может иметь доступ к устройствам через паравиртуализированные драйверы, сквозные драйверы или обоими способами. Шаг 1 нужен только для подготовки к шагу 2. Обратите внимание, что простой запуск системы на виртуальной машине не добавляет дополнительных преимуществ безопасности или надёжности.

Шаг 2. Несколько виртуальных машин

Второй шаг сейсмической модернизации усиливает существующие стены. В программном обеспечении разработчик может повысить безопасность и надёжность, разделив исходную систему на несколько подсистем, каждая из которых состоит из виртуальной машины, выполняющей код только части исходной системы. Каждая комбинация VM/VMM выполняется в отдельном компоненте CAmkES, который внедряет изоляцию между разными подсистемами, не позволяя им влиять друг на друга, а затем допускает сожительство разных уровней безопасности.

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

Для обеспечения безопасности крайне важно, чтобы эти интерфейсы были узкими, ограничивая связь между разделами только тем, что абсолютно необходимо. Как правило, разделы должны взаимодействовать друг с другом, так что на этом этапе мы также добавим каналы связи. Критически важно, что seL4 позволяет контролировать и ограничивать обмен памятью между разделами, чтобы минимизировать объём данных. Кроме того, интерфейсные протоколы должны быть эффективными, с минимальным количеством сообщений или объёмом данных.

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

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

В нашем примере мы получили три раздела: виртуальную машину, реализующую функции связи наземной станции под управлением Linux; другую виртуальную машину, реализующую функции навигации на основе камеры (также работающую под управлением Linux); и нативный компонент, предоставляющий общий доступ к сети, как показано на рис. 8.

8.
Рис. Функциональность разделена на несколько виртуальных машин

Шаг 3. Нативные компоненты

Когда система разложена на отдельные разделы виртуальной машины, некоторые или все отдельные разделы можно повторно реализовать в виде нативных компонентов, а не виртуальных машин. Это значительно уменьшит поверхность атаки для той же функциональности. Дополнительное преимущество преобразования компонента в машинный код — снижение нагрузки и повышение производительности, удаление гостевой ОС и накладных расходов на исполнение кода и коммуникации VMM.

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

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

В нативных компонентах реализуются функции связи, криптографии и управления (mission-manager). В нашем примере разберём на нативные модули виртуальную машину для канала связи между бортовым компьютером и наземной станцией. Такое разделение стало компромиссом между усилиями по переделке подсистем и выгодами от использования нативных компонентов с точки зрения производительности и надёжности. Мы оставим в виртуальной машине камеру и WiFi как ненадёжный устаревший компонент (см. рис. 9).

9.
Рис. Функциональность реализована в нативных компонентах

Шаг 4. Надёжность системы в целом

Получив все необходимые модули, сделаем заключительный шаг: анализ всей системы в целом на основе надёжности архитектуры и отдельных компонентов.

Без дополнительной верификации Ivory не даёт нам гарантий функциональной корректности, но даёт уверенность в отказоустойчивости и аварийной надёжности. В рамках HACMS коммуникация, криптография, и модуль управления реализованы на доказуемо типобезопасном предметно-ориентированном языке Ivory, с выделением фиксированного объёма памяти в куче. Учитывая изоляцию компонентов, мы считаем, что эти гарантии сохраняются в присутствии ненадёжных компонентов (таких как виртуальная машина камеры).

Его уровень надёжности соответствует уровню, полученному благодаря тщательной реализации известного кода. Сетевой компонент реализован на стандартном коде C, состоящем из пользовательского кода для платформы и уже существующего кода библиотеки. В общем анализе безопасности системы любая компрометация сетевого компонента повлияет только на сетевые пакеты. Надёжность можно повысить без особых затрат с помощью таких методов, как синтез драйверов, а также с помощью типобезопасных языков вроде Ivory. Поскольку трафик зашифрован, такая атака не поставит под угрозу условие из спецификаций, что в бортовой компьютер попадают только авторизованные команды.

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

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

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

Эта библиотека может включать шаблоны безопасности (такие как дезинфекция входных данных, фильтры вывода, мониторы снижения уровня секретности и времени выполнения), потенциально сгенерированные из спецификаций более высокого уровня, а также такие компоненты инфраструктуры, как повторно используемые криптомодули, хранилище ключей, файловые системы, сетевые стеки и драйверы высокой надёжности. Первый шаг к ослаблению этих ограничений — создание библиотеки предварительно проверенных компонентов высокого уровня надёжности для использования в качестве надёжных строительных блоков в таких архитектурах. Основными техническими проблемами здесь являются рассуждения о параллелизме и протоколах, а также о потоке информации в присутствии доверенных компонентов. Если безопасность зависит более чем от одного такого компонента, то возникает необходимость обосновать надёжность их взаимодействия и совместного использования. В настоящее время создание таких систем возможно за меньшую стоимость, чем традиционное тестирование. Несмотря на эти ограничения, работа демонстрирует быстрое развитие реальных высоконадёжных систем на основе seL4.

Разработка дизайна и кода seL4 заняла два человеко-года. Если добавить все серотип-специфичные доказательства, в общей сложности получится 18 человеко-лет для 8700 строк кода на C. Для сравнения, разработка сравнимого по размеру микроядра L4Ka::Pistachio из семейства seL4 заняло шесть человеко-лет и не обеспечило значительного уровня надёжности. Это означает разницу по скорости разработки всего лишь в 3,3 раза между верифицированным и традиционным софтом. Согласно методу оценки Кольбера и Бома, сертификация по традиционным критериям EAL7 для 8700 строк кода C займёт более 45,9 человеко-лет. Это означает, что формальная верификация реализации на бинарном уровне уже в 2,3 раза дешевле, чем самый высокий уровень сертификации по общим критериям, при этом обеспечивает значительно более высокую надёжность.

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

Показать больше

Похожие публикации

Добавить комментарий

Ваш адрес email не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»