70. Классификация систем защиты. Доказательный подход к системам защиты .

Пусть задана политика безопасности Р. Тогда система защиты - хорошая, если она надежно поддерживает Р, и - плохая, если она ненадежно поддерживает Р. Однако надежность поддержки тоже надо точно определить. Здесь снова обратимся к иерархической схеме. Пусть политика Р выражена на языке Я₁, формулы которого определяются через услуги U₁,..., U_k.

Пример 1. Все субъекты S системы разбиты на два множества S₁ и S₂, S₁S₂=S, S₁S₂=. Все объекты, к которым может быть осуществлен доступ, разделены на два класса О₁ и О₂ O₁O₂= О, O₁O₂=. Политика безопасности Р -тривиальная: субъект S может иметь доступ R к объекту О тогда и только тогда, когда SS_i, О_i, i = 1, 2. Для каждого обращения субъекта S на доступ к объекту О система защиты вычисляет функции принадлежности

для субъекта и объекта: I_s( S₁), I_s( S₂), I₀( O₁), I₀( O₂). Затем вычисляется логическое выражение:

(I_s( S₁) I₀( O₁)) (I_s( S₂) I₀( O₂)).

Если полученное значение - 1 (истинно), то доступ разрешен. Если - 0 (ложно), то - неразрешен. Ясно, что язык Я₁, на котором мы выразили политику безопасности Р, опирается на услуги:

• вычисление функций принадлежности I_x(А);

• вычисление логического выражения;

• вычисление оператора "если x=l, то S ->0, если x=0, то S -+>О".

Для поддержки услуг языку Я₁, требуется свой язык Я₂, на котором мы определим основные выражения для предоставления услуг языку верхнего уровня. Возможно, что функции Я₂ необходимо реализоватьопираясь на язык Я₃ более низкого уровня и т.д.

Пусть услуги, описанные на языке Я₂ мы умеем гарантировать. Тогда надежность выполнения политики Р определяется полнотой ее описания в терминах услуг U₁,...,U_k. Если модель Р - формальная, то есть язык Я₁, формально определяет правила политики Р, то можно доказать или опровергнуть утверждение, что множество предоставленных услуг полностью и однозначно определяет политику Р. Гарантии выполнения этих услуг равносильны гарантиям соблюдения политики. Тогда более сложная задача сводится к более простым и к доказательству того факта, что этих услуг достаточно для выполнения политики. Все это обеспечивает доказанность защиты с точки зрения математики, или гарантированность с точки зрения уверенности в поддержке политики со стороны более простых функций.

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

Однако проводить подобный анализ в каждой системе дорого. Кроме того, методика проведения анализа государственных систем - конфиденциальная информация. Выход был найден в том, что условия теорем, доказывающих поддержку политики безопасности (включая соответствующую политику), формулировать без доказательства в виде стандарта. Такой подход американцы впервые применили в 1983 году, опубликовав открыто проект стандарта по защите информации в ЭСОД ("Оранжевая книга"), где сформулированы требования гарантированной поддержки двух классов политик - дискреционной и политики MLS. Затем этот метод они применили в 1987 г. для описания гарантированно защищенных распределенных сетей, поддерживающих те же политики, и в 1991 г.для описания требований гарантированно защищенных баз данных. Этот же путь использовали канадцы и европейские государства, создав свои стандарты защиты.