Учебно-методический комплекс теоретические основы компьютерной безопасности

Состояние v₀ безопасно, и

Функция переходов FT такова, что для любого состояния v, достижимого из v₀ при выполнении конечной последовательности запросов из множества Q таких, что при FT (v,q)=v*, где v=(F_L,A) и v*=(F_L*,A*), переходы системы из состояния в состояние подчиняются следующим ограничениям для s∈S и для o∈O

• 
  если read ∈A*[s,o] и read ∈A[s,o], то F_L*(s) ≥ F_L*(o);
  
• 
  если read ∈A[s,o] и F_L*(s) < F_L*(o), то read ∉ A*[s,o]; - если write ∈A*[s,o] и write ∉A[s,o], то F_L*(s) ≥ F_L*(o);
  
• 
  если write ∈A[s,o] и F_L*(s) < F_L*(o), то write ∉A*[s,o] .
  

Доказательство.
Необходимость. Предположим, что система безопасна. Тогда состояние v₀ безопасно по определению. Предположим также, что существует некоторое состояние v, достижимое из состояния v₀ путем исполнения конечной последовательности запросов из Q, при которых FT (v,q)= v*, и при этом одно из первых двух ограничений (по чтению) не выполняется. Тогда, хотя состояние v* и является достижимым, но небезопасно по определению 2.2.3. Если в состоянии v* не выполняется одно из двух последних (по записи) ограничений, то в этом случае состояние v* также будет небезопасным, но уже по определению 2.2.4. Таким образом, условия теоремы действительно необходимы для обеспечения безопасности системы. Достаточность. Предположим, что система небезопасна. Тогда должно быть небезопасным либо состояние v₀, либо состояние v, достижимое из v₀ путем исполнения конечной последовательности запросов из Q . Исходное состояние v₀ безопасно по условию теоремы. Тогда, так как v₀ безопасно, небезопасно какое-либо состояние v*, переход в которое осуществляется из безопасного состояния v: FT (v,q)=v*. Однако это противоречит четырем ограничениям на переходы FT по условиям теоремы. Следовательно, такой переход невозможен, и данное утверждение (о том, что система небезопасна) неверно. Таким образом, условия теоремы достаточны для безопасности системы Σ(v₀ ,Q, FT). Теорема доказана. ■
Ввиду формального характера изложения и доказательства ОТБ несколько подробнее поясним ее суть. Четыре ограничения на функцию переходов фактически выражают требования соблюдения в каждом состоянии системы правил NRU и NWD независимо от предыстории доступов конкретных субъектов к конкретным объектам:

• 
  если какой-либо субъект имеет разрешение на доступ к какому-либо объекту и в предыдущем состоянии и в новом (следующем) состоянии по матрице доступа, то и в новом состоянии это возможно только лишь при доминировании его уровня безопасности над уровнем объекта;
  
• 
  если какой-либо субъект в предыдущем состоянии имел права чтения какого-либо объекта, а при переходе в новое состояние понизил свой уровень безопасности ниже уровня безопасности объекта, то право чтения по матрице доступа соответствующего субъекта к соответствующему объекту должно быть аннулировано;
  
• 
  если как в предыдущем, так и в следующем состоянии какой-либо субъект по матрице доступа имеет право записи в какой-либо объект, то это возможно только лишь при условии, что и в новом состоянии уровень безопасности объекта будет доминировать над уровнем безопасности субъекта;
  
• 
  если в предыдущем состоянии по матрице доступа какой-либо субъект имел право записи в какой-либо объект, а при переходе системы в новое состояние уровень объекта понизился до уровня ниже уровня субъекта, то право записи субъекта в данный объект по матрице доступа в новом состоянии должно быть аннулировано.
  

Иначе говоря, при переходах системы в новое состояние в матрице доступа не должно возникать никаких новых, и не должно сохраняться никаких старых отношений доступа, которые были бы небезопасны в смысле правил NRU и NWD.
Таким образом, ограничения, накладываемые на функцию перехода FT, по сути, совпадают с критериями безопасности и в этом отношение
ОТБ избыточна.
Модель Белла-ЛаПадулы сыграла огромную роль в развитии теории компьютерной безопасности, и ее положения были введены в качестве обязательных требований к системам, обрабатывающим информацию, содержащую государственную тайну, в стандартах защищенных КС, в частности, в известной "Оранжевой книге" (1983 г.). Одной из сильных сторон модели Белла-ЛаПадулы является автоматическое решение проблемы "троянских" программ. Процесс переноса информации с помощью "троянской" программы из объекта, доступ к которому субъекту не разрешен по матрице доступа, регламентируется как и любые другие потоки принципами NRU и NWD. Таким образом, если такой перенос информации и произойдет, то он будет укладываться в ограничения определений 2.2.3 и 2.2.4, и, следовательно, с точки зрения критерия безопасности по определению 2.2.6 система останется в безопасном состоянии.