Журнал "Information Security/ Информационная безопасность" #4, 2022

Как создатель формальной матема- тической модели СЗИ, вы можете напи- сать все, что сочтете необходимым, и при этом ваша математическая модель и ее доказательство безопасности могут быть сколь угодно точными и непроти- воречивыми. Но важно помнить, что все заложенное в формальную модель долж- но быть действительно реализовано в коде продукта. И вы должны уметь доказать соответствие каждой строчки формальной модели программному коду продукта, то есть пройти валидацию. Именно поэтому я рекомендую не переусложнять модель и не описывать априори невыполнимые условия без- опасности в вашем продукте, хотя бы и строгие в математическом плане. Тем самым создается потенциальная возможность несогласия исследователь- ской лаборатории с моделью и после- дующего непрохождения сертификации во ФСТЭК. Вернемся к модели. Зададим основ- ные свойства и операции множеств. Я намеренно привожу конкретный при- мер описания множеств, ведь, к сожа- лению, при анализе существующих моделей безопасности их авторы часто забывают указать именно свойства, которым удовлетворяют элементы мно- жества, – тем самым они повышают вероятность опровержения безопасности описываемой системы. Будем говорить, что множество X обладает линейной структурой, если его элементы можно складывать и умножать по правилам, характерным для линейных структур. Определение. Линейное пространство X определяется как множество элемен- тов, на котором заданы две операции: сумма x + y и произведение x (элемента x ∈ X на число λ из некоторого поля), причем x, y ∈ X ⇒ α x + β y ∈ X Операции удовлетворяют следующим аксиомам: l существует "единица": 1 ⋅ x = x; l λ ⋅ (μx) = λ ⋅ μ ⋅ x (ассоциативность умножения); l ( λ + μ) ⋅ x = λ x + μx, λ ⋅ (x + y) = λ x + λ y (дистрибутивность); l x + y = y + x (коммутативность); l (x + y) + z = x + (y + z) (ассоциативность суммы); l существует "ноль" ∈ X : x + 0 = x; l существует обратная величина -x ∈ X : x + (-x) = 0. Замечание. При построении и доказательстве математической модели дискреционного доступа понятие линейного пространства играет одну из ключевых ролей с точки зрения алгебры и теории множеств. Будем считать, что система Q, равная декартовому произведению множеств S, O, P, определена как минимум на линейном пространстве X. Понятие линейного пространства говорит о том, что для системы Q заданы простейшие алгебраические операции – сумма и произведение. Определение. Множество U ⊂ X откры- то, если вместе с каждой точкой u ∈ U оно содержит некоторую окрестность u, и замкнуто, если содержит все свои предельные точки. Замечания: l объединение любого числа и пере- сечение конечного числа открытых множеств есть открытое множество; l объединение конечного числа и пере- сечение любого числа замкнутых мно- жеств – замкнутое множество; l дополнение замкнутого (открытого) множества до всего пространства есть открытое (замкнутое) множество; l замыкание любого множество замкнуто. Важно отметить, что указанные свой- ства являются лишь необходимыми, но не достаточными. Для удобства проверки формальной модели рекомендуется также вносить замечания, в которых будет объяснена связь математических свойств и свойств реальной системы в терминах инфор- мационной безопасности. Шаг третий После того как вы определились со множествами, их основными свойствами и операциями на них, необходимо задать функции, которые будут действовать в вашем пространстве. Здесь под функ- цией понимается правило взаимодей- ствия субъектов и объектов доступа. Помимо описания самих функций (что с чем работает) не следует забывать и про свойства этих функций. Важно, чтобы функции были непрерывными и замкнутыми относительно операций. Определение. Функцию (оператор) f: X → Y называют непрерывной в точке x 0 , если для любого ε > 0 можно указать такое δ , что p Y (f(x), f(X 0 )) < δ , если p X (x, x 0 ) < ε , и непрерывной на X, если она непре- рывна в любой точке X. Определение. Линейное нормирован- ное пространство, если оно полно, назы- вается ба' наховым. Определение. Линейный оператор A называется замкнутым, если из x n → x и Ax n → y следует x ∈ D A и Ax = y. Замечание. Если оператор определен на всем (банаховом) пространстве, то замкнутость и ограниченность равно- сильны. Если вы хотите создать максимально удобную для чтения и проверки модель, то после описания каждой функции можно дать письменное разъяснение ее смысла. Шаг четвертый Четвертым шагом является задание и доказательство основных теорем информационной безопасности и теории множеств. На этом шаге важно соблюдать после- довательность. 1. Сначала вы говорите, что принято считать безопасной системой, описы- ваете свойства, которым она должна удовлетворять 1 . 2. Затем переходите в математическое пространство, задаете необходимые тео- ремы теории множеств. Примером таких теорем может быть теорема отделимости и аксиома выбора. И далее строите и доказываете по ним безопасность математической модели СЗИ. Шаг пятый Заключительным этапом будет зада- ние смысловой однозначности теорем ИБ и теорем из теории множеств. В модели важно объяснить, какие именно свойства, операции, теоремы в математическом пространстве будут доказывать соответствие модели кри- териям безопасной системы – изоли- руемости, полноты и верифицируемо- сти. Затем делается вывод о том, что доказательство модели в математиче- ском пространстве влечет за собой дока- зательство теорем ИБ и, следовательно, безопасность вашей системы. Описанный алгоритм построения и доказательства модели СЗИ является не единственным, но наиболее простым, по мнению автора. l • 49 ИССЛЕДОВАНИЕ www.itsec.ru 1 Отличная теория на эту тему есть в книге Девянина П.Н. “Модели безопасности компьютерных систем. Управление доступом и информационными потоками". Ваше мнение и вопросы присылайте по адресу is@groteck.ru