Формально-логическая модель системы контроля доступа для архитектуры Zero Trust

DOI:

Современные угрозы информационной безопасности, такие как целевые атаки, инсайдерские риски и утечки данных, демонстрируют недостаточность традиционных периметровых моделей защиты [1,2]. Концепция безопасности Zero Trust, основанная на принципах «никому не доверяй, проверяй всегда», становится новым стандартом для защиты критически важных активов и информации, составляющей коммерческую тайну [3,4]. Однако практическая реализация этой концепции сопряжена со сложностями, связанными с отсутствием строгих формальных описаний, что приводит к неоднозначности в интерпретации политик, логическим противоречиям и, как следствие, к уязвимостям в системе доступа [5].

Анализ литературы показывает, что существующие работы в основном посвящены архитектурным принципам и практическим аспектам внедрения Zero Trust [6], в то время как вопросы формального моделирования и верификации логики принятия решений остаются недостаточно разработанными, что создает пробел между высокоуровневыми концепциями и их корректной, доказуемо безопасной реализацией.

Целью данного исследования является разработка формально-логической модели системы контроля доступа, соответствующей ключевым принципам Zero Trust: динамическому контекстно-зависимому принятию решений, обязательной классификацией данных и непрерывной верификации. Для достижения поставленной цели решаются следующие задачи: формализация базовых сущностей и отношений в системе Zero Trust [7]; построение математической модели агрегации политик и оценки угроз; определение системы обязательных ограничений; демонстрация возможностей автоматизированной верификации на основе предложенной модели.

МАТЕРИАЛЫ И МЕТОДЫ

В качестве методологической основы исследования использован аппарат теории множеств и математической логики предикатов, что позволяет абстрагироваться от конкретных технологий реализации и сфокусироваться на строгом описании логики работы системы [8-10]. Исходными материалами для построения модели являются требования концепции Zero Trust. В формальной постановке задачи определены базовые множества и ключевые предикаты, представленные в Таблице 1.

Таблица 1. Описание переменных.

Table 1. description of variables.

Обозначение	Тип	Описание	Операции/Зависимости
levels	Множество	levels = {0,1,2,3}	Упорядоченное множеств уровней конфиденциальности Уровень 0 – публичный. Уровень 3 – совершенно секретно.
S	Множество	S = {S i , S 2 , ... , S n , } -множество    субъектов (пользователей, сервисов)	Элемент s e S.
R	Множество	R = {R i , R2, ■■■ , Rn, } Множество    ресурсов, содержащих коммерческую тайну. Каждому      ресурсу присвоен      уровень конфиденциальности C(r) e levels.	Элемент r e R.

p	Множество	P = {P 1 , P 2 , ... , P n , } Множество    политик доступа. p: S x R x к ^ {true, false}	Элемент p £ P. Политика p возвращает true, если в данном контексте она разрешает доступ субъекта s к ресурсу r
к	Множество	Множество   всех возможных состояний контекста К : L x D x n x ... (L -   множество геолокаций, D - доверие к устройву, N -доверие к сети и прочее)	Элемент k £ к - вектор, элемент декартова произведения.
A(s, r, k)	Предикат	Решающий предикат А : S x R x к ^ {true, false}	A(s, r, k) = V p(s, r, k), p £P Доступ разрешен, если хотя бы одна политика в текущем контексте разрешает его
T(s, r, k)	Предикат	T : S x r x к ^ {true, false}	Фиксирует    факт обнаружения признаков нарушения безопасности. Возвращает true, если в текущем контексте k для субъекта s и ресурса r система обнаружения угроз или анализа аномалий выявила признаки компрометации, нарушения, или рискованного поведения.
V(s, r, k)	Предикат	Непрерывная верификация . V : S x r x к ^ {true, false}	V(s, r, k) = A(s, r, k) Л -T(s, r, k) Доступ возможен только если политики разрешают и угроз не обнаружено
Access (s, r, k)	Функция решения	Access : S x R x к ^ {Pe'rmit, Deny, Terminat} Access (s, r, k) = Permit ^ V (s, r, k) = true Л -3 активная сессия Access (s, r, k) = Terminate ^ 3 активная сессия Л V(s, r, k) = false Access (s, r, k) = Deny ^ -3 активная сессия Л V(s, r, k) = false	Permit - начальное предоставление доступа. Terminate    - принудительное прекращение активного доступа (непрерывная верификация). Deny - отказ в начальном доступе. Форма 1 - Permit выдается только если условие доверия истинно и у субъекта нет уже открытой сессии к этому ресурсу. Форма 2 - Terminate выдается только если условие доверия стало ложным и сессия активна. Форма 3 - Deny выдается только если сессии нет и условие доверия ложно.

РЕЗУЛЬТАТЫ

В результате проведенного исследования разработана     формальная     модель     с определенными ограничениями.

Принцип явного запрета

Формализация:

Vs e 5, Vr e R, Vk e K: (Vp e P: p(s, r, k) = false) ^ A(s, r, k) = false           (1)

Пояснение к формуле (1): если все политики p возвращают false для запроса (s, r, k), то предикат разрешения A обязан быть false. Таким образом, доступ запрещен, если его явно не разрешает ни одна политика.

Монотонность по уровню

КОНФИДЕНЦИАЛЬНОСТИ

Формализация:

Vs e 5, Vr i , r j e R, Vk e K: (C(r i ) >  C(rj)) Л (A(s, r j , k) = false) ^ A(s, r i , k) = false      (2)

Пояснение к формуле (2): если политики запретили доступ к ресурсу r j c уровнем C(r j ), то доступ к любому ресурсу ri, с большим уровнем конфиденциальности C(ri), должен быть также запрещен.

Непротиворечивость контекстуальной

ОЦЕНКИ

Формализация:

Vs e S, Vr e R, Vk i , k j e K: (k i = k j ) ^ (Access(s, r, k i ) = Access(s, r, k j ))             (3)

Пояснение к формуле (3): если в два разных момента времени контекст k идентичен (включая все параметры:   геолокацию, доверие к устройству, доверие к сети и прочее), то и итоговое решение Access должно быть одинаковым. Это ограничение гарантирует предсказуемость системы.

Неотъемлемость непрерывной

ВЕРИФИКАЦИИ

Формализация:

Vs e S, Vr e R, Vk i , k j e K: ((Access(s, r, k i ) = Permit) Л (k i V k j )) ^ Access(s, r, k j ) e (4)

{Permit, Deny, Terminate}

Пояснение к формуле (4) : решение, принятое при другом контексте, не является гарантией доступа в будущем. Любое изменение контекста или появление угрозы должно перепроверяться .

Запрет на обход политик через контекст

Формализация:

Vs e S, Vr e R, Vk i , k e K: (Bk i : A(s, r, k i ) = false) ^ (Vk: A(s, r, k) = false)          (5)

Пояснение к формуле (5): если существует хотя бы один контекст (например, доверие к устройству), в котором политики запрещают доступ, то этот доступ запрещен во всех возможных контекстах. Таким образом, субъект не может, манипулируя параметрами контекста, получить доступ, который ему был бы запрещен.

Предложенная формализация создает строгую математическую основу для применения методов автоматизированной проверки корректности системы Zero Trust . Это позволяет автоматически и строго доказывать ключевые свойства безопасности не только ручным тестированием.

Статический анализ полноты политик

ДОСТУПА

Bs e S, Br e R, Bk e K: (Vp e P: p(s, r, k) = false)                   (6)

Автоматический поиск ситуаций, не покрытых политиками,       позволит       устранить неопределенность в правилах доступа.

Bs e S,Br e R, Bk e K, Bp_l,p j e P : (p_l(s,r,k) = true) Л (p j (s,r,k) = false) (7)

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

Динамическая проверка корректности

РАБОТЫ СИСТЕМЫ

Bs e S,Br e R,Bk e K: (Vp e P:p(s,r,k) = false) л(Access(s,r,k) = Permit)       (8)

Проверяем, существует ли сценарий, при котором доступ разрешен, хотя все политики его запрещают .

Bs e S,Br e R, Bk_t,k j e K: (A(s,r, k_l) = false) Л (Accesses,r,kj) = Permit) (9)

Проверяем, можно ли, изменив контекст, получить доступ, который в другом контексте был явно запрещен политиками .

Bs e S,Br_l,r j e R,Bk e K: (c(r_l) > C(r j )) Л (A(s,r j ,k) = false) Л (A(s,r_l,k) = true) (10)

Проверяем, возможно ли получить доступ к более секретному документу, когда доступ к менее секретному запрещен .

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

ОБСУЖДЕНИЕ

Алгоритм системы Zero Trust для обработки запроса доступа в момент времени t можно представить следующими этапами.

Таблица 2. Описание этапов решения задачи.

Table 2. Description of the stages of solving the problem.

Этап	Вход	Действия
Подготовка и сбор данных	Идентификатор субъекта s £ S , идентификатор ресурса r £ R, контекст k EK.	Извлечь уровень конфиденциальности ресурса с = С (г) Определить состояние сессии
Статическая оценка политик	Кортеж (s, г, к)	Для каждой политики р E Р вычислить ее решение p(s, г, к) Агрегировать результаты всех политик в A(s, г, к), который равен true - если все правила разрешают доступ, и false – иначе.
Динамическая оценка угроз	Кортеж (s, г, к)	Анализ контекста к и поведение субъекта s на предмет аномалий и индикаторов компрометации Вычисление предиката угрозы T(s, г, к), который равен true – угроза обнаружена, false - иначе
Расчет общего условия доверия	Предикаты A(s, г, k'),T(s, г, к)	Вычисление комплексного предиката верификации V (s, г, к) который равен true -системе можно доверять в данный момент для данного запроса, false- доверие нарушено
Принятие финального решения	Предикат V (s, г, к)	Применить логику функции Access

ЗАКЛЮЧЕНИЕ

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

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

Ключевым научным результатом является формализация пяти фундаментальных ограничений (1)  –  (5), обеспечивающих соблюдение    принципов    Zero    Trust.

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

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