Всем привет! Сегодня я хочу поделиться с вами опытом создания формальных моделей СЗИ и рассказать 5 основных шагов с помощью которых можно построить формальную модель СЗИ и доказать ее безопасность.
С 2020 года, после выхода приказа ФСТЭК России № 76 от 02.06.2020 «Об утверждении Требований по безопасности информации, устанавливающих уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий» разработчики ПО в области информационной безопасности для прохождения сертификации во ФСТЭК обязаны формально моделировать и доказывать безопасность своих СЗИ.
Как это сделать, если у Вас нет в арсенале обученных специалистов, компетентных в области формальной верификации или нет времени разбираться в том, как работают заточенные под это дело специальные программные решения (например, известный Event-B)?
Но, например, Вы хорошо учились на первом курсе и знаете введение в мат анализ: теорию множеств.
По большому счету любое ПО - это дискретная система, поэтому проще всего ее описывать, пользуясь дискретным представлением.
Здесь удобнее и проще всего будет использовать теорию множеств, которая по ее говорящему названию стоит на определении элементов множеств, задания свойств и операций на нем.
Перейдем к последовательному описанию шагов.
Шаг один
Для начала необходимо определить границы моделируемой системы и понять ее основные компоненты. Для формального моделирования вовсе не обязательно описывать каждый компонент системы, достаточно выделить основные ее модули и задать их составляющие, объединив в классы (множества) по общим функциональным (нефункциональным) признакам.
Для примера давайте рассмотрим простейший модуль СЗИ - систему разграничения доступа прав пользователей (возьмем дискреционную модель разграничения доступа, как наиболее простую в описании). Важно заметить, что мандатная и ролевая системы будут, конечно, сложней в описании, но ненамного. В мандатной системе необходимо будет учесть проверку по мандатным уровням и меткам (то есть там будет не одна, а две функции проверки прав: по мандатным уровням и по мандатным меткам). А в ролевой системе необходимо будет учесть влияния ролей (также дополнительная функция проверки прав).
Вернемся к моделированию: для описания системы дискреционного разграничения доступа зададим основные рекомендуемые множества:
Важно заметить, что указанный набор множеств является лишь рекомендацией, если Вы видите необходимым ввести дополнительные множества, это не будет ошибкой. Главное - чтобы эти дополнительные множества действительно были полезны при моделировании.
Шаг два
Теперь необходимо задать свойства и операции на этих множествах.
Это очень важный этап, потому как в дальнейшем по сути все, что будет описано в данном пункте, будет характеризовать возможные состояния Вашей системы.
Приведу пример: одно из самых важных свойств множества при доказательстве безопасности системы - это его замкнутость. Почему это важно? Потому что по сути этим свойством Вы "говорите", что ситуация, при которой возникает дополнительный элемент множества, неудовлетворяющий свойствам этого множества, является невозможной. Если перенести это свойство к описанию СЗИ, это можно сравнить со следующим: в системе не может возникнуть состояния, при котором у пользователя, которому заранее присвоено определенное множество прав доступа, появляется дополнительно право доступа, которым он не должен обладать.
Здесь, конечно, должна быть важная оговорка, что поскольку создателем математического формального описания СЗИ являетесь Вы сами, написать Вы можете что угодно. И Ваша математическая модель, и ее доказательство безопасности могут быть сколь угодно точными. Важно помнить, что все, что Вы закладываете в формальную модель, должно быть реально реализовано в коде Вашего продукта.
И Вы в любой момент должны уметь доказать соответствие формальной модели Вашему продукту (пройти валидацию).
Именно поэтому я рекомендую Вам не перебарщивать со сложностью модели и не обещать в ней «золотых гор", которых по факту в Вашем продукте может не быть.
Зададим основные свойства и операции.
Будем говорить, что множество X обладает линейной структурой, если его элементы можно складывать и умножать по правилам, характерным для линейных структур.
Определение: Линейное пространство X определяется как множество элементов, на котором заданы две операции: сумма x+y и произведение λx (элемента x X на число λ из некоторого поля), причем
Замечание: При построении и доказательстве математической модели ДД понятие линейного пространства играет одну из ключевых ролей с точки зрения алгебры и теории множеств. Будем считать, что система Q равная декартовому произведению множеств S, O, P определена, как минимум, на линейном пространстве X. Понятие линейного пространства говорит о том, что для системы Q заданы простейшие алгебраические операции: сумма и произведение.
Замечание.
• Объединение любого числа и пересечение конечного числа открытых множеств есть открытое множество.
• Объединение конечного числа и пересечение любого числа замкнутых множеств – замкнутое множество.
• Дополнение замкнутого (открытого) множества до всего пространства есть открытое (замкнутое) множество.
• Замыкание любого множество замкнуто.
Шаг три
После того, как Вы определились с множествами и с их основными свойствами (важно заметить, что приведенных здесь свойств недостаточно для наиболее корректного построения модели, их скорее можно признать ключевыми) и операциями на них, необходимо задать функции, которые будут действовать в Вашем пространстве.
Здесь под функцией понимается правило взаимодействия субъектов и объектов доступа.
Помимо описания самих функций (что с чем работает) надо не забыть про свойства этих функций, важно, чтобы функции были непрерывными и замкнутыми относительно операций.
Шаг четыре
Теперь необходимо связать элементы множества с функциями, которые Вы задали.
Если Вы хотите создать модель, максимально удобную для чтения и проверки, Вы можете после описания каждой функции дать письменное разъяснения ее смысла.
Шаг пять
Заключительным этапом будет задание и доказательство основных теорем ИБ и теории множеств.
Здесь важно соблюдать последовательность: сперва Вы говорите, что принято считать безопасной системой, описываете ее свойства, которым она должна удовлетворять (отличная теория на эту тему есть в книжке Девянина П.Н. «Модели безопасности компьютерных систем. Управление доступом и информационными потоками»), затем переходите в математическое пространство, задаете смысловую однозначность теорем ИБ и теорем из теории множеств и далее доказываете теоремы в мат пространстве.
Их доказательство влечет за собой доказательство теорем ИБ и, следовательно, безопасность Вашей системы.
Отмечу еще раз, что указанный алгоритм построения и доказательства модели СЗИ не является единственным, но наиболее простым, по мнению автора.
Со статьей по теме формального моделирования, можно ознакомится здесь (в ней приведен полный текст примера моделирования СЗИ с дискреционной политикой разграничения доступа).
Далее планирую освятить вопрос моделирования МЭ и мандатной политики разграничения прав пользователей.
Буду рада взаимодействию с Вами!
