Научная статья опубликована в журнале 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, направленной на обеспечение безопасной работы критических систем во враждебной киберсреде — в данном случае, нескольких автономных транспортных средств. Технология основана на формальной верификации программного обеспечения — это программы с автоматически проверенными математическими доказательствами, которое работает в соответствии со своей спецификацией. Хотя статья не посвящена самим формальным методам, она объясняет, как использовать верификацию артефактов для защиты реальных систем на практике.
Возможно, самый впечатляющий результат HACMS — что технологию можно распространить на существующие реальные системы, значительно улучшив их защиту от кибератак. Этот процесс называется «сейсмической модернизацией безопасности» (seismic security retrofit) по аналогии с сейсмической модернизацией зданий. Более того, большая часть реинжиниринга сделана инженерами компании «Боинг», а не специалистами по формальной верификации.
«Птичка» во время беспилотного испытательного полёта
Далеко не весь софт на вертолёте построен на математических моделях и доказательствах. Область формальной верификации ещё не готова к такому масштабу. Тем не менее, программа HACMS продемонстрировала, что стратегическое применение формальных методов к наиболее важным частям общей системы значительно улучшает защиту. Подход HACMS работает для систем, в которых желаемое свойство безопасности может быть достигнуто посредством чисто принудительного применения на уровне архитектуры. В его основе — наше верифицированное микроядро sel4, о котором поговорим ниже. Оно гарантирует изоляцию между подсистемами, за исключением чётко определённых каналов связи, на которые распространяется политика безопасности системы. Эта изоляция гарантируется на уровне архитектуры с помощью верифицированного фреймворка CAmkES для системных компонентов. С помощью предметно-ориентированных языков от Galois Inc. платформа CAmkES интегрируется с инструментами анализа архитектуры от Rockwell Collins и университета Миннесоты, а также с высоконадёжными программными компонентами.
Достижения HACMS основаны на старом верном друге инженера-программиста — модуляризации. Инновация в том, что формальные методы доказывают наблюдаемость интерфейсов и инкапсуляцию внутренностей модулей. Это гарантированное соблюдение модульности позволяет инженерам, которые не являются экспертами по формальным методам (как в компании «Боинг»), создавать новые или даже модернизировать существующие системы и достигать высокой устойчивости. Хотя инструменты пока не обеспечивают полного доказательства безопасности системы.
Доказательства математической корректности программ восходят, по крайней мере, к 1960-м годам, но долгое время их реальная польза для разработки программного обеспечения была ограничена масштабом и глубиной. Однако в последние годы произошёл ряд впечатляющих прорывов в формальной верификации на уровне кода реальных систем, от верифицированного компилятора C CompCert до верифицированного микроядра seL4 (см. научные статьи о нём), верифицированной системы конференц-связи CoCon, верифицированного ML-компилятора CakeML, верифицированных программ для доказательства теорем Milawa и Candle, верифицированной файловой системы с защитой от сбоев FSCQ, верифицированной распределённой системы IronFleet и верифированного фреймворка параллельного ядра CertiKOS, а также важных математических теорем, в том числе проблемы четырёх красок, автоматического доказательства гипотезы Кеплера и теоремы Фейта — Томпсона о нечётном порядке. Всё это настоящие системы. Например, CompCert — коммерческий продукт, микроядро seL4 используется в аэрокосмической и беспилотной авиации, в качестве платформы Интернета вещей, а система CoCon использовалась на многочисленных крупных научных конференциях.
Эти проекты верификации требуют значительных усилий. Чтобы сделать формальные методы общедоступными, эти усилия необходимо сократить. Здесь мы демонстрируем, как стратегическое сочетание формальных и неформальных методов, частичная автоматизация формальных методов и тщательная разработка программного обеспечения для максимизации преимуществ изолированных компонентов позволили нам значительно повысить надёжность систем, общий размер и сложность которых на порядки больше, чем у упомянутых выше.
Обратите внимание, мы применяем формальную верификацию в первую очередь для кода, от которого зависит безопасность системы. Но есть и другие преимущества. Например, доказательства корректности кода делают предположения о контексте, в котором он выполняется (например, о поведении оборудования и конфигурации программного обеспечения). Формальная верификация делает эти предположения явными, что помогает разработчикам сфокусироваться на других средствах верификации, таких как тестирование. Кроме того, во многих случаях система включает и проверенный, и непроверенный код. Во время код-ревью, тестирования и отладки формальная верификация действует как объектив, фокусируя внимание на критическом непроверенном коде системы.
Начнём с фундамента для построения доказуемо надёжных систем — ядра операционной системы (ОС). Это наиболее важная часть, которая экономически эффективно гарантирует надёжность всей системы.
Микроядро seL4 предоставляет формально верифицированный минимальный набор механизмов для реализации защищённых систем. В отличие от стандартных ядер, оно целенаправленно универсально и поэтому подходит для реализации ряда политик безопасности и системных требований.
Одна из основных целей разработки seL4 заключается в обеспечении сильной изоляции между взаимно не доверяющими друг другу компонентами, которые работают поверх ядра. Поддерживается его работа в качестве гипервизора, например, для целых операционных систем Linux, сохраняя при этом их изолированными от критичных для безопасности компонентов, которые могут работать вместе, как показано на рисунке 1. В частности, эта функция позволяет разработчикам систем использовать устаревшие компоненты со скрытыми уязвимостями рядом с высоконадёжными компонентами.
Рис. 1. Изоляция и контролируемые коммуникации в seL4
Ядро seL4 занимает особое положение среди микроядер общего назначения. Мало того, что оно обеспечивает лучшую производительность в своем классе, его 10 000 строк кода C прошли более тщательную формальную верификацию, чем любое другое общедоступное программное обеспечение в истории человечества с точки зрения не только строк доказательства, но и прочности доказанных свойств. В основе лежит доказательство «функциональной корректности» реализации ядра на C. Оно гарантирует, что любое поведение ядра предсказывается его формальной абстрактной спецификацией: см. онлайн-приложение для представления о том, как выглядят эти доказательства. Следуя этой гарантии, мы добавили дополнительные доказательства, которые объясним после введения в основные механизмы ядра.
Ядро seL4 предоставляет минимальный набор механизмов для реализации защищённых систем: потоки, управление «способностями», виртуальные адресные пространства, межпроцессное взаимодействие (IPC), сигнализация и доставка прерываний.
Ядро сохраняет своё состояние в «объектах ядра». Например, для каждого потока в системе существует «объект потока», хранящий информацию о шедулинге, выполнении и управлении доступом. Программы пользовательского пространства могут ссылаться на объекты ядра только косвенно через так называемые «способности» или «возможности» (capabilities), которые объединяют ссылку на объект с набором прав доступа к нему. Например, поток не может запустить или остановить другой поток, если не имеет «способности» для соответствующего объекта потока.
Потоки взаимодействуют и синхронизируются путём отправки сообщений через объекты «конечная точка» (endpoint) межпроцессного взаимодействия. Один поток со способностью отправки на соответствующую конечную точку может отправить сообщение другому потоку, имеющему способность получения на эту конечную точку. Объекты «уведомление» (notification) обеспечивают синхронизацию через наборы двоичных семафоров. Виртуальное преобразование адресов управляется объектами ядра, которые представляют каталоги страниц, таблицы страниц и объекты фреймов или тонкие абстракции над соответствующими объектами процессорной архитектуры. У каждого потока есть определённая способность “VSpace”, которая указывает на корень дерева объектов преобразования адресов потока. Сами возможности управляются ядром и хранятся в объектах ядра “CNodes”, расположенных в структуре графа, который сопоставляет ссылки на объекты с правами доступа, аналогично сопоставлению виртуальных таблиц страниц с физическими адресами в памяти. У каждого потока своя способность идентификации корневого CNode. Набор способностей, доступных из этого корня, мы называем «CSpace потока». Способности могут передаваться через конечные точки с передачей работы, а также их можно объявлять общими с помощью общих CSpace. Рисунок 2 демонстрирует эти объекты ядра.
Рис. 2. Объекты ядра в системе на seL4 с двумя потоками, взаимодействующими через конечную точку
Благодаря своей универсальности API-интерфейсы ядра seL4 работают на низком уровне и поддерживают высокодинамичные системные архитектуры. Поэтому прямые доказательства для этих API проблематично получить.
Высокоуровневая концепция политик управления доступом абстрагируется от отдельных объектов и возможностей ядра, захватывая вместо этого конфигурацию управления доступом системы с помощью набора абстрактных «субъектов» (компонентов) и полномочий, которые каждый из них имеет над другими (например, для чтения данных и отправки сообщений). В примере на рис. 2, компоненты A и B получили полномочия над конечной точкой.
В работе Сьюэлла с коллегами доказано, что политики контроля доступа seL4 гарантируют соблюдение двух основных свойств безопасности: ограничение полномочий и целостность.
Ограничение полномочий означает, что политика контроля доступа является статическим (неизменным) безопасным приближением конкретных возможностей и объектов ядра в системе для любого будущего состояния. Это свойство подразумевает, что независимо от того, как развивается система, ни один компонент никогда не получит больше полномочий, чем предсказывает политика контроля доступа. На рисунке 2 политика для компонента B не содержит доступа на запись к компоненту A. Таким образом, компонент B никогда не сможет получить этот доступ в будущем. Это свойство подразумевает, что рассуждения на уровне политики являются безопасным приближением к рассуждениям о конкретном состоянии контроля доступа в системе.
Целостность означает, что независимо от того, что делает компонент, он никогда не сможет изменять данные в системе (включая любые системные вызовы, которые он может выполнять), которые ему явно не разрешает изменять политика контроля доступа. Например, на рис. 2 единственным компонентом полномочий A над другим компонентом является право отправки данных на конечную точку, откуда получает информацию компонент B. Это означает, что компонент А способен изменять только своё состояние, состояние потока B и состояние буфера сообщений. Он не может изменять другие части системы.
Побочный эффект целостности — это конфиденциальность, когда компонент не способен без разрешения прочитать информацию из другого компонента: это доказанное сильное свойство нетранзитивного невмешательства seL4. То есть в должным образом настроенной системе (с более жёсткими ограничениями, чем просто для целостности) ни один из компонентов не сможет без разрешения узнать информацию о другом компоненте или его исполнении. Доказательство выражает это свойство в терминах политики информационного потока, которую можно извлечь из политики управления доступом, используемой в доказательстве целостности. Информация будет передаваться только тогда, когда это явно разрешено политикой. Доказательство охватывает явные информационные потоки, а также потенциальные каналы скрытого хранения в ядре. Но каналы синхронизации находятся вне его области и должны обрабатываться иными средствами.
Дальнейшие доказательства в seL4 включают расширение функциональной корректности и, следовательно, теорем безопасности до бинарного уровня для архитектуры ARMv7 и профиль худшего времени выполнения для ядра (1, 2), необходимый для систем реального времени. Ядро seL4 доступно для разных архитектур: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 и Intel x64. На данный момент оно прошло машинную проверку на архитектуре ARMv7 для всего стека верификации, а также на ARMv7a с расширениями гипервизора для функциональной корректности.
В предыдущем разделе описаны программные методы, с помощью которых ядро seL4 создаёт прочный фундамент для доказуемо надёжных систем. Ядро формирует достоверную вычислительную базу (TCB) — обязательный компонент программного обеспечения, которое обязано работать корректно для гарантированной безопасности системы. В реальных системах эта база гораздо шире, чем просто микроядро. Нужно верифицировать дополнительный программный стек, чтобы получить тот же уровень уверенности, что и для ядра. Однако существуют классы систем, для которых нет необходимости в такой верификации: им достаточно теорем изоляции на уровне ядра для выведения определённых свойств безопасности на уровне системы. В этом разделе приведён пример такой системы.
Это системы, в которых архитектуры компонентов уже реализовали критическое свойство, возможно, вместе с несколькими небольшими доверенными компонентами. Наш пример — ПО управления полётом квадрокоптера, демонстрационного аппарата в упомянутой ранее программе HACMS.
На рисунке 3 показаны основные аппаратные компоненты квадрокоптера. Архитектура намеренно более сложная, чем требуется для квадрокоптера, поскольку она должна была представлять ULB и на этом уровне абстракции сходна с архитектурой ULB.
Рис. 3. Архитектура автономного летательного аппарата
На рисунке изображены два основных компьютера: бортовой компьютер, который взаимодействует с наземной станцией и управляет программным обеспечением на борту (например, камерой), и навигационный вычислитель для управления полётом транспортного средства, считывания данных датчиков и управления двигателями. Компьютеры связаны через внутреннюю сеть или шину CAN на квадрокоптере, Ethernet на ULB. На квадрокоптере также есть незащищённая точка WiFi, что даёт возможность продемонстрировать дополнительные методы защиты.
В данном примере рассмотрим бортовой компьютер. Для него должны исполняться четыре основных свойства:
Рабочая гипотеза состоит в том, что камера ненадёжна, потенциально скомпрометирована или вредоносна, что её драйверы и устаревшее ПО потенциально скомпрометированы, также как любые внешние каналы коммуникации. В этом примере мы предполагаем правильную и сильную криптографию, то есть что ключ нельзя подобрать, и выводим за рамки задачи возможность подавления противником радиосвязи с наземной станцией.
На рисунке 4 показано, как спроектирована архитектура квадрокоптера, которая обеспечивает эти свойства. Виртуальная машина (VM) под Linux служит контейнером для устаревшего программного обеспечения бортовых устройств, драйверов камер и точки WiFi. Изолируем модуль управления криптографией в собственном компоненте, с подключениями к шине CAN, каналу наземной станции и к виртуальной машине Linux для отправки данных на наземную станцию. Задача криптографического компонента — передавать (только) авторизованные сообщения в бортовой компьютер через CAN-интерфейс стека и отправлять диагностические данные обратно на наземную станцию. Компонент радиосвязи отправляет и получает необработанные сообщения, которые шифруются и расшифровываются (с аутентификацией) криптографическим компонентом.
Рис.4. Упрощённая архитектура бортового компьютера квадрокоптера
Установка желаемых свойств системы сводится исключительно к свойствам изоляции и поведению архитектуры в части информационных потоков, а также к поведению единственного доверенного криптографического компонента. Если предположить правильное поведение этого компонента, ключи не могут быть скомпрометированы, так как ни один другой компонент не имеет к ним доступа. Канал между Linux и криптографическим компонентом на рис. 4 предназначен только для передачи сообщений и не даёт доступа к памяти. В шину CAN могут попасть только авторизованные сообщения, потому что криптографический компонент — единственная связь с шиной. Ненадёжное ПО и WiFi, как часть виртуальной машины Linux, инкапсулируются изоляцией компонентов и могут взаимодействовать с остальной частью системы только через доверенный криптографический компонент.
Легко представить, что такого рода анализ архитектуры можно в значительной степени автоматизировать с помощью проверки моделей и инструментов механических рассуждений более высокого уровня. Как было отмечено для систем MILS, границы компонентов в такой архитектуре — не только удобный инструмент разбиения на модули и управления кодом, но с принудительной изоляцией обеспечивают эффективные границы для формальных рассуждений о поведении системы. Однако всё зависит от правильного применения границ компонентов во время выполнения в окончательной бинарной реализации системы.
Обсуждавшиеся ранее механизмы ядра seL4 способны обеспечить такую реализацию, но уровень абстракции механизмов резко контрастирует с блоками и стрелками архитектурной схемы: даже более абстрактная политика управления доступом по-прежнему содержит гораздо больше деталей, чем схема архитектуры. В реальной системе такого размера десятки тысяч объектов ядра и «способностей», созданных программно, а ошибки в конфигурации могут привести к нарушениям безопасности. Затем обсудим, каким образом мы не только автоматизируем конфигурацию и создание такого кода, но и как автоматически доказать соблюдение границ архитектуры.
Как доказательства безопасности упрощаются с формальными абстракциями политик безопасности, также абстракция помогает в разработке систем. Компонентная платформа Camkes работает на абстракциях seL4 поверх низкоуровневых механизмов ядра, обеспечивая коммуникационные примитивы и декомпозицию системы на функциональные единицы, как показано на рис. 5. Используя эту платформу, системные архитекторы могут проектировать и строить системы на основе seL4 с точки зрения компонентов высокого уровня, которые взаимодействуют друг с другом и с аппаратными устройствами через коннекторы, такие как удалённые вызовы процедур (RPC), датапорты и события.
Рис. 5. Рабочий процесс CAmkES
Внутренне CAmkES реализует эти абстракции с помощью низкоуровневых объектов ядра seL4. Каждый компонент содержит (по крайней мере) один поток, CSpace и VSpace. Коннекторы RPC используют объекты конечной точки, и CAmkES генерирует промежуточный код для обработки сообщений и передачи их по конечным точкам IPC. Аналогичным образом, коннектор датапорта реализуется через общую память — общие фреймы, присутствующие в адресных пространствах двух компонентов — и опционально может ограничить направление передачи данных. Наконец, коннектор событий реализован с помощью механизма уведомлений seL4.
CAmkES также генерирует на языке capDL низкоуровневую спецификацию начальной конфигурации объектов и возможностей ядра системы. Эта спецификация становится входными данными для инициализатора seL4, который первым запускается после загрузки и выполняет необходимые операции seL4 для создания инстанса и инициализации системы.
Таким образом, платформа компонентов генерирует код без дополнительных усилий со стороны разработчика. Компонентная архитектура описывает набор блоков и стрелок, а задача реализации сводится к простому заполнению полей. Платформа генерирует остальное, обеспечивая реализацию описанной архитектуры.
На платформе с традиционными компонентами сгенерированный код расширит доверенную вычислительную базу системы, поскольку он может влиять на функциональность компонентов. Однако CAmkES также генерирует доказательства.
При генерации «промежуточного» кода CAmkES производит формальные доказательства в Isabelle/HOL, выполняя валидацию в процессе трансляции и демонстрируя, что сгенерированный «промежуточный» код подчиняется спецификации высокого уровня, а сгенерированная спецификация capDL является правильным уточнением описания CAmkES. Мы также доказали, что инициализатор seL4 правильно настраивает систему в требуемой начальной конфигурации. При этом мы автоматизируем большую часть построения системы без расширения доверенной вычислительной базы.
Разработчики редко смотрят на выдачу генераторов кода, их интересует только функциональность и бизнес-логика. Так же и мы предполагаем, что доказательства для промежуточного кода не нуждаются в проверке, то есть разработчики могут сосредоточиться на доказательстве корректности собственного кода. Как сгенерированный CAmkES заголовок даёт разработчику API для сгенерированного кода, так и операторы леммы верхнего уровня производят API для доказательств. Леммы описывают ожидаемое поведение коннекторов. В примере промежуточного кода RPC на рис. 6 сгенерированная функция предоставляет способ вызова удалённой функции в другом компоненте. Чтобы сохранить абстракции, вызов должен быть эквивалентен вызову . Сгенерированная системой лемма гарантирует, что из сгенерированного кода RPC ведёт себя как прямой вызов .
Рис. 6. Cгенерированный код RPC
Для реального использования сгенерированных системой доказательств они должны быть компонуемы с (почти) произвольными доказательствами, предоставленными пользователем, как для функции , так и для контекстов, в которых используются и . Чтобы добиться этой компонуемости, спецификация коннекторов параметризуется через предоставленные пользователем спецификации удалённых функций. Таким образом, инженеры могут рассуждать о своей архитектуре, предоставляя спецификации и доказательства для своих компонентов, и полагаться на спецификации для сгенерированного кода.
На сегодняшний день мы продемонстрировали этот процесс от начала и до конца с помощью специального коннектора CAmkES RPC (1, 2). Поскольку шаблоны других коннекторов (датапорты и события) значительно проще, чем RPC, будет несложно расширить генератор доказательств для поддержки этих коннекторов, что позволит создавать более разнообразные верифицированные системы.
После кода для коммуникации CAmkES создаёт начальную конфигурацию управления доступом для применения границ архитектуры. Чтобы доказать, что эти два описания системы — capDL и CAmkES — соответствуют друг другу, рассмотрим описание CAmkES как абстракцию для описание capDL. Используем упомянутый ранее проверенный фреймворк, чтобы вывести полномочия одного объекта над другим объектом из описания capDL. Так мы повысим доказательство до уровня политики. Кроме того, мы определили правила для вывода полномочий между компонентами в описании CAmkES. Полученное доказательство гарантирует, что у объектов capDL, представленных в виде графа полномочий с объектами, сгруппированными по компонентам, те же границы между группами, что и в эквивалентном графе компонентов CAmkES. Интуитивно, такое соответствие границ означает, что анализ архитектуры политики из описания CAmkES сохранит политику из описания, сгенерированного capDL, которое, в свою очередь, гарантированно удовлетворяет требованиям ограничения полномочий, целостности и конфиденциальности, как упоминалось ранее.
Наконец, для доказательства корректной инициализации CAmkES использует универсальный инициализатор, который запустится как первая пользовательская задача после загрузки. В seL4 эта первая (и уникальная) пользовательская задача имеет доступ ко всей доступной памяти, используя её для создания объектов и «способностей» в соответствии с подробным описанием capDL, которое она принимает в качестве входных данных. Доказано, что состояние после выполнения инициализатора удовлетворяет состоянию, описанному в заданной спецификации. Это доказательство справедливо для точной модели инициализатора, но ещё не на уровне реализации. По сравнению с глубиной остальной цепи доказательств это ограничение может показаться слабым, но оно уже является более формальным доказательством, чем требуется на высшем уровне (EAL7) общих критериев оценки безопасности.
На практике трудно обеспечить разработку системы с нуля ради безопасности, поэтому решающее значение для разработки безопасных систем имеет возможность модернизации старого ПО. Наш фреймворк на базе seL4 поддерживает итеративный процесс, который мы называем «сейсмическая модернизация безопасности», как обычный архитектор модернизирует существующие здания для большей сейсмоустойчивости. Проиллюстрируем процесс на примере постепенной адаптации существующей программной архитектуры беспилотного вертолёта, перейдя от традиционного схемы тестирования к высоконадёжной системе с теоремами, подкреплёнными формальными методами. Хотя этот пример основан на реальном проекте ULB, здесь он упрощён и не включает все детали.
Оригинальная архитектура вертолёта совпадает с архитектурой, описанной на рис. 3. Его функциональность обеспечивают два отдельных компьютера: навигационный вычислитель управляет фактическим полётом, а бортовой компьютер выполняет задачи высокого уровня (такие как связь с наземной станцией и навигация по картинке с камеры). Первоначальная версия бортового компьютера была монолитным приложением под Linux. В процессе модернизации инженеры компании «Боинг» применили методы, инструменты и компоненты, предоставленные партнёрами по программе HACMS.
Первым шагом было принять систему как есть и запустить ее в виртуальной машине поверх безопасного гипервизора (см. рис. 7). В метафоре сейсмической модернизации это соответствует размещению системы на более подвижном фундаменте. Виртуальная машина поверх seL4 в этой системе состоит из одного компонента CAmkES, который включает монитор виртуальной машины (VMM) и гостевую операционную систему, в данном случае Linux. Ядро предоставляет абстракции оборудования виртуализации, а VMM управляет этими абстракциями для виртуальной машины. Ядро seL4 ограничивает не только гостевую ОС, но и VMM, поэтому не нужно доверять реализации VMM для обеспечения принудительной изоляции. Отказ VMM приведёт к отказу гостевой ОС, но не к отказу всей системы.
Рис. 7. Все функциональные возможности в одной виртуальной машине
В зависимости от конфигурации системы, виртуальная машина может иметь доступ к устройствам через паравиртуализированные драйверы, сквозные драйверы или обоими способами. В случае сквозных драйверов разработчики могут использовать системный MMU или IOMMU для предотвращения нарушения границ изоляции аппаратными устройствами и драйверами в гостевой системе. Обратите внимание, что простой запуск системы на виртуальной машине не добавляет дополнительных преимуществ безопасности или надёжности. Шаг 1 нужен только для подготовки к шагу 2.
Второй шаг сейсмической модернизации усиливает существующие стены. В программном обеспечении разработчик может повысить безопасность и надёжность, разделив исходную систему на несколько подсистем, каждая из которых состоит из виртуальной машины, выполняющей код только части исходной системы. Каждая комбинация VM/VMM выполняется в отдельном компоненте CAmkES, который внедряет изоляцию между разными подсистемами, не позволяя им влиять друг на друга, а затем допускает сожительство разных уровней безопасности.
В целом, разделы следуют существующей архитектуре ПО, хотя если архитектуры недостаточно для эффективной изоляции, может потребоваться перепроектирование.
Как правило, разделы должны взаимодействовать друг с другом, так что на этом этапе мы также добавим каналы связи. Для обеспечения безопасности крайне важно, чтобы эти интерфейсы были узкими, ограничивая связь между разделами только тем, что абсолютно необходимо. Кроме того, интерфейсные протоколы должны быть эффективными, с минимальным количеством сообщений или объёмом данных. Критически важно, что seL4 позволяет контролировать и ограничивать обмен памятью между разделами, чтобы минимизировать объём данных.
Помимо виртуальных машин, представляющих подсистемы исходной системы, мы также извлекаем и реализуем компоненты для любых общих ресурсов (таких как сетевой интерфейс).
Можно повторять шаг 2 до тех пор, пока мы не достигнем желаемой детализации разделов. Правильная детализация — это компромисс между прочностью изоляции, с одной стороны, и повышенными накладными расходами на коммуникации и затратами на реконструкцию, с другой стороны.
В нашем примере мы получили три раздела: виртуальную машину, реализующую функции связи наземной станции под управлением Linux; другую виртуальную машину, реализующую функции навигации на основе камеры (также работающую под управлением Linux); и нативный компонент, предоставляющий общий доступ к сети, как показано на рис. 8.
Рис.8. Функциональность разделена на несколько виртуальных машин
Когда система разложена на отдельные разделы виртуальной машины, некоторые или все отдельные разделы можно повторно реализовать в виде нативных компонентов, а не виртуальных машин. Это значительно уменьшит поверхность атаки для той же функциональности. Дополнительное преимущество преобразования компонента в машинный код — снижение нагрузки и повышение производительности, удаление гостевой ОС и накладных расходов на исполнение кода и коммуникации VMM.
Нативные компоненты также повышают потенциал применения формальной верификации и других методов для повышения надёжности компонента. Варианты разные: от полной функциональной проверки собственного кода до совместной генерации кода и доказательств, проверки модели, использования типобезопасных языков программирования, статического анализа или традиционного тщательного тестирования меньшей кодовой базы.
Благодаря изоляции, которую обеспечивают seL4 и компонентная архитектура, становится возможной совместная работа в системе компонентов с разными уровнями надёжности. В этом случае компоненты низкой надёжности не уменьшают общую надёжность системы, а разработчики выигрывают от того, что не нужно тратить усилия на верификацию этого кода.
В нашем примере разберём на нативные модули виртуальную машину для канала связи между бортовым компьютером и наземной станцией. В нативных компонентах реализуются функции связи, криптографии и управления (mission-manager). Мы оставим в виртуальной машине камеру и WiFi как ненадёжный устаревший компонент (см. рис. 9). Такое разделение стало компромиссом между усилиями по переделке подсистем и выгодами от использования нативных компонентов с точки зрения производительности и надёжности.
Рис. 9. Функциональность реализована в нативных компонентах
Получив все необходимые модули, сделаем заключительный шаг: анализ всей системы в целом на основе надёжности архитектуры и отдельных компонентов.
В рамках HACMS коммуникация, криптография, и модуль управления реализованы на доказуемо типобезопасном предметно-ориентированном языке Ivory, с выделением фиксированного объёма памяти в куче. Без дополнительной верификации Ivory не даёт нам гарантий функциональной корректности, но даёт уверенность в отказоустойчивости и аварийной надёжности. Учитывая изоляцию компонентов, мы считаем, что эти гарантии сохраняются в присутствии ненадёжных компонентов (таких как виртуальная машина камеры).
Сетевой компонент реализован на стандартном коде C, состоящем из пользовательского кода для платформы и уже существующего кода библиотеки. Его уровень надёжности соответствует уровню, полученному благодаря тщательной реализации известного кода. Надёжность можно повысить без особых затрат с помощью таких методов, как синтез драйверов, а также с помощью типобезопасных языков вроде Ivory. В общем анализе безопасности системы любая компрометация сетевого компонента повлияет только на сетевые пакеты. Поскольку трафик зашифрован, такая атака не поставит под угрозу условие из спецификаций, что в бортовой компьютер попадают только авторизованные команды.
Виртуальная машина видеокамеры — самая слабая часть системы, так как она работает в системе Linux и в ней предполагается наличие уязвимостей. Но VM изолирована, так что если злоумышленники её взломают, они не смогут перейти к другим компонентам. Самое худшее, что может сделать злоумышленник, — это отправить неверные данные компоненту управления. Как и в квадрокоптере, этот компонент проверяет данные, полученные от камеры. И он успешно выдержал кибератаку, упомянутую в начале статьи. Это была атака типа «белый ящик», где команде пентестеров дали доступ ко всему коду и документации, а также ко всем внешним каналам коммуникаций. Ей намеренно предоставили рутовый доступ к виртуальной машине камеры, имитируя успешную атаку на устаревшее программное обеспечение. Сдерживание атаки и способность защититься от этого очень мощного сценария стали достойной проверкой наших требований безопасности и выявления любых пропущенных предположений, проблем интерфейса или других проблем безопасности, которые исследовательская группа могла не распознать.
В этой статье приведён обзор метода достижения очень высоких уровней безопасности для систем, в которых свойство безопасности применимо через компонентную архитектуру. Мы доказали теоремы для уровня ядра и его правильной конфигурации, а также теоремы, которые гарантируют, что компонентная платформа правильно настраивает границы защиты в соответствии с описанием своей архитектуры, и что она генерирует правильный код для удалённых вызовов процедур. Связь с высокоуровневым анализом безопасности системы остаётся неформальной, а теоремы коммуникационного кода не покрывают все примитивы коммуникаций, предоставленные платформой. Для автоматического получения теоремы, которая покрывает всю систему от начала до конца, требуется проделать дополнительную работу. Однако на данном этапе ясно, что это осуществимая задача.
Основная цель представленной работы заключается в резком сокращении усилий по проверке для конкретных классов систем. Описанный здесь чисто архитектурный подход можно расширить на другие системы, кроме ULB, но он явно ограничен тем фактом, что может выражать только свойства, которые определяются компонентной архитектурой системы. Отдача уменьшится, если эта архитектура изменяется во время выполнения программы, а также если свойства критически зависят от поведения слишком большого числа доверенных компонентов или компонентов слишком большого размера.
Первый шаг к ослаблению этих ограничений — создание библиотеки предварительно проверенных компонентов высокого уровня надёжности для использования в качестве надёжных строительных блоков в таких архитектурах. Эта библиотека может включать шаблоны безопасности (такие как дезинфекция входных данных, фильтры вывода, мониторы снижения уровня секретности и времени выполнения), потенциально сгенерированные из спецификаций более высокого уровня, а также такие компоненты инфраструктуры, как повторно используемые криптомодули, хранилище ключей, файловые системы, сетевые стеки и драйверы высокой надёжности. Если безопасность зависит более чем от одного такого компонента, то возникает необходимость обосновать надёжность их взаимодействия и совместного использования. Основными техническими проблемами здесь являются рассуждения о параллелизме и протоколах, а также о потоке информации в присутствии доверенных компонентов. Несмотря на эти ограничения, работа демонстрирует быстрое развитие реальных высоконадёжных систем на основе seL4. В настоящее время создание таких систем возможно за меньшую стоимость, чем традиционное тестирование.
Разработка дизайна и кода seL4 заняла два человеко-года. Если добавить все серотип-специфичные доказательства, в общей сложности получится 18 человеко-лет для 8700 строк кода на C. Для сравнения, разработка сравнимого по размеру микроядра L4Ka::Pistachio из семейства seL4 заняло шесть человеко-лет и не обеспечило значительного уровня надёжности. Это означает разницу по скорости разработки всего лишь в 3,3 раза между верифицированным и традиционным софтом. Согласно методу оценки Кольбера и Бома, сертификация по традиционным критериям EAL7 для 8700 строк кода C займёт более 45,9 человеко-лет. Это означает, что формальная верификация реализации на бинарном уровне уже в 2,3 раза дешевле, чем самый высокий уровень сертификации по общим критериям, при этом обеспечивает значительно более высокую надёжность.
Для сравнения, описанный здесь подход HACMS использует для каждой новой системы только существующие доказательства, включая доказательства, сгенерированные инструментами. Таким образом, общие усилия по доказательству для системы, которая соответствует этому подходу, сводятся к человеко-неделям, а не годам, а тестирование сводится только к проверке допущений.
В феврале 2017 года со взлётной площадки «Боинга» в Аризоне поднялся вертолёт с обычным заданием: облёт ближайших холмов. Он летел полностью автономно. Согласно требованиям по технике безопасности Федерального управления авиации США, пилот не прикасался к органам управления. Это был не первый автономный полёт AH-6, которого в компании называют Беспилотной Птичкой (Unmanned Little Bird, ULB). Он так летает уже много лет. Однако на этот раз посреди полёта вертолёт подвергся кибератаке. Бортовой компьютер атаковало вредоносное программное обеспечение видеокамеры, а также вирус, доставленный через заражённую флэшку, которую вставили во время техобслуживания. Атака поставила под угрозу некоторые подсистемы, но не смогла повлиять на безопасную эксплуатацию воздушного судна.Ключевые идеи
- Формальные доказательства из программной архитектуры верифицированного микроядра можно недорого масштабировать на реальные системы.
- Возможны и желательны разные уровни безопасности и надёжности в рамках одной системы. Необязательно обеспечивать максимальную надёжность всего кода.
- Достаточно умеренного редизайна и рефакторинга, чтобы поднять существующие системы до уровня высоконадёжного кода.
Можно подумать, что военная авиация с лёгкостью отразит подобную кибератаку. В реальности же команда профессиональных пентестеров по заказу агентства DARPA в рамках программы по разработке высоконадёжных военных компьютерных систем High-Assurance Cyber Military Systems (HACMS) в 2013 году успешно взломала первую версию программного обеспечения ULB, которое изначально разрабатывалось для обеспечения безопасности полётов, а не защиты от кибератак. Хакеры получили возможность разбить вертолёт или посадить его на любое место по своему желанию. Поэтому риск таких атак с пассажиром на борту трудно переоценить, а неудачная попытка взлома в феврале 2017 года указывает на некие фундаментальные изменения в ПО.
В этой статье объясняются эти изменения и технология, которая сделала их возможными. Речь идёт о технологии, разработанной в рамках программы HACMS, направленной на обеспечение безопасной работы критических систем во враждебной киберсреде — в данном случае, нескольких автономных транспортных средств. Технология основана на формальной верификации программного обеспечения — это программы с автоматически проверенными математическими доказательствами, которое работает в соответствии со своей спецификацией. Хотя статья не посвящена самим формальным методам, она объясняет, как использовать верификацию артефактов для защиты реальных систем на практике.
Возможно, самый впечатляющий результат HACMS — что технологию можно распространить на существующие реальные системы, значительно улучшив их защиту от кибератак. Этот процесс называется «сейсмической модернизацией безопасности» (seismic security retrofit) по аналогии с сейсмической модернизацией зданий. Более того, большая часть реинжиниринга сделана инженерами компании «Боинг», а не специалистами по формальной верификации.
«Птичка» во время беспилотного испытательного полёта
Далеко не весь софт на вертолёте построен на математических моделях и доказательствах. Область формальной верификации ещё не готова к такому масштабу. Тем не менее, программа HACMS продемонстрировала, что стратегическое применение формальных методов к наиболее важным частям общей системы значительно улучшает защиту. Подход HACMS работает для систем, в которых желаемое свойство безопасности может быть достигнуто посредством чисто принудительного применения на уровне архитектуры. В его основе — наше верифицированное микроядро sel4, о котором поговорим ниже. Оно гарантирует изоляцию между подсистемами, за исключением чётко определённых каналов связи, на которые распространяется политика безопасности системы. Эта изоляция гарантируется на уровне архитектуры с помощью верифицированного фреймворка CAmkES для системных компонентов. С помощью предметно-ориентированных языков от Galois Inc. платформа CAmkES интегрируется с инструментами анализа архитектуры от Rockwell Collins и университета Миннесоты, а также с высоконадёжными программными компонентами.
Достижения HACMS основаны на старом верном друге инженера-программиста — модуляризации. Инновация в том, что формальные методы доказывают наблюдаемость интерфейсов и инкапсуляцию внутренностей модулей. Это гарантированное соблюдение модульности позволяет инженерам, которые не являются экспертами по формальным методам (как в компании «Боинг»), создавать новые или даже модернизировать существующие системы и достигать высокой устойчивости. Хотя инструменты пока не обеспечивают полного доказательства безопасности системы.
Формальная верификация
Доказательства математической корректности программ восходят, по крайней мере, к 1960-м годам, но долгое время их реальная польза для разработки программного обеспечения была ограничена масштабом и глубиной. Однако в последние годы произошёл ряд впечатляющих прорывов в формальной верификации на уровне кода реальных систем, от верифицированного компилятора C CompCert до верифицированного микроядра seL4 (см. научные статьи о нём), верифицированной системы конференц-связи CoCon, верифицированного ML-компилятора CakeML, верифицированных программ для доказательства теорем Milawa и Candle, верифицированной файловой системы с защитой от сбоев FSCQ, верифицированной распределённой системы IronFleet и верифированного фреймворка параллельного ядра CertiKOS, а также важных математических теорем, в том числе проблемы четырёх красок, автоматического доказательства гипотезы Кеплера и теоремы Фейта — Томпсона о нечётном порядке. Всё это настоящие системы. Например, CompCert — коммерческий продукт, микроядро seL4 используется в аэрокосмической и беспилотной авиации, в качестве платформы Интернета вещей, а система CoCon использовалась на многочисленных крупных научных конференциях.
Эти проекты верификации требуют значительных усилий. Чтобы сделать формальные методы общедоступными, эти усилия необходимо сократить. Здесь мы демонстрируем, как стратегическое сочетание формальных и неформальных методов, частичная автоматизация формальных методов и тщательная разработка программного обеспечения для максимизации преимуществ изолированных компонентов позволили нам значительно повысить надёжность систем, общий размер и сложность которых на порядки больше, чем у упомянутых выше.
Обратите внимание, мы применяем формальную верификацию в первую очередь для кода, от которого зависит безопасность системы. Но есть и другие преимущества. Например, доказательства корректности кода делают предположения о контексте, в котором он выполняется (например, о поведении оборудования и конфигурации программного обеспечения). Формальная верификация делает эти предположения явными, что помогает разработчикам сфокусироваться на других средствах верификации, таких как тестирование. Кроме того, во многих случаях система включает и проверенный, и непроверенный код. Во время код-ревью, тестирования и отладки формальная верификация действует как объектив, фокусируя внимание на критическом непроверенном коде системы.
seL4
Начнём с фундамента для построения доказуемо надёжных систем — ядра операционной системы (ОС). Это наиболее важная часть, которая экономически эффективно гарантирует надёжность всей системы.
Микроядро seL4 предоставляет формально верифицированный минимальный набор механизмов для реализации защищённых систем. В отличие от стандартных ядер, оно целенаправленно универсально и поэтому подходит для реализации ряда политик безопасности и системных требований.
Одна из основных целей разработки seL4 заключается в обеспечении сильной изоляции между взаимно не доверяющими друг другу компонентами, которые работают поверх ядра. Поддерживается его работа в качестве гипервизора, например, для целых операционных систем Linux, сохраняя при этом их изолированными от критичных для безопасности компонентов, которые могут работать вместе, как показано на рисунке 1. В частности, эта функция позволяет разработчикам систем использовать устаревшие компоненты со скрытыми уязвимостями рядом с высоконадёжными компонентами.
Рис. 1. Изоляция и контролируемые коммуникации в seL4
Ядро seL4 занимает особое положение среди микроядер общего назначения. Мало того, что оно обеспечивает лучшую производительность в своем классе, его 10 000 строк кода C прошли более тщательную формальную верификацию, чем любое другое общедоступное программное обеспечение в истории человечества с точки зрения не только строк доказательства, но и прочности доказанных свойств. В основе лежит доказательство «функциональной корректности» реализации ядра на C. Оно гарантирует, что любое поведение ядра предсказывается его формальной абстрактной спецификацией: см. онлайн-приложение для представления о том, как выглядят эти доказательства. Следуя этой гарантии, мы добавили дополнительные доказательства, которые объясним после введения в основные механизмы ядра.
seL4 API
Ядро seL4 предоставляет минимальный набор механизмов для реализации защищённых систем: потоки, управление «способностями», виртуальные адресные пространства, межпроцессное взаимодействие (IPC), сигнализация и доставка прерываний.
Ядро сохраняет своё состояние в «объектах ядра». Например, для каждого потока в системе существует «объект потока», хранящий информацию о шедулинге, выполнении и управлении доступом. Программы пользовательского пространства могут ссылаться на объекты ядра только косвенно через так называемые «способности» или «возможности» (capabilities), которые объединяют ссылку на объект с набором прав доступа к нему. Например, поток не может запустить или остановить другой поток, если не имеет «способности» для соответствующего объекта потока.
Потоки взаимодействуют и синхронизируются путём отправки сообщений через объекты «конечная точка» (endpoint) межпроцессного взаимодействия. Один поток со способностью отправки на соответствующую конечную точку может отправить сообщение другому потоку, имеющему способность получения на эту конечную точку. Объекты «уведомление» (notification) обеспечивают синхронизацию через наборы двоичных семафоров. Виртуальное преобразование адресов управляется объектами ядра, которые представляют каталоги страниц, таблицы страниц и объекты фреймов или тонкие абстракции над соответствующими объектами процессорной архитектуры. У каждого потока есть определённая способность “VSpace”, которая указывает на корень дерева объектов преобразования адресов потока. Сами возможности управляются ядром и хранятся в объектах ядра “CNodes”, расположенных в структуре графа, который сопоставляет ссылки на объекты с правами доступа, аналогично сопоставлению виртуальных таблиц страниц с физическими адресами в памяти. У каждого потока своя способность идентификации корневого CNode. Набор способностей, доступных из этого корня, мы называем «CSpace потока». Способности могут передаваться через конечные точки с передачей работы, а также их можно объявлять общими с помощью общих CSpace. Рисунок 2 демонстрирует эти объекты ядра.
Рис. 2. Объекты ядра в системе на seL4 с двумя потоками, взаимодействующими через конечную точку
Доказательства безопасности
Благодаря своей универсальности API-интерфейсы ядра seL4 работают на низком уровне и поддерживают высокодинамичные системные архитектуры. Поэтому прямые доказательства для этих API проблематично получить.
Высокоуровневая концепция политик управления доступом абстрагируется от отдельных объектов и возможностей ядра, захватывая вместо этого конфигурацию управления доступом системы с помощью набора абстрактных «субъектов» (компонентов) и полномочий, которые каждый из них имеет над другими (например, для чтения данных и отправки сообщений). В примере на рис. 2, компоненты A и B получили полномочия над конечной точкой.
В работе Сьюэлла с коллегами доказано, что политики контроля доступа seL4 гарантируют соблюдение двух основных свойств безопасности: ограничение полномочий и целостность.
Ограничение полномочий означает, что политика контроля доступа является статическим (неизменным) безопасным приближением конкретных возможностей и объектов ядра в системе для любого будущего состояния. Это свойство подразумевает, что независимо от того, как развивается система, ни один компонент никогда не получит больше полномочий, чем предсказывает политика контроля доступа. На рисунке 2 политика для компонента B не содержит доступа на запись к компоненту A. Таким образом, компонент B никогда не сможет получить этот доступ в будущем. Это свойство подразумевает, что рассуждения на уровне политики являются безопасным приближением к рассуждениям о конкретном состоянии контроля доступа в системе.
Целостность означает, что независимо от того, что делает компонент, он никогда не сможет изменять данные в системе (включая любые системные вызовы, которые он может выполнять), которые ему явно не разрешает изменять политика контроля доступа. Например, на рис. 2 единственным компонентом полномочий A над другим компонентом является право отправки данных на конечную точку, откуда получает информацию компонент B. Это означает, что компонент А способен изменять только своё состояние, состояние потока B и состояние буфера сообщений. Он не может изменять другие части системы.
Побочный эффект целостности — это конфиденциальность, когда компонент не способен без разрешения прочитать информацию из другого компонента: это доказанное сильное свойство нетранзитивного невмешательства seL4. То есть в должным образом настроенной системе (с более жёсткими ограничениями, чем просто для целостности) ни один из компонентов не сможет без разрешения узнать информацию о другом компоненте или его исполнении. Доказательство выражает это свойство в терминах политики информационного потока, которую можно извлечь из политики управления доступом, используемой в доказательстве целостности. Информация будет передаваться только тогда, когда это явно разрешено политикой. Доказательство охватывает явные информационные потоки, а также потенциальные каналы скрытого хранения в ядре. Но каналы синхронизации находятся вне его области и должны обрабатываться иными средствами.
Дальнейшие доказательства в seL4 включают расширение функциональной корректности и, следовательно, теорем безопасности до бинарного уровня для архитектуры ARMv7 и профиль худшего времени выполнения для ядра (1, 2), необходимый для систем реального времени. Ядро seL4 доступно для разных архитектур: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 и Intel x64. На данный момент оно прошло машинную проверку на архитектуре ARMv7 для всего стека верификации, а также на ARMv7a с расширениями гипервизора для функциональной корректности.
Безопасность по архитектуре
В предыдущем разделе описаны программные методы, с помощью которых ядро seL4 создаёт прочный фундамент для доказуемо надёжных систем. Ядро формирует достоверную вычислительную базу (TCB) — обязательный компонент программного обеспечения, которое обязано работать корректно для гарантированной безопасности системы. В реальных системах эта база гораздо шире, чем просто микроядро. Нужно верифицировать дополнительный программный стек, чтобы получить тот же уровень уверенности, что и для ядра. Однако существуют классы систем, для которых нет необходимости в такой верификации: им достаточно теорем изоляции на уровне ядра для выведения определённых свойств безопасности на уровне системы. В этом разделе приведён пример такой системы.
Это системы, в которых архитектуры компонентов уже реализовали критическое свойство, возможно, вместе с несколькими небольшими доверенными компонентами. Наш пример — ПО управления полётом квадрокоптера, демонстрационного аппарата в упомянутой ранее программе HACMS.
На рисунке 3 показаны основные аппаратные компоненты квадрокоптера. Архитектура намеренно более сложная, чем требуется для квадрокоптера, поскольку она должна была представлять ULB и на этом уровне абстракции сходна с архитектурой ULB.
Рис. 3. Архитектура автономного летательного аппарата
На рисунке изображены два основных компьютера: бортовой компьютер, который взаимодействует с наземной станцией и управляет программным обеспечением на борту (например, камерой), и навигационный вычислитель для управления полётом транспортного средства, считывания данных датчиков и управления двигателями. Компьютеры связаны через внутреннюю сеть или шину CAN на квадрокоптере, Ethernet на ULB. На квадрокоптере также есть незащищённая точка WiFi, что даёт возможность продемонстрировать дополнительные методы защиты.
В данном примере рассмотрим бортовой компьютер. Для него должны исполняться четыре основных свойства:
- правильная аутентификация команд от наземной станции;
- приватность криптографических ключей;
- никаких дополнительных сообщений для навигационного вычислителя;
- ненадёжное ПО с других бортовых систем не может влиять на полёт аппарата.
Рабочая гипотеза состоит в том, что камера ненадёжна, потенциально скомпрометирована или вредоносна, что её драйверы и устаревшее ПО потенциально скомпрометированы, также как любые внешние каналы коммуникации. В этом примере мы предполагаем правильную и сильную криптографию, то есть что ключ нельзя подобрать, и выводим за рамки задачи возможность подавления противником радиосвязи с наземной станцией.
На рисунке 4 показано, как спроектирована архитектура квадрокоптера, которая обеспечивает эти свойства. Виртуальная машина (VM) под Linux служит контейнером для устаревшего программного обеспечения бортовых устройств, драйверов камер и точки WiFi. Изолируем модуль управления криптографией в собственном компоненте, с подключениями к шине CAN, каналу наземной станции и к виртуальной машине Linux для отправки данных на наземную станцию. Задача криптографического компонента — передавать (только) авторизованные сообщения в бортовой компьютер через CAN-интерфейс стека и отправлять диагностические данные обратно на наземную станцию. Компонент радиосвязи отправляет и получает необработанные сообщения, которые шифруются и расшифровываются (с аутентификацией) криптографическим компонентом.
Рис.4. Упрощённая архитектура бортового компьютера квадрокоптера
Установка желаемых свойств системы сводится исключительно к свойствам изоляции и поведению архитектуры в части информационных потоков, а также к поведению единственного доверенного криптографического компонента. Если предположить правильное поведение этого компонента, ключи не могут быть скомпрометированы, так как ни один другой компонент не имеет к ним доступа. Канал между Linux и криптографическим компонентом на рис. 4 предназначен только для передачи сообщений и не даёт доступа к памяти. В шину CAN могут попасть только авторизованные сообщения, потому что криптографический компонент — единственная связь с шиной. Ненадёжное ПО и WiFi, как часть виртуальной машины Linux, инкапсулируются изоляцией компонентов и могут взаимодействовать с остальной частью системы только через доверенный криптографический компонент.
Легко представить, что такого рода анализ архитектуры можно в значительной степени автоматизировать с помощью проверки моделей и инструментов механических рассуждений более высокого уровня. Как было отмечено для систем MILS, границы компонентов в такой архитектуре — не только удобный инструмент разбиения на модули и управления кодом, но с принудительной изоляцией обеспечивают эффективные границы для формальных рассуждений о поведении системы. Однако всё зависит от правильного применения границ компонентов во время выполнения в окончательной бинарной реализации системы.
Обсуждавшиеся ранее механизмы ядра seL4 способны обеспечить такую реализацию, но уровень абстракции механизмов резко контрастирует с блоками и стрелками архитектурной схемы: даже более абстрактная политика управления доступом по-прежнему содержит гораздо больше деталей, чем схема архитектуры. В реальной системе такого размера десятки тысяч объектов ядра и «способностей», созданных программно, а ошибки в конфигурации могут привести к нарушениям безопасности. Затем обсудим, каким образом мы не только автоматизируем конфигурацию и создание такого кода, но и как автоматически доказать соблюдение границ архитектуры.
Верификация компонентного представления
Как доказательства безопасности упрощаются с формальными абстракциями политик безопасности, также абстракция помогает в разработке систем. Компонентная платформа Camkes работает на абстракциях seL4 поверх низкоуровневых механизмов ядра, обеспечивая коммуникационные примитивы и декомпозицию системы на функциональные единицы, как показано на рис. 5. Используя эту платформу, системные архитекторы могут проектировать и строить системы на основе seL4 с точки зрения компонентов высокого уровня, которые взаимодействуют друг с другом и с аппаратными устройствами через коннекторы, такие как удалённые вызовы процедур (RPC), датапорты и события.
Рис. 5. Рабочий процесс CAmkES
Генерация кода
Внутренне CAmkES реализует эти абстракции с помощью низкоуровневых объектов ядра seL4. Каждый компонент содержит (по крайней мере) один поток, CSpace и VSpace. Коннекторы RPC используют объекты конечной точки, и CAmkES генерирует промежуточный код для обработки сообщений и передачи их по конечным точкам IPC. Аналогичным образом, коннектор датапорта реализуется через общую память — общие фреймы, присутствующие в адресных пространствах двух компонентов — и опционально может ограничить направление передачи данных. Наконец, коннектор событий реализован с помощью механизма уведомлений seL4.
CAmkES также генерирует на языке capDL низкоуровневую спецификацию начальной конфигурации объектов и возможностей ядра системы. Эта спецификация становится входными данными для инициализатора seL4, который первым запускается после загрузки и выполняет необходимые операции seL4 для создания инстанса и инициализации системы.
Таким образом, платформа компонентов генерирует код без дополнительных усилий со стороны разработчика. Компонентная архитектура описывает набор блоков и стрелок, а задача реализации сводится к простому заполнению полей. Платформа генерирует остальное, обеспечивая реализацию описанной архитектуры.
На платформе с традиционными компонентами сгенерированный код расширит доверенную вычислительную базу системы, поскольку он может влиять на функциональность компонентов. Однако CAmkES также генерирует доказательства.
Автоматические доказательства
При генерации «промежуточного» кода CAmkES производит формальные доказательства в Isabelle/HOL, выполняя валидацию в процессе трансляции и демонстрируя, что сгенерированный «промежуточный» код подчиняется спецификации высокого уровня, а сгенерированная спецификация capDL является правильным уточнением описания CAmkES. Мы также доказали, что инициализатор seL4 правильно настраивает систему в требуемой начальной конфигурации. При этом мы автоматизируем большую часть построения системы без расширения доверенной вычислительной базы.
Разработчики редко смотрят на выдачу генераторов кода, их интересует только функциональность и бизнес-логика. Так же и мы предполагаем, что доказательства для промежуточного кода не нуждаются в проверке, то есть разработчики могут сосредоточиться на доказательстве корректности собственного кода. Как сгенерированный CAmkES заголовок даёт разработчику API для сгенерированного кода, так и операторы леммы верхнего уровня производят API для доказательств. Леммы описывают ожидаемое поведение коннекторов. В примере промежуточного кода RPC на рис. 6 сгенерированная функция предоставляет способ вызова удалённой функции в другом компоненте. Чтобы сохранить абстракции, вызов должен быть эквивалентен вызову . Сгенерированная системой лемма гарантирует, что из сгенерированного кода RPC ведёт себя как прямой вызов .
Рис. 6. Cгенерированный код RPC
Для реального использования сгенерированных системой доказательств они должны быть компонуемы с (почти) произвольными доказательствами, предоставленными пользователем, как для функции , так и для контекстов, в которых используются и . Чтобы добиться этой компонуемости, спецификация коннекторов параметризуется через предоставленные пользователем спецификации удалённых функций. Таким образом, инженеры могут рассуждать о своей архитектуре, предоставляя спецификации и доказательства для своих компонентов, и полагаться на спецификации для сгенерированного кода.
На сегодняшний день мы продемонстрировали этот процесс от начала и до конца с помощью специального коннектора CAmkES RPC (1, 2). Поскольку шаблоны других коннекторов (датапорты и события) значительно проще, чем RPC, будет несложно расширить генератор доказательств для поддержки этих коннекторов, что позволит создавать более разнообразные верифицированные системы.
После кода для коммуникации CAmkES создаёт начальную конфигурацию управления доступом для применения границ архитектуры. Чтобы доказать, что эти два описания системы — capDL и CAmkES — соответствуют друг другу, рассмотрим описание CAmkES как абстракцию для описание capDL. Используем упомянутый ранее проверенный фреймворк, чтобы вывести полномочия одного объекта над другим объектом из описания capDL. Так мы повысим доказательство до уровня политики. Кроме того, мы определили правила для вывода полномочий между компонентами в описании CAmkES. Полученное доказательство гарантирует, что у объектов capDL, представленных в виде графа полномочий с объектами, сгруппированными по компонентам, те же границы между группами, что и в эквивалентном графе компонентов CAmkES. Интуитивно, такое соответствие границ означает, что анализ архитектуры политики из описания CAmkES сохранит политику из описания, сгенерированного capDL, которое, в свою очередь, гарантированно удовлетворяет требованиям ограничения полномочий, целостности и конфиденциальности, как упоминалось ранее.
Наконец, для доказательства корректной инициализации CAmkES использует универсальный инициализатор, который запустится как первая пользовательская задача после загрузки. В seL4 эта первая (и уникальная) пользовательская задача имеет доступ ко всей доступной памяти, используя её для создания объектов и «способностей» в соответствии с подробным описанием capDL, которое она принимает в качестве входных данных. Доказано, что состояние после выполнения инициализатора удовлетворяет состоянию, описанному в заданной спецификации. Это доказательство справедливо для точной модели инициализатора, но ещё не на уровне реализации. По сравнению с глубиной остальной цепи доказательств это ограничение может показаться слабым, но оно уже является более формальным доказательством, чем требуется на высшем уровне (EAL7) общих критериев оценки безопасности.
Сейсмическая модернизация безопасности
На практике трудно обеспечить разработку системы с нуля ради безопасности, поэтому решающее значение для разработки безопасных систем имеет возможность модернизации старого ПО. Наш фреймворк на базе seL4 поддерживает итеративный процесс, который мы называем «сейсмическая модернизация безопасности», как обычный архитектор модернизирует существующие здания для большей сейсмоустойчивости. Проиллюстрируем процесс на примере постепенной адаптации существующей программной архитектуры беспилотного вертолёта, перейдя от традиционного схемы тестирования к высоконадёжной системе с теоремами, подкреплёнными формальными методами. Хотя этот пример основан на реальном проекте ULB, здесь он упрощён и не включает все детали.
Оригинальная архитектура вертолёта совпадает с архитектурой, описанной на рис. 3. Его функциональность обеспечивают два отдельных компьютера: навигационный вычислитель управляет фактическим полётом, а бортовой компьютер выполняет задачи высокого уровня (такие как связь с наземной станцией и навигация по картинке с камеры). Первоначальная версия бортового компьютера была монолитным приложением под Linux. В процессе модернизации инженеры компании «Боинг» применили методы, инструменты и компоненты, предоставленные партнёрами по программе HACMS.
Шаг 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. Надёжность системы в целом
Получив все необходимые модули, сделаем заключительный шаг: анализ всей системы в целом на основе надёжности архитектуры и отдельных компонентов.
В рамках HACMS коммуникация, криптография, и модуль управления реализованы на доказуемо типобезопасном предметно-ориентированном языке Ivory, с выделением фиксированного объёма памяти в куче. Без дополнительной верификации Ivory не даёт нам гарантий функциональной корректности, но даёт уверенность в отказоустойчивости и аварийной надёжности. Учитывая изоляцию компонентов, мы считаем, что эти гарантии сохраняются в присутствии ненадёжных компонентов (таких как виртуальная машина камеры).
Сетевой компонент реализован на стандартном коде C, состоящем из пользовательского кода для платформы и уже существующего кода библиотеки. Его уровень надёжности соответствует уровню, полученному благодаря тщательной реализации известного кода. Надёжность можно повысить без особых затрат с помощью таких методов, как синтез драйверов, а также с помощью типобезопасных языков вроде Ivory. В общем анализе безопасности системы любая компрометация сетевого компонента повлияет только на сетевые пакеты. Поскольку трафик зашифрован, такая атака не поставит под угрозу условие из спецификаций, что в бортовой компьютер попадают только авторизованные команды.
Виртуальная машина видеокамеры — самая слабая часть системы, так как она работает в системе Linux и в ней предполагается наличие уязвимостей. Но VM изолирована, так что если злоумышленники её взломают, они не смогут перейти к другим компонентам. Самое худшее, что может сделать злоумышленник, — это отправить неверные данные компоненту управления. Как и в квадрокоптере, этот компонент проверяет данные, полученные от камеры. И он успешно выдержал кибератаку, упомянутую в начале статьи. Это была атака типа «белый ящик», где команде пентестеров дали доступ ко всему коду и документации, а также ко всем внешним каналам коммуникаций. Ей намеренно предоставили рутовый доступ к виртуальной машине камеры, имитируя успешную атаку на устаревшее программное обеспечение. Сдерживание атаки и способность защититься от этого очень мощного сценария стали достойной проверкой наших требований безопасности и выявления любых пропущенных предположений, проблем интерфейса или других проблем безопасности, которые исследовательская группа могла не распознать.
Ограничения и будущая работа
В этой статье приведён обзор метода достижения очень высоких уровней безопасности для систем, в которых свойство безопасности применимо через компонентную архитектуру. Мы доказали теоремы для уровня ядра и его правильной конфигурации, а также теоремы, которые гарантируют, что компонентная платформа правильно настраивает границы защиты в соответствии с описанием своей архитектуры, и что она генерирует правильный код для удалённых вызовов процедур. Связь с высокоуровневым анализом безопасности системы остаётся неформальной, а теоремы коммуникационного кода не покрывают все примитивы коммуникаций, предоставленные платформой. Для автоматического получения теоремы, которая покрывает всю систему от начала до конца, требуется проделать дополнительную работу. Однако на данном этапе ясно, что это осуществимая задача.
Основная цель представленной работы заключается в резком сокращении усилий по проверке для конкретных классов систем. Описанный здесь чисто архитектурный подход можно расширить на другие системы, кроме ULB, но он явно ограничен тем фактом, что может выражать только свойства, которые определяются компонентной архитектурой системы. Отдача уменьшится, если эта архитектура изменяется во время выполнения программы, а также если свойства критически зависят от поведения слишком большого числа доверенных компонентов или компонентов слишком большого размера.
Первый шаг к ослаблению этих ограничений — создание библиотеки предварительно проверенных компонентов высокого уровня надёжности для использования в качестве надёжных строительных блоков в таких архитектурах. Эта библиотека может включать шаблоны безопасности (такие как дезинфекция входных данных, фильтры вывода, мониторы снижения уровня секретности и времени выполнения), потенциально сгенерированные из спецификаций более высокого уровня, а также такие компоненты инфраструктуры, как повторно используемые криптомодули, хранилище ключей, файловые системы, сетевые стеки и драйверы высокой надёжности. Если безопасность зависит более чем от одного такого компонента, то возникает необходимость обосновать надёжность их взаимодействия и совместного использования. Основными техническими проблемами здесь являются рассуждения о параллелизме и протоколах, а также о потоке информации в присутствии доверенных компонентов. Несмотря на эти ограничения, работа демонстрирует быстрое развитие реальных высоконадёжных систем на основе seL4. В настоящее время создание таких систем возможно за меньшую стоимость, чем традиционное тестирование.
Приложение: трудозатраты
Разработка дизайна и кода seL4 заняла два человеко-года. Если добавить все серотип-специфичные доказательства, в общей сложности получится 18 человеко-лет для 8700 строк кода на C. Для сравнения, разработка сравнимого по размеру микроядра L4Ka::Pistachio из семейства seL4 заняло шесть человеко-лет и не обеспечило значительного уровня надёжности. Это означает разницу по скорости разработки всего лишь в 3,3 раза между верифицированным и традиционным софтом. Согласно методу оценки Кольбера и Бома, сертификация по традиционным критериям EAL7 для 8700 строк кода C займёт более 45,9 человеко-лет. Это означает, что формальная верификация реализации на бинарном уровне уже в 2,3 раза дешевле, чем самый высокий уровень сертификации по общим критериям, при этом обеспечивает значительно более высокую надёжность.
Для сравнения, описанный здесь подход HACMS использует для каждой новой системы только существующие доказательства, включая доказательства, сгенерированные инструментами. Таким образом, общие усилия по доказательству для системы, которая соответствует этому подходу, сводятся к человеко-неделям, а не годам, а тестирование сводится только к проверке допущений.
Комментарии (23)
old_bear
24.01.2019 20:04я был в экстазе
Чорт, я прямо сейчасзакурилтам нахожусь.
P.S. Даже мимо ветки промахнулся под впечатлением. Или это таки глюк движка?artskep
24.01.2019 20:08Ну, это нормально и понятно. И тема, вообще-то верная, КМК.
Но просто вспомните последний раз, когда вы видели формально оформленные требования от заказчика, и вернитесь в реальность.
А если этого недостаточно, то вспомните теорему о неполноте.
emmibox
24.01.2019 21:26Злоумышленник в потоке камеры сделает вот так и будет глубоко пофигу, что микроядро формально корректно работает, и компилятор формально верифицирован…
А все от того, что есть доверие к процессору. И к памяти доверие тоже есть… А если тяжелая заряженная частица пролетит через ту память?!
amartology
24.01.2019 21:40Зачем тяжёлая заряженная частица? Можно аккуратно лазером посветить в нужный бит памяти)
oteuqpegop
24.01.2019 21:58>Злоумышленник
ИМХО верификация (по крайней мере, на текущем этапе) это больше о надежности, чем о безопасности. Начиная от хитрых физических эффектов типа Rowhammer, некоторые из которых обязательно забудут включить в модель; и заканчивая тем, что в самый первый раз верификатор запускается на неверифицированной системе, которая может быть за счет этого скомпрометирована и намеренно давать ложноположительные результаты (а париться с инкрементальной верификацией и начинать с человекопроверяемого уровня никто не станет). Плюс для верификации нужна сперва спецификация, которая, по сути, тоже код, потенциально содержащий ошибки. Плюс намеренные бэкдоры. Плюс зоопарк периферии и отсутствие контроля над ее производством. Так что это скорее актуально в случае какой-то узкоспециализированной системы, которую очень дорого или невозможно фиксить от багов, но на которую не проводится атак.emmibox
24.01.2019 23:58Они тут конкретную модель угроз заявили. И хакеров притянули за уши к процессу. И суть защиты в изолировании памяти. Так вот в этой модели — и с защитой памяти птичку можно уложить при неких исследованиях «поглубже»…
Верификация просто обычное дело для всякого летающего и мало отношения имеет к взлому.
amarao
24.01.2019 21:49+1А чем формальная спецификация ОС отличается от формального исходного кода ОС? И там и там могут быть баги. Если мы предполагаем, что формальная спецификация не содержит ошибок, то мы можем так же предположить, что исходный код не содержит ошибок. Если же мы допускаем возможность ошибок в формальной спецификации, то это получаются, обычные тесты на необычном языке. Часть багов ловят, но не идеальны.
oteuqpegop
24.01.2019 22:05Тесты не покрывают все возможные пути выполнения обычно, а верификация покрывает. Это скорее можно сравнить с параллельным написанием программы на двух языках. Но в плане багов да.
amarao
24.01.2019 22:52Если представить себе тесты с 100% cyclomatic coverage, то это же оно и будет? То есть люди говорят про «формальное доказательство программы», и все себе представляют волшебную программу без багов. А в реальности — это всего лишь tdd-от-математиков.
oteuqpegop
24.01.2019 23:40unsigned char unsafe_images_vault [100500]; unsigned char kernel_security_settings [256]; //какой-то код void verySecureFunction (size_t l) { memcpy(kitty_image_with_shellcode_ptr, unsafe_images_vault, l); }
Тестовое покрытие не учитывает состояние, разве нет? Если тесты покрывают эту функцию, это ничего в общем случае не говорит о состоянии в момент прохода, а в низкоуровневых языках (да и не только) фактический смысл кода может полностью изменяться при изменении состояния, как в примере выше. Если доступ к памяти никак не ограничивается, то вариантов будет околобесконечное количество для каждой функции, и все не протестируешь.
Ares_ekb
25.01.2019 06:48Нет, это не то же самое. Тестами невозможно покрыть 100%. Даже если покрыты все ветки, остаются ещё все комбинации всех значений переменных. Если в программе есть рекурсивные структуры данных типа списков или деревьев, то количество возможных значений бесконечно.
Там в принципе совершенно другой подход. Например, как выглядят олимпиады по программированию. Дают задание на написание программы, которая что-то делает, дают примеры входных тестовых данных и примеры ожидаемых выходных. Человек пишет программу, запускает её на этих тестовых данных. Добавляет для верности какие-то свои тесты. Затем если программа нормально работает на тестовых данных на сервере, то всё норм.
А, вот, как выглядит это с формальными доказательствами. Дается задание написать функцию, которая после тройного применения к списку возвращает исходный список. Задание написано на формальном языке, его невозможно как-то неправильно интерпретировать. И нет ни одного теста! Ни в задании, ни на сервере, ни самому разработчику их тоже писать не нужно. Если программа соответствует спецификации, то она на 100% корректна.
Как вы эту простую задачку покрыли бы тестами на 100%? Тестов должно было бы быть бесконечное количество.
nikitadanilov
26.01.2019 12:34Так оно и будет для однопоточных, детерминированных, нераспределенных (т.е. тривиальных) программ.
artskep
26.01.2019 22:53nikitadanilov
26.01.2019 23:32Какое отношение это имеет к доказательству корректности какой-либо конкретной программы?
artskep
26.01.2019 22:51В реальности «волшебная программа без багов» невозможна.
Товарищ Тюринг это математически доказал, кстати.
Конечно, товарищ Гедель в своей теореме о неполноте по большому счету доказал почти то же, но Тюринг все-таки как-то ближе к программистам… :-)amarao
26.01.2019 23:12Вы путаете существование программы без багов и возможность доказать, что данная программа без багов.
Программа без багов очевидно существует, просто потому, что какая-то комбинация байтов таки является таковой. А вот какая — вот тут-то и вопрос.artskep
26.01.2019 23:28Программа без багов очевидно существует, просто потому, что какая-то комбинация байтов таки является таковой. А вот какая — вот тут-то и вопрос.
Ха-Ха-ХА! Туше :-).
Но я даже могу сказать какая программа без багов существует — та, которая не написана. Нет программы — нет проблем.
Но я таки предполагал какую-то программу из реального мира, что предполагает, что она должна удовлетворять некоторому (хотя бы минимально очевидному) ТЗ.
И тут, конечно, возникают проблемы.
dim2r
26.01.2019 16:39+1Тоже занимался темой самодиагностики программ
habr.com/ru/post/342302
Пришел к выводу, что надо писать некий контейнер, в который помещаешь маленькие хотелки, которые выдают свои маленькие действия. Контейнер проверят, чтобы действия хотелок не противоречили друг другу.
lingvo
26.01.2019 19:18Помоему самая главная мысль из этой статьи заложена здесь:
Компьютеры связаны через внутреннюю сеть или шину CAN на квадрокоптере
Что такое CAN? CAN — это CAN (англ. Controller Area Network — сеть контроллеров) — стандарт промышленной сети, ориентированный на передачу коротких, изначально заданных сообщений в реальном времени. Причем CAN-контроллеры — это полностью реализованные в железе микросхемы, которые физически невозможно перепрограммировать. Т.е. вы не сможете передать что-то, что не заложено в устройство на этапе проектирования сети — например файл, вирус, или изображение. Т.е. взломать Flight Computer через тот же CAN — физически невозможно. Возможно только повлиять на его работу давая ложные данные, но он их может перепроверить и не принять.
Т.е. изолируем критическую часть системы управления от некритической каким-то примитивным железным протоколом — и можно говорить, что уже половина дела в защите от кибератак сделана.
artskep
26.01.2019 20:46Причем CAN-контроллеры — это полностью реализованные в железе микросхемы, которые физически невозможно перепрограммировать.
Я бы сказал, что это слишком сильное заявление…
artskep
Как только много лет назад я узнал о L4, и о том, что L4 формально верифицируют, я был в экстазе.
Буквально через месяц, когда я всерьез начал работу над проектом, где L4 было в качестве микроядра, я осознал, что это не сработает никогда.
Потому что можно формально верифицировать ядро. Но формально верифицировать хотелки заказчика…