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

Давайте разберемся, как построить формальную модель безопасности, если в штате не предусмотрены специалисты, компетентные в области формальной верификации, или нет времени разби- раться в том, как работают заточенные под эту задачу специализированные программные решения. По большому счету любое ПО – это дискретная система, поэтому проще всего ее описывать, пользуясь дискрет- ным представлением. Дискретное представление предпола- гает набор зависимых или независимых элементов, которые по каким-то при- знакам могут быть объединены во мно- жества и подмножества. Наиболее удоб- ным и простым математическим аппа- ратом, не требующим особенной подго- товки для использования, является тео- рия множеств. Перейдем к последова- тельному описанию шагов. Шаг первый Для начала необходимо определить границы моделируемой системы и понять ее основные компоненты. Для формального моделирования вовсе не обязательно описывать каждый компо- нент системы, достаточно выделить основные ее модули и задать их состав- ляющие, объединив в множества (груп- пы, классы) по общим функциональным (нефункциональным) признакам и свой- ствам. В качестве примера рассмотрим про- стейший модуль СЗИ – систему разгра- ничения доступа прав пользователей и дискреционную модель как наиболее простую в описании. Важно заметить, что мандатная и ролевая системы будут хотя немного, но все сложнее в описании. В мандатной системе необходимо учесть проверку по мандатным уровням и меткам. То есть в мандатной модели дополнительно потребуются две функции проверки прав: по мандатным уровням и по мандатным меткам. В ролевой системе необходимо учесть влияние ролей, то есть потребуется дополнительная функция проверки прав. Для описания системы дискреционного разграничения доступа зададим основ- ные рекомендуемые множества: l S – множество субъектов доступа; l O – множество объектов доступа; l C – множество контейнеров; l E = O ∪ C – множество объектов доступа (сущностей), где O ∩ C = ∅ ; l R r = {read r , write r , execute r , own r , remove r } – множество видов прав доступа; l R a = {read a , write a , remove a } – множе- ство видов доступа, где read a – доступ на чтение, write a – доступ на запись, remover – доступ на удаление; l P ⊆ S × (E ∪ S) × R r – множество прав доступа субъектов доступа к сущно- стям и субъектам доступа; l A ⊆ S × (E ∪ S) × R a – множество доступов субъектов доступа к сущно- стям и субъектам доступа; l R f = {write m , write t } – множество видов информационных потоков, где write m – информационный поток по памяти, write t – информационный поток по времени; l F ⊆ (E × S) × (E ∪ S) × R f – множество информационных потоков; l q = (S, O, P) – состояние системы; l Q – множество состояний системы; l M – матрица доступов, где M[s, o] ⊆ P – права доступа субъекта доступа s ∈ S к объекту o ∈ O. Важно заметить, что приведенный набор множеств является лишь реко- мендацией, и если вы считаете необхо- димым ввести дополнительные множе- ства, это не будет ошибкой. Главное, чтобы дополнительные множества дей- ствительно были полезны при модели- ровании, а не просто создавали избы- точность в описании модели. Шаг второй Теперь необходимо задать свойства и операции на множествах. Это очень важный этап, поскольку все, что будет описано на данном шаге, в дальнейшем будет характеризовать возможные состояния вашей системы. Пример. Одно из самых важных свойств множества при доказательстве безопасности системы – его замкнутость. Почему это важно? Потому что по факту данным свойством вы заявляете, что ситуация, при которой возникает дополнительный элемент множества, не удовлетворяющий свойствам данного множества, является невозможной. Если перенести описанное свойство на определение СЗИ, это можно трактовать так: в системе не может возникнуть состояние, при котором у пользователя с заранее присвоенным определенным множеством прав доступа p i появляется дополнительное право доступа p i+1 , не заданное администратором системы, то есть право, которым пользователь не должен обладать. 48 • ИССЛЕДОВАНИЕ 5 шагов построения формальной модели СЗИ для доказательства ее безопасности осле выхода приказа ФСТЭК России № 76 от 02.06.2020 г. “Об утверждении Требований по безопасности информации, устанавливающих уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий" разработчики ПО в области информационной безопасности для прохождения сертификации во ФСТЭК обязаны формально моделировать и доказывать безопасность своих СЗИ. В данной статье будут описаны пять основных шагов, с помощью которых можно построить формальную модель СЗИ и доказать ее безопасность. П Ксения Синцова, аспирант НИУ ВШЭ, департамент математики