Теоретические основы защиты информации.

Поэтому предположение неверно и теорема 1 доказана.

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

Условие 1. (Идентификация и аутентификация). Если для любых tÎN, pÍR, S, ОÎО_t, , то вычислены функции принадлежности S и О к множествам О_t(U₁), О_t(U₂), D.

Условие 2. (Разрешительная подсистема). Если SÎО_t(U_i), OÎО_t(U_j) и  в момент t, то из i=j следует

, и из i¹j следует  (не разрешается доступ).

Условие 3. (Отсутствие обходных путей политики безопасности). Для любых tÎN, рÍR, если субъект S, активизированный к моменту t, получил в момент t доступ , то в момент t произошел запрос на доступ .

Теорема 2. Если в построенной системе å выполняются предположения 1-4 и условия 1-3, то выполняется политика безопасности.

Доказательство. Утверждение теоремы следует из двух утверждений:

а) Если для произвольного рÍR , SÎO_t(U_i), OÎO_t(U_i), то доступ  разрешен.

б) Если SÎO_t(U_i), OÎO_t(U_j), i¹j, то какой-либо доступ в момент t субъекта S к объекту О невозможен.

Докажем а). Если , то по условию 1 вычислены функции принадлежности и определено, что SÎO_t(U_i), OÎO_t(U_j). Если i = j, то выполнена посылка условия 2. Тогда согласно условию 2 доступ разрешен.

Докажем теперь б). Если , вычислены функции принадлежности и определено, что SÎO_t(U_i), OÎO_t(U_j), i¹j. Тогда по условию 2 доступ не разрешен.

Если доступ  стал возможен, минуя запрос , и S - активизирован к моменту t, то сделанное предположение противоречит условию 3. Если S - не активизирован, то наличие доступа  противоречит определению доступа. Теорема доказана.

Теорема означает, что гарантировав выполнение условий 1-3, мы гарантируем выполнение политики безопасности.

Рассмотрим вопрос о создании системы, в которой можно с достаточной степенью уверенности поддерживать функции 1-3. Для этого рассмотрим следующую архитектуру:

1. В каждый момент только один пользователь может работать с системой. Физическое присутствие другого исключено.

2. При смене пользователей системы друг другом уходящий :

*                записывает во внешнюю память все объекты, которые он хочет сохранить для дальнейших сеансов;

*                 выключает питание