ГОСТ Р ИСО/МЭК 15408-3-2013 Информационная технология (ИТ). Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности

     11.5 Моделирование политики безопасности (ADV_SPM)

11.5.1 Цели

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

11.5.2 Ранжирование компонентов

Семейство содержит только один компонент.

11.5.3 Замечания по применению

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

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

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

Модель политики безопасности ОО выводится в неформальном виде из ее реализации посредством рассмотрения предлагаемых требований безопасности из ЗБ. Неформальное представление считается успешно осуществленным в случае, когда выполнение принципов ОО (называемых также "неизменными", "инвариантами") осуществляется его характеристиками. Цель формальных методов состоит в усилении строгости такого выполнения. Представление неформальных доводов часто приводит к наличию среди них доводов заведомо неверных и необоснованных; в особенности это касается тех случаев, когда возрастает степень влияния взаимоотношений между объектами, субъектами и операциями. С целью минимизации риска возникновения небезопасных состояний выполняется прослеживание правил и характеристик модели политики безопасности с соответствующими свойствами и характеристиками некой формальной системы, чья строгость и стойкость могут быть впоследствии использованы для получения свойств безопасности посредством теорем и формального доказательства.

В то время как термин "формальная модель политики безопасности" используется в основном в академических кругах, в ИСО/МЭК 15408 нет фиксированного определения термина "безопасность"; его значение приравнивается к изложенному в ФТБ. Таким образом, формальная модель политики безопасности является лишь формальным представлением набора изложенных ФТБ.

Термин политика безопасности традиционно ассоциируется только с политиками контроля доступа, мандатного (полномочного) или избирательного (дискреционного). Однако содержание политики безопасности не ограничивается только правилами контроля доступа; существуют также политики аудита, идентификации, аутентификации, шифрования, управления и другие требуемые в ОО политики безопасности, реализуемые в соответствии с их описаниями в ПЗ/ЗБ. Компонент ADV_SPM.1.1D предназначен для идентификации таких формально модулируемых политик.

11.5.4 ADV_SPM.1 Формальная модель политики безопасности ОО

Зависимости: ADV_FSP.4 Полная функциональная спецификация

11.5.4.1 Элементы действий разработчика
     

    11.5.4.1.1 ADV_SPM.1.1D

Разработчик должен представить формальную модель ПБО для [назначение: список формально моделируемых политик].

11.5.4.1.2 ADV_SPM.1.2D

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

    11.5.4.1.3 ADV_SPM.1.3D

Разработчик должен представить формальное доказательство соответствия между какой-либо формальной функциональной спецификацией и моделью ПБО.
     

    11.5.4.1.4 ADV_SPM.1.4D

Разработчик должен продемонстрировать соответствие между функциональной спецификацией и моделью ПБО.
     

    11.5.4.2 Элементы содержания и представления свидетельств
     

    11.5.4.2.1 ADV_SPM.1.1C

Модель ПБО должна быть изложена в формальном стиле с предоставлением вспомогательного пояснительного текста согласно требованиям и в ней должны быть идентифицированы моделируемые политики ФБО.
     

    11.5.4.2.2 ADV_SPM.1.2C

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

    11.5.4.2.3 ADV_SPM.1.3C