Валидация и верификация требований к системе
Очень часто путают два понятия валидация и верификация. Кроме того, часто путают валидацию требований к системе с валидацией самой системы. Я предлагаю разобраться в этом вопросе.
В статье «Моделирование объекта как целого и как композиции» я рассмотрел два подхода к моделированию объекта: как целого и как конструкции. В текущей статье нам это деление понадобится.
Пусть у нас есть проектируемый функциональный объект. Пусть этот объект рассматривается нами как часть конструкции другого функционального Объекта. Пусть есть описание конструкции Объекта, такое, что в нем присутствует описание объекта. В таком описании объект имеет описание как целого, то есть, описаны его интерфейсы взаимодействия с другими объектами в рамках конструкции Объекта. Пусть дано описание объекта как конструкции. Пусть есть информационный объект, содержащий требования к оформлению описания объекта как конструкции. Пусть есть свод знаний, который содержит правила вывода, на основании которых из описания объекта как целого получается описание объекта как конструкции. Свод знаний – это то, чему учат конструкторов в институтах – много, очень много знаний. Они позволяют на основе знанию об объекте спроектировать его конструкцию.
Итак, можно начинать. Мы можем утверждать, что если правильно описан объект как целое, если свод знаний верен, и если правила вывода были соблюдены, то полученное описание конструкции объекта, будет верным. То есть, на основе этого описания будет построен функциональный объект, соответствующий реальным условиям эксплуатации. Какие могут возникнуть риски:
1. Использование неправильных знаний об Объекте. Модель Объекта в головах у людей может не соответствовать реальности. Не знали реальной опасности землетрясений, например. Соответственно, могут быть неправильно сформулированы требования к объекту.
2. Неполная запись знаний об Объекте – что-то пропущено, сделаны ошибки. Например, знали о ветрах, но забыли упомянуть. Это может привести к недостаточно полному описанию требований к объекту.
3. Неверный свод знаний. Нас учили приоритету массы над остальными параметрами, а оказалось, что надо было наращивать скорость.
4. Неправильное применение правил вывода к описанию объекта. Логические ошибки, что-то пропущено в требованиях к конструкции объекта, нарушена трассировка требований.
5. Неполная запись полученных выводов о конструкции системы. Все учли, все рассчитали, но забыли написать.
6. Созданная система не соответствует описанию.
Понятно, что все артефакты проекта появляются, как правило, в завершенном своем виде только к концу проекта и то не всегда. Но, если предположить, что разработка водопадная, то риски такие, как я описал. Проверка каждого риска – это определенная операция, которой можно дать название. Если кому интересно, можно попытаться придумать и озвучить эти термины.
Что такое верификация? По-русски, верификация – это проверка на соответствие правилам. Правила оформляются в виде документа. То есть, должен быть документ с требованиями к документации. Если документация соответствует требованиям этого документа, то она прошла верификацию.
Что есть валидация? По-русски валидация – это проверка правильности выводов. То есть, должен быть свод знаний, в котором описано, как получить описание конструкции на основе данных об объекте. Проверка правильности применения этих выводов – есть валидация. Валидация — это в том числе проверка описания на непротиворечивость, полноту и понятность.
Часто валидацию требований путают с валидацией продукта, построенного на основе этих требований. Так делать не стоит.
Верификация программы
54. Верификация программы
Доказательство того, что поведение программы соответствует спецификации на эту программу
Полезное
Смотреть что такое «Верификация программы» в других словарях:
верификация программы — верификация Доказательство того, что поведение программы соответствует спецификации на эту программу. [ГОСТ 19781 90] Тематики обеспеч. систем обраб. информ. программное Синонимы верификация EN program verification … Справочник технического переводчика
верификация — 02.02.03 верификация (символ) [verification]: Техническая процедура проверки, посредством которой производят измерения символа для определения его соответствия требованиям спецификации к этому символу. Источник … Словарь-справочник терминов нормативно-технической документации
ВЕРИФИКАЦИЯ — (от лат. verificatio доказательство, подтверждение) установление истинности или эмпирической осмысленности научных утверждений. Этот термин получил широкое распространение в связи с неопозитивистской программой эмпирического обоснования науки. С… … Философская энциклопедия
верификация (доказательство правильности) программы — — [Е.С.Алексеев, А.А.Мячев. Англо русский толковый словарь по системотехнике ЭВМ. Москва 1993] Тематики информационные технологии в целом EN program verification … Справочник технического переводчика
верификация кода — Проверка соответствия кода [программы] для ЭВМ установленным техническим требованиям. [А.С.Гольдберг. Англо русский энергетический словарь. 2006 г.] Тематики энергетика в целом EN code audit … Справочник технического переводчика
верификация программ — 1. Любой метод, который убеждает в том, что программа будет выполнять именно то, что от нее ожидается. 2. Доказательство того, что поведение программы соответствует спецификации на эту программу (ДСТУ 2873). [Домарев В.В. Безопасность… … Справочник технического переводчика
Верификация — Позитивизм … Википедия
Формальная верификация — формальное доказательство соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства. Из за рутинности даже простой формальной верификации и… … Википедия
Switch-технология — технология разработки систем логического управления на базе конечных автоматов, охватывающая процесс спецификации, проектирования, реализации, отладки, верификации, документирования и сопровождения. Предложена А. А. Шалыто в 1991 году [1].… … Википедия
ГОСТ 19781-90: Обеспечение систем обработки информации программное. Термины и определения — Терминология ГОСТ 19781 90: Обеспечение систем обработки информации программное. Термины и определения оригинал документа: 9. Абсолютная программа Non relocatable program Программа на машинном языке, выполнение которой зависит от ее… … Словарь-справочник терминов нормативно-технической документации
Микроядро seL4. Формальная верификация программ в реальном мире
Научная статья опубликована в журнале Communications of the ACM, октябрь 2018, том 61, номер 10, стр. 68−77, doi: 10.1145/3230627
В феврале 2017 года со взлётной площадки «Боинга» в Аризоне поднялся вертолёт с обычным заданием: облёт ближайших холмов. Он летел полностью автономно. Согласно требованиям по технике безопасности Федерального управления авиации США, пилот не прикасался к органам управления. Это был не первый автономный полёт AH-6, которого в компании называют Беспилотной Птичкой (Unmanned Little Bird, ULB). Он так летает уже много лет. Однако на этот раз посреди полёта вертолёт подвергся кибератаке. Бортовой компьютер атаковало вредоносное программное обеспечение видеокамеры, а также вирус, доставленный через заражённую флэшку, которую вставили во время техобслуживания. Атака поставила под угрозу некоторые подсистемы, но не смогла повлиять на безопасную эксплуатацию воздушного судна.
Ключевые идеи
В этой статье объясняются эти изменения и технология, которая сделала их возможными. Речь идёт о технологии, разработанной в рамках программы 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 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 использует для каждой новой системы только существующие доказательства, включая доказательства, сгенерированные инструментами. Таким образом, общие усилия по доказательству для системы, которая соответствует этому подходу, сводятся к человеко-неделям, а не годам, а тестирование сводится только к проверке допущений.