Глава 2. Описание процесса моделирования и верификации механизма управления доступом операционной системы

Рассматриваемый процесс состоит из нескольких этапов, которые далее будут описываться последовательно. Изложение в целом следует логике регламентирующего документа ГОСТ Р ИСО/МЭК 15408-3 в той части, где описывается класс доверия ADV «Разработка». При этом сначала рассматриваются более абстрактные представления модели политики безопасности управления доступом, затем более детальное представление модели и в конечном счете рассматривается задача верификации механизма управления доступом в ядре ОС, где мы имеем дело уже с конкретной программной системой, реализованной на языке программирования Си.

Напомним читателю требования класса доверия «Разработка», в котором в соответствии с ГОСТ Р ИСО/МЭК 15408-3 [6] для функций безопасности объекта оценки (ФБО) и функциональных требований безопасности (ФТБ) указывается, что класс «Разработка» содержит шесть семейств доверия для структурирования и представления ФБО на различных уровнях детализации. Эти семейства включают в себя:

Далее в ГОСТ Р ИСО/МЭК 15408-3 отмечается, что при документировании функциональных возможностей безопасности ОО необходимо продемонстрировать два основных свойства. Первое свойство заключается в том, что определенная функциональная возможность выполняется правильно, согласно спецификации. Второе свойство, которое несколько сложнее продемонстрировать, заключается в том, что невозможно использовать ОО так, чтобы это привело к искажению или обходу функциональных возможностей безопасности. Два этих свойства требуют применения различных подходов к их анализу.

В рамках книги мы в первую очередь концентрируемся на исследовании первого свойства — спецификации функциональных возможностей безопасности, поэтому рассматриваем семейства «Функциональная спецификация» (ADV_FSP), «Проект ОО» (ADV_TDS) и «Моделирование политики безопасности» (ADV_SPM).

Изложение начинается с проблем построения и верификации модели политики безопасности управления доступом, затем рассматривается вопрос построения функциональной спецификации ОО и вопрос ее соответствия модели политики безопасности управления доступом.

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

В [6] отмечается, что в функциональной спецификации ОО не описывается, каким образом реализуются функции безопасности, этот вопрос с той или иной степенью детальности рассматривается в семействе «Проект ОО» (ADV_TDS). В рамках ADV_TDS особенно важно исследовать структуру реализации механизма управления доступом. В связи с этим в главе 6 описываются модуль безопасности (Linux Security Module — LSM) — ключевой компонент механизма управления доступом ОССН и методы его формальной спецификации и верификации.

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

2.1. Этап I. Формализация модели политики безопасности управления доступом и ее верификация

В нашем случае ОО [4] служит механизм управления доступом ОС1, являющейся важнейшей частью СЗИ ОССН. Правила ограничения доступа к тем или иным информационным ресурсам составляют политику безопасности управления доступом. Ответственность за полную и корректную реализацию этих требований возлагается на механизмы, встроенные в ядро ОС. Можно считать, что разработка некоторого документа верхнего уровня, который строго и полно описывает требования к механизму управления доступом, это один из первых этапов создания (или сборки) системы в рамках классического подхода к проектированию программ «сверху-вниз», о полезности которого было много написано еще 70-80-е годы 20-го века. Заметим, как теоретики, так и практики, приверженцы этого подхода уже в те годы отмечали, что собственно проектирование «сверху-вниз» не дает гарантий построения «правильных» программ. Такие «гарантии», точнее, свидетельства, демонстрирующие или даже доказывающие «правильность» или «корректность» получаемого программного решения, может дать только тщательная проверка, верификация всех проектных и рабочих документов (артефактов) и проверка их взаимной согласованности.

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

По мере роста объема документации ОО, в частности требований к механизму управления доступом, степень уверенности в том, что в нем нет пропусков и несогласованностей, снижается. Если размер документа, описывающего требования, превышает размер 5-10 страниц, то, если не провести тщательную проверку, можно гарантировать, что ошибки в нем есть. В нашем случае такой документ включает в себя около 300 страниц математического текста с пояснениями на русском языке. Единственной возможностью существенно повысить согласованность (консистентность) документа является представление его содержания в некотором виде, которое можно проанализировать при помощи современных средств верификации. Таким представлением может быть формальная модель, изложенная на подходящем языке формальных спецификаций (далее будем говорить «на формальном языке»). При этом от «формальной» спецификации мы ожидаем, что одновременно она написана на формальном языке, семантика которого строго и однозначно определена, и имеются программные инструменты, которые позволяют анализировать и верифицировать спецификации на таком формальном языке.

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

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

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

2.2. Этап II. Разработка спецификации системных вызовов ОС и доказательство ее соответствия с формальной моделью политики безопасности

На втором этапе необходимо связать требования к механизму управления доступом (модель политики безопасности управления доступом) с функциональной спецификацией ОО (рис. 2.1). Это требуется для того, чтобы решить еще одну задачу, предусмотренную требованиями ГОСТ Р ИСО/МЭК 15408, а именно, доказательство соответствия между формальной функциональной спецификацией и формальной моделью политики безопасности (доказательство «соответствия между моделью политики безопасности и функциональной спецификацией (ADV_SPM «Моделирование политики безопасности»)» [6]).

В нашем случае функциональной спецификацией ОО является интерфейс API (Application Program Interface) операционной системы, т. е. интерфейс системных вызовов.

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

fig21 s1 Формализация и верификация модели политики безопасности s2 Разработка спецификации системных вызовов ОС и доказательство её соответствия с формальной моделью политики безопасности s1->s2 a1 Event-B спецификация МРОСЛ ДП-модели s1->a1 a2 ФСП на Event-B s2->a2 a1->a2

Рис. 2.1. Первые два этапа верификации механизма управления доступом ОС

Сделаем три замечания:

  • использование второго языка спецификаций и перевод с первого на второй имеют смысл, если спецификации на втором языке будут использоваться далее в процессе верификации ОО;
  • спецификация системных вызовов может описывать не полную функциональность ОС, а лишь те требования к API, которые важны в контексте управления доступом, это так называемые частичные спецификации;
  • после того как построена формальная функциональная спецификация API ОС, должно быть продемонстрировано соответствие данной спецификации требованиям модели политики безопасности. Если соответствие доказано, то можно гарантировать, что выполнение требований функциональной спецификации ОО гарантирует выполнение требований модели политики безопасности управления доступом. При этом нужно принять во внимание, что структура формальной модели политики безопасности управления доступом (набор типов данных и операций) отличается от структуры API ОС, поскольку системные вызовы оперируют с конкретными файлами, идентификаторами процессов и другими сущностями реальной ОС, а формальная модель политики безопасности оперирует с абстрактными информационными ресурсами, субъектами и объектами, между которыми определены правила управления доступом и его администрирования. Для формального анализа соответствия две спецификации нужно привести к некоторому «общему знаменателю». Эта задача не простая, но решаемая.

2.3. Этапы III и IV. Исследование механизма управления доступом ОС

После того как выполнены работы первого и второго этапа, мы имеем формальное, математическое доказательство того, что, во-первых, модель политики безопасности управления доступом консистентна и, во-вторых, функциональные требования к ОО согласованы с требованиями к политике безопасности управления доступом. И то, и другое необходимо для обеспечения соответствия уровням доверия ОУД6 и ОУД7. Однако пока не был рассмотрен вопрос о том, отвечает ли реализация ОО тем требованиям, которые зафиксированы в спецификациях системных вызовов и/или в модели политики безопасности управления доступом.

Получить ответ на этот вопрос существенно сложнее, чем решить проблемы на первых двух этапах, поскольку размер и сложность реализации системных вызовов несоизмеримо больше в сравнении с моделями и их спецификациями, которые мы рассматривали выше. Современный уровень технологий позволяет математически строго верифицировать программы из класса ОС размером 10–20 тысяч строк на языке типа Си. Ядро ОС Linux сейчас содержит около 20 млн строк на Си. По этой причине для обеспечения уверенности в корректности реализации механизма управления доступом в ядре ОС Linux приходится искать некоторое компромиссное решение (что, в действительности, не противоречит требованиям стандартов).

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

Общая схема механизма управления доступом, которая рассматривается в данном случае, была предложена в проекте Security-Enhanced Linux (SELinux) [16], предполагающем встраивание специальных дополнительных точек контроля доступа ко всем информационным ресурсам, контролируемым ядром ОС. Эти точки не выполняют собственно контроль, а лишь играют роль «перехватчиков», они обращаются к специальному модулю ядра Linux Security Modules (LSM), где, собственно, и выполняется проверка корректности доступа. В случае некорректного доступа LSM выдает запрет на доступ, что обеспечивает безопасность доступа к защищаемым ресурсам. Логика проверок, которые выполняются модулем LSM, должна полностью отвечать конкретной политике безопасности управления доступом, установленной для конкретного механизма управления доступом.

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

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

fig22 s1 Формализация и верификация модели политики безопасности s2 Разработка спецификации системных вызовов ОС и доказательство её соответствия с формальной моделью политики безопасности s1->s2 a1 Event-B спецификация МРОСЛ ДП-модели s1->a1 s3 Разработка и верификация спецификации API LSM s2->s3 a2 ФСП на Event-B s2->a2 s4 Разработка низкоуровневой спецификаций API LSM и верификация реализации LSM s3->s4 a3 Event-B спецификация API LSM s3->a3 a4 ACSL спецификация API LSM s4->a4 a1->a2 a1->a3 a2->a3 a3->a4

Рис. 2.2. Процесс верификации механизма управления доступом ОС. Этапы I–IV

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

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

Из этого следует вывод, что спецификацию API LSM нужно строить на основе понимания требований к этому модулю. «Понимание» — объект не формальный. По этой причине на рис. 2.2 связь между этапом II и этапом III обозначена при помощи пунктирной линии. В силу неформальности перехода от второго этапа к третьему без дополнительных исследований мы не можем утверждать, что из выполнения требований спецификации к каждой из функций из API LSM будет следовать выполнение общих требований по защите информации, инвариантов безопасности (что мы доказывали при исследовании модели политики управления доступом).

Для решения это проблемы к задаче построения формальной спецификации API LSM добавляется задача ее верификации, т. е. доказательства ее консистентности и доказательства сохранения инвариантов безопасности при выполнении произвольных обращений к API LSM. Такого рода доказательство можно выполнить при помощи тех же инструментов, что использовались на первом и втором этапах, но это означает, что спецификацию API LSM придется писать на языке Event-B. Собственно в этом и состоит содержание III этапа: разработка спецификаций API LSM на Event-B и ее верификация.

Содержание IV этапа — разработка спецификации API LSM на уровне языка программирования и верификация уже не модели, а реализации модуля LSM. Спецификация в этом случае уже разрабатывается на языке спецификаций ACSL, специально предназначенного для описания требований к интерфейсам программ, реализованных на языке Си. Для верификации реализации модуля LSM, естественно, также нужно использовать другие инструменты, которые предназначены для верификации Си-программ.

Переход от спецификаций API LSM на Event-B к спецификациям на ACSL трудно сделать совсем формальным, однако здесь риск получить неадекватную спецификацию невелик, поэтому на рис. 2.2 связь между III и IV этапами обозначена не пунктирной, а сплошной линией.

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

fig23 s1 Формализация и верификация модели политики безопасности s2 Разработка спецификации системных вызовов ОС и доказательство её соответствия с формальной моделью политики безопасности s1->s2 a1 Event-B спецификация МРОСЛ ДП-модели s1->a1 s3 Разработка и верификация спецификации API LSM s2->s3 a2 ФСП на Event-B s2->a2 s4 Разработка низкоуровневой спецификаций API LSM и верификация реализации LSM s3->s4 a3 Event-B спецификация API LSM s3->a3 s5 Мониторинг API LSM s4->s5 a4 ACSL спецификация API LSM s4->a4 a5 Анализ трассы на уровне API LSM s5->a5 a1->a2 a1->a3 a2->a3 a3->a4 a4->a5

Рис. 2.3. Схема процесса верификации механизма управления доступом ОС. Вариант 1

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

В связи с этим приходится выбирать другой вариант организации сквозной проверки соответствия поведения ОО требованиям модели политики безопасности управления доступом. Эта схема представлена на рис. 2.4. В этой схеме трассы наблюдаются на уровне системных вызовов, а не на уровне модуля LSM. Критерий корректности трассы — выполнение требований функциональной спецификации системных вызовов (ФСП). В силу результата второго этапа процесса верификации выполнение требований ФСП гарантирует выполнение требований модели политик безопасности управления доступом в целом. Тем самым, если хотя бы одну трассу не удается сопоставить с ФСП, нужно делать вывод о том, что требования модели политики безопасности нарушаются. Если все трассы удается сопоставить с ФСП, то мы получаем набор объективных свидетельств о выполнении требований политики безопасности.

fig24 s1 Формализация и верификация модели политики безопасности s2 Разработка спецификации системных вызовов ОС и доказательство её соответствия с формальной моделью политики безопасности s1->s2 a1 Event-B спецификация МРОСЛ ДП-модели s1->a1 s3 Разработка и верификация спецификации API LSM s2->s3 a2 ФСП на Event-B s2->a2 s4 Разработка низкоуровневой спецификаций API LSM и верификация реализации LSM s3->s4 a3 Event-B спецификация API LSM s3->a3 s5 Мониторинг системных вызовов ОС s4->s5 a4 ACSL спецификация API LSM s4->a4 a5 Анализ трассы на уровне API ОС s5->a5 a1->a2 a1->a3 a2->a3 a2->a5 a3->a4 a4->a5

Рис. 2.4. Схема процесса верификации механизма управления доступом ОС. Вариант 2

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

В рамках исследований ОССН Astra Linux Special Edition был выбран последний вариант схемы процесса верификации механизма управления доступом, представленный на рис. 2.4.

2.4. Замечание об используемой терминологии

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

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

В профессиональной речи часто термин «модель» понимается как синоним термина «спецификация», хотя буквально «спецификация» это лишь точное, детальное описание чего-либо, в частности описание модели или описание реальной программной сущности или программного процесса. Понятно, что описание программной сущности (например, некоторой функции на языке Си), это не то же самое, что сама сущность. Однако в случае рассмотрения спецификаций на Event-B «модель» и «спецификация» (модели) может значить одно и то же.

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

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

Формальная модель (или формальная спецификация) — модель, представленная в формальной машиночитаемой нотации, например в Event-B. Термин «формальный» здесь означает, что для такого представления моделей могут быть разработаны или уже разработаны инструменты, которые анализируют такие модели, проводят их верификацию, а иногда и трансформацию в программы на языках программирования.

Функциональная спецификация ОО, в соответствии с определением, приведенном в стандарте ГОСТ Р ИСО/МЭК 15408, — это «полная полуформальная функциональная спецификация с дополнительной формальной спецификацией». В нашем подходе полуформальные спецификации мы используем как некоторый исходный артефакт, на основе которого строится система формальных спецификаций. Формализация спецификаций нужна для того, чтобы можно было использовать те или иные программные инструменты для анализа/верификации самих спецификаций/моделей или для анализа соответствия между спецификациями/моделями различного уровня детальности или между спецификациями (требований) и программных реализаций.

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

  1. Как уже отмечалось, описывается конкретный опыт проведения работ по подготовке к сертификации ОССН Astra Linux Special Edition, поэтому, хотя по тексту может быть написано просто «операционная система», как правило, имеется в виду архитектура ОС Linux, а иногда и специфические решения, которые используются именно в ОССН. Вместе с тем общая схема процесса верификации достаточно мало зависит от специфики ОС.↩︎