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

Зависимости
ADV_FSP.1 Неформальная функциональная спецификация
Элементы действий разработчика
ADV_SPM.3.1D	Разработчик должен представить модель ПБО.
ADV_SPM.3.2D	Разработчик должен демонстрировать или доказать, где это требуется, соответствие между функциональной спецификацией и моделью ПБО.
Элементы содержания и представления свидетельств
ADV_SPM.3.1C	Модель ПБО должна быть формальной.
ADV_SPM.3.2C	Модель ПБО должна содержать описание правил и характеристик всех политик ПБО, которые могут быть смоделированы.
ADV_SPM.3.3C	Модель ПБО должна включать в себя логическое обоснование, которое демонстрирует, что она согласована и полна относительно всех политик ПБО, которые могут быть смоделированы.
ADV_SPM.3.4C	Демонстрация соответствия между моделью ПБО и функциональной спецификацией должна показать, что все функции безопасности в функциональной спецификации являются непротиворечивыми и полными относительно модели ПБО.
ADV_SPM.3.5C	Там, где функциональная спецификация полуформальна, демонстрация соответствия между моделью ПБО и функциональной спецификацией должна быть полуформальной.
ADV_SPM.3.6C	Там, где функциональная спецификация формальна, доказательство соответствия между моделью ПБО и функциональной спецификацией должно быть формальным.
Элементы действий оценщика
ADV_SPM.3.1E	Оценщик должен подтвердить, что представленная информация удовлетворяет всем требованиям к содержанию и представлению свидетельств.