что такое верификация программного обеспечения

Верификация и валидация

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

Мы решили разобраться с терминологией, чтобы придерживаться наиболее правильного толкования этих понятий. В ходе исследования, мы нашли работу В.В. Кулямина «Методы верификации программного обеспечения» [1]. В ней дается развернутое описание этих терминов, и мы приняли решение в дальнейшем опираться на определения, данные в этой работе. Приведем некоторые выдержки их этой работы, относящиеся к верификации и валидации.

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

Для дальнейшего изложения нам необходимо ввести термин «артефакт жизненного цикла ПО». Артефактами жизненного цикла ПО называются различные информационные сущности, документы и модели, создаваемые или используемые в ходе разработки и сопровождения ПО. Так, артефактами являются техническое задание, описание архитектуры, модель предметной области на каком-либо графическом языке, исходный код, пользовательская документация и т.д. Различные модели, используемые отдельными разработчиками при создании и анализе ПО, но не зафиксированные в виде доступных другим людям документов, не могут считаться артефактами.

Различие между верификацией и валидацией проиллюстрировано на рисунке 1.

Верификация отвечает на вопрос «Делаем ли мы продукт правильно?», а валидация- на вопрос «Делаем ли мы правильный продукт?»

также добавляет путаницы, поскольку афористичность этого высказывания, к сожалению, сочетается с двусмысленностью. Однако многочисленные труды его автора позволяют считать, что он подразумевал под верификацией и валидацией примерно те же понятия, которые определены выше. Указанные разночтения можно проследить и в содержании стандартов программной инженерии. Так, стандарт ISO 12207 [5] считает тестирование разновидностью валидации, но не верификации, что, по-видимому, является следствием использования неточного определения из стандартного словаря [3].

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

Источник

Верификация и валидация ПО: технологии и инструменты

Сейчас как никогда актуальна проблема обеспечения качества ПО: даже единичный отказ может привести к ликвидации компании или человеческим жертвам. Как обеспечить качество ПО и постоянно поддерживать его на требуемом уровне?

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

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

Сегодня организации вкладывают около 30% бюджета, выделяемого на ИТ, в обеспечение качества и тестирование, что неудивительно — более половины всех систем являются критически важными для бизнеса [1]. При этом компаниям и организациям необходимо максимально гибко реагировать на изменения и внедрять формализованные процессы и методы контролируемого выпуска безопасного ПО. Активно внедряются механизмы автоматического обновления ПО по Сети, методы DevOps и «непрерывная инженерия» (continuous software engineering) [2], что повышает потребность в процессах непрерывной верификации и валидации, требующих намного более тщательного, чем еще совсем недавно, выполнения процедур испытания на общую работоспособность.

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

Выбор методов верификации и валидации ПО зависит от модели разработки (V-модель, каскадная, спиральная и т. д.) и стандарта (ISO/IEC 25000 SQUARE, ISO/IEC 12207:2017) (рис. 1).

Рис. 1. Стандарты обеспечения качества процесса разработки ПО и конечного продукта

За качество собственно процесса разработки ПО отвечают стандарт ISO/МЭК 12207, регламентирующий процессы верификации и валидации, а также V-модель, в рамках которой каждой задаче разработки ставится в соответствие процесс тестирования. Например, модульный тест проверяет соответствие исходного кода низкоуровневой архитектуре, интеграционные тесты проверяют совместимость (интеграцию) ранее протестированных компонентов, системные тесты позволяют выяснить, соответствует ли полностью интегрированный продукт спецификациям, а приемочные тесты — отвечает ли продукт ожиданиям пользователя.

В стандартах серии ISO 25000, относящихся к качеству программного продукта, выделены следующие характеристики ПО:

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

Рис. 2. Инструменты для проверки основных характеристик качества ПО

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

Технологии и инструменты

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

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

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

Инструментов тестирования так же много, как и языков программирования. В табл. 1 приведены основные средства тестирования для первой десятки наиболее популярных языков программирования (согласно рейтингу Tiobe).

Инструменты контроля сопровож-даемости. Позволяют анализировать исходный код и проверять его на соответствие правилам модульности, читаемости и др. (табл. 2).

Инструменты контроля удобства использования. Применяются для оценки программного продукта в процессе работы с ним реальных пользователей. В то же время такие инструменты позволяют проводить валидацию пользовательского интерфейса без участия самих пользователей (табл. 3).

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

Средства проверки производительности. Позволяют выяснить, насколько быстро система работает под нагрузкой (табл. 5). Эти средства не предназначены для поиска дефектов в приложении, а применяются для оценки измеримых характеристик: времени отклика, пропускной способности и т. д.

Средства непрерывной верификации и валидации. Принцип непрерывного обеспечения качества предполагает тесную интеграцию процессов верификации и валидации на всех этапах разработки. Типичный пример — разработка с ориентацией на тестирование: плановые показатели качества задаются еще до разработки ПО. С учетом преимуществ непрерывной интеграции, одной из основ DevOps, все большее значение придается инструментам, помогающим не только автоматизировать верификацию и валидацию, но и интегрировать эти процессы в цикл разработки. Перечисленные в табл. 6 инструменты позволяют проверять характеристики качества в рамках сред непрерывной интеграции Jenkins, Travis CI, Bamboo, GoCD, Ansible и т. п. Требуется встроить валидацию и верификацию в жизненный цикл ПО, обеспечив автоматическое, прозрачное для разработчиков выполнение соответствующих процессов. Представленные в табл. 6 инструменты проверяют несколько характеристик качества и позволяют получить данные для глобальной оценки и визуализации. В рамках процессов непрерывной верификации и валидации также могут применяться инструменты модульного тестирования, фиксации и замены и статического анализа.

Для управления действиями, выполняемыми при помощи всех перечисленных видов инструментов, и контроля над процессом верификации и валидации в целом, применяются средства управления тестовыми случаями: Test Link, Test Rail, Microfocus Quality Center, VSTS, IBM Rational Quality Manager, XStudio и др.

Перспективы

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

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

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

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

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

Аристотель говорил: «Совершенство — это не действие, а привычка». Широкий выбор инструментов — это важно, но главное — создание культуры обеспечения качества ПО и приобретение соответствующих навыков.

1. Capgemini. MicroFocus, and Sogeti. World quality report. 2018. [Online]. URL: https:// www.capgemini.com/service/world-quality-report-2018-19/ (дата обращения: 16.05.2019).

2. B. Fitzgerald, K. Stol. Continuous software engineering: A roadmap and agenda // J. Syst. Softw.— 2017 (Jan). — Vol. 123. — P. 176–189.

Моисес Родригес (mrodriguez@aqclab.es) — доцент, Марио Пьяттини (mario.piattini@uclm.es) — профессор, Университет Кастилии-Ла-Манчи (Испания); Кристоф Эберт (christof.ebert@vector.com) — директор, Vector Consulting Services.

Moises Rodriguez, Mario Piattini, Christof Ebert, Software Verification and Validation Technologies and Tools. IEEE Software, March/April 2019, IEEE Computer Society. All rights reserved. Reprinted with permission.

Поделитесь материалом с коллегами и друзьями

Источник

Микроядро 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 использует для каждой новой системы только существующие доказательства, включая доказательства, сгенерированные инструментами. Таким образом, общие усилия по доказательству для системы, которая соответствует этому подходу, сводятся к человеко-неделям, а не годам, а тестирование сводится только к проверке допущений.

Источник