Ключевые моменты лекции 3 /
Модель мандатного управления доступом. Модель Биба
Модель Биба часто и не без основания считают «зеркальной» для модели Белла и Лападула. В самом деле, она также построена на уровнях, но уже на уровнях целостности, и сформулированные для нее правила – это No Write Up и No Read Down. Однако, тут могут возникнуть сложности с интерпретацией.

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

В самом бытовом понимании, целостность либо есть, либо нет: всего два уровня. Но целостность может также описываться в ином ключе: например, степень повреждения данных, если речь идет о необходимости восстановлении объекта. Или же целостность может пониматься как степень достоверности объекта. Иногда целостность – это комплексное свойство зоны на производстве и приписанного к ней оборудования и ПО, в зависимости от нашей способности контролировать эту зону.
В общем, вспоминаем, как в первой лекции мы определяли качественные -ilities и формулируем требования к целостности, исходя из нашего контекста и целей безопасности. Часто модель Биба и ее правила становятся применимы as is или с модификацией.
Например, для достоверности очень неплохо работают правила модели Биба в оригинальном виде: получение информации из недостоверного источника (то есть чтение снизу) недопустимо для субъекта, работающего на более высоком уровне, так как он может записать эту информацию в более достоверный.
А вот если мы рассматриваем поврежденный объект, и у нас есть несколько его версий, то версия с наименьшими повреждениями находится на верхнем уровне, и мы в нее пишем для восстановления данных. А более поврежденные версии рассматриваем в качестве источника неповрежденных фрагментов, то есть читать можем откуда угодно. Такая модифицированная модель Биба получила название Ring Policy (см.слайды).
Есть интерпретация целостности в виде доверия к субъекту, например для получения определенного уровня доверия в сети доверия (Web of Trust) нужно получить «подтверждения личности» от других субъектов не ниже этого уровня. Если субъект получает и затем предъявляет подтверждение личности от субъекта с более низким уровнем, то его уровень целостности (доверия) автоматически снижается. Такая модель, в которой «чтение снизу» для субъекта не запрещено, но приводит к понижению его уровня, называется Low Watermark Policy.

Ключевые моменты лекции 3 /
Изъяны моделей мандатного управления доступом

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

Ключевые моменты лекции 3 /
Модель мандатного управления доступом. Модель Кларка-Вилсона

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

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

Ключевые моменты лекции 3 /
Модели мандатного управления доступом. Модель Китайской стены

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

Ключевые моменты лекции 3 /
Архитектурный подход MILS. Что такое MILS

MILS основан на теории архитектурного подхода к безопасности и расширяет ее, предлагая методы и инструменты для создания высоконадежных архитектур для безопасного обмена информацией и надежных систем. MILS упрощенно характеризуется как использование т.н. ядра разделения для запуска приложений, принадлежащих к разным областям безопасности или имеющих разные уровни требований безопасности (критичность, целостность и т.п.) на одном компьютере. Идея MILS заключается в разработке интуитивно понятной логической архитектуры для достижения цели (целей) безопасности, а затем в создании реализации, структурированной для точного отражения этой архитектуры.
Название MILS было аббревиатурой, обозначающей «множество независимых уровней безопасности/безопасности». Сегодня оно используется как имя собственное для подхода, который начинается с разделения проектируемой системы на изолированные разделы или домены безопасности. Хотя идея такого разделения впервые появилась в 1981 году в статье J.Rushby, должная технологическая реализация оказалась возможна только в начале 2000х. Именно в это время MILS возродился как концепция, частично из мандатных моделей и работ Rushby, частично из архитектурных требований к ПО критического назначения: например, применяемого в авионике.
С точки зрения ISO 42010, подход MILS, конкретизированный для системы, вероятно является одним из архитектурных представлений (architectural view) системы. Он используется при определении архитектуры системы и в дальнейшем в процессе определения проекта.

Довольно свежее и подробное описание архитектурного подхода MILS представлено в документе, выпущенном IIC в 2020 “MILS Architectural Approach Supporting Trustworthiness of the IIoT Solutions”.

Ключевые моменты лекции 3 /
Архитектурный подход MILS. Архитектура политики

Базовое понятие для MILS – так называемая архитектура политики. Мы исключили отношение порядка, которое является определяющим для многих мандатных моделей, и оставили неупорядоченное множество доменов. На этом множестве доменов вводится топология возможного взаимодействия между доменами. Она выглядит как направленный граф (узлы – домены, ребра – направления потоков информации). Этот граф еще не политика безопасности, а архитектура, к которой политика применяется, разрешая или запрещая потоки информации.
По аналогии можно сравнить архитектуру политики с дорожной инфраструктурой. Дорога, односторонняя или двусторонняя, с разными типами покрытия, разным количеством полос движения, наличием или отсутствием разделительной полосы и отбойника, сама по себе позволяет отрегулировать движение транспорта: это архитектура. На дороге дополнительно используются знаки и применяются ПДД для дополнительного регулирования движения: это политика.

Ключевые моменты лекции 3 /
Архитектурный подход MILS. Требования к реализации

Существенным для определения системы как MILS системы является не только использование комбинации архитектуры и политики как формальной модели, основанной на моделях безопасности, но и должная реализация этой модели на основе подходящих технологий. Реализация должна исключать возможность непредусмотренного взаимодействия доменов, в том числе на уровне аппаратных средств. В том числе поэтому применяются требования к CPU, MMU, IOMMU.
В основе разделения доменов лежит так называемое ядро разделения (Separation Kernel). Ядро разделения – это механизм, обеспечивающий как изоляцию, так и управление информационными потоками.

Задача ядра разделения – создать среду, которая неотличима от среды, предоставляемой физически распределенной системой.

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

Ключевые моменты лекции 3 /
Архитектурный подход MILS. Функции ядра разделения

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

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

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

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

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

Слайды к третьей лекции и место для вашей обратной связи

Всем доброе! Нарисовала вам картинок и жду на лекции в 10 утра, офлайн или в тимз.

Хорошая новость - завтра последняя лекция как обычно, в 11

Конспект лекции 4 - поехали

Ключевые моменты лекции 4 /
Assurance / Гарантии безопасности

Assurance, если посмотреть в ISO 15026 или ГОСТ 15026, это «основание для утверждения, что требование выполнено или будет выполнено». Это основание может быть получено различными методами, обычно говорят о методике assurance. При этом часто ссылаются на следующие понятия:
Claim (переводится в ГОСТ как «претензия») – утверждение типа "истина/ложь" о выполнении ограничений на значения однозначно определенных свойств (называемых связанными с претензией свойствами), а также ограничений на неопределенность значений свойств в пределах этих ограничений в случае применимости претензии при указанных условиях.
Для нас эти свойства, к примеру, это наши цели безопасности и предположения безопасности. Вспоминаем стрелочку между квадратиками Security Objectives и Assurance на схеме анализа из первой лекции.
Assurance Case (переводится как, о ужас, «гарантийный случай») - обоснованный проверяемый артефакт, подтверждающий, что удовлетворяется claim верхнего уровня (или совокупность claims), и включающий систематическую аргументацию и ее явные предположения. То есть это как теорема с доказательством и леммами.
Еще пара определений. Часто говорят о compliance и conformance. Compliance – это обязательное соответствие некоторому набору требований (например, регулятора), достигаемое посредством получения assurance. Conformance – это добровольное соответствие, то есть использование требований/проверка на соответствие по желанию (просто иногда удобно использовать готовый набор требований).

Ключевые моменты лекции 4 /
Валидация и верификация
(вы их больше не перепутаете)

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

Если говорить еще проще, верификация задается вопросом, строим ли мы систему правильно, а валидация – строим ли мы правильную систему.

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

Я когда-то давно писала статью на securelist, в ней можно найти больше букв на эту тему. Вот она на русском, вот на английском.

Ключевые моменты лекции 4 /
Методы верификации

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

Ключевые моменты лекции 4 /
Формальная верификация

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

Тем не менее, перечислим известные и применяемые методы формальной верификации. Во-первых, это model checking (проверка на модели) - метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить, удовлетворяет ли заданная модель системы формальным спецификациям.

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

Метод дедуктивной верификации реализует проверку правильности программы относительно ее спецификации, записанной на формальном языке спецификаций. Условия корректности программы генерируются автоматически по формулам логики и спецификации программы путем применения системы логических правил. Доказательство условий корректности проводится с помощью некоторой системы автоматического доказательства. Метод ограничен ситуациями математической неразрешимости.
Кроме этих двух методов, множество авторов упоминают множество других методов. Некоторые из них действительно существенно отличаются (например, вовлекают динамические методы), другие представляют собой комбинации или улучшения известных. Мы рассматривали также методы уточнения и генерации кода (refinement and code generation) и метод абстрактной интерпретации (abstract interpretation) описываемый в неплохой статье парой европейских ученых.
Источники
Книга Ю.Г.Карпов «Model Checking»
Слайды к лекциям на ВМК МГУ, содержат в т.ч. примеры из книжки Ю.Г.Карпова и компиляцию полезной информации по формальным методам
Слайды к курсу лекций в СПб Политехе
Методичка к курсу лекций в МГУ от автора из ИСП РАН
Материалы Института системного программирования РАН (ИСП РАН)

Ключевые моменты лекции 4 /
Гарантии безопасности в MILS

Сама идея развития MILS, начиная где-то с 2010, включала идею поставки компонентов разными разработчиками с готовыми assurance cases на типовые для этих компонентов цели безопасности. Если при совмещении компонентов не возникает новых свойств, влияющих на нарушение гарантий, то такая система автоматически получает унаследованные от компонентов гарантии безопасности.
Для этого ввели три специальных свойства:
Компонуемость (composability) — условие, при котором компоненты могут быть составлены без ущерба для их индивидуальных свойств. Это важнейшее свойство, предоставляемое ядром разделения (или платформой MILS). Компоненты А и В могут выполняться изолированно, и ни один из них не влияет на работу другого.
Композиционность (compositionality) — условие, при котором компоненты могут быть составлены таким образом, чтобы создавать новые свойства композиции из их индивидуальных свойств. Композиционность представляет собой способность соединять два компонента таким образом, чтобы их поведение конструктивно комбинировалось для создания нового поведения.
Аддитивность (или аддитивная композиционность) (additivity) — особый вид композиционности, при котором «дополнение» отдельных, но различных свойств компонентов сохраняется в композиции наряду с их общими свойствами. Эта концепция необходима для обеспечения составления платформы MILS из основных компонентов MILS.

Ключевые моменты лекции 4 /
Верификация MILS системы

Проверка системы MILS состоит из четырех частей:
обоснование взаимного невлияния доменов (non-interference assurance),
обоснование локальных политик (local policies assurance),
обоснование безопасности архитектуры политики (policy architecture assurance),
обоснование свойства композиционности (compositionality)

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

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