Формальные и неформальные политики безопасности

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

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

Неформальные модели политик безопасности предполагают описание поведения подсистемы безопасности в рамках вербальных (словесных) утверждений, не обладающих математической строгостью. Утверждения в неформальных моделях, как правило, формируют требования к поведению подсистемы безопасности на общем уровне без указания особенностей их реализации.

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

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

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

Рассмотрим модели разграничения доступа в компьютерных системах. Возможная классификация таких моделей представлена ниже.