ГОСТ Р ИСО/МЭК 15408-3-2002
Элементы содержания и представления свидетельств
ADV RCR.2.1C Для каждой смежной пары имеющихся представлении ФБО анализдолжен де
монстрировать. что всефункциональные возможности более абстрактного пред
ставления ФБО. относящиеся к безопасности, правильно и полностью
уточнены вменее абстрактном представлении ФБО.
ADV_RCR.2.2C Для каждой смежной пары имеющихся представлений ФБО, где части обоих
представлений специфицированы но меньшей мере полуформально, демонстрация
соответствия между этими частями представлений должна быть полуформальной.
Элементы действий оценщика
ADV_RCR.2.1E Оценщикдолжен подтвердить, что представленная информация удовлетворяет
всем требованиям к содержанию и представлению свидетельств.
ADV RCR.3 Формальная демонстрация соответствия
Замечания по применению
Необходимо, чтобы разработчиклибо демонстрировал, либо доказал соответствие, как описано
ниже в требованиях, соразмерно с уровнем строгости стиля представления. Например, соответствие
необходимо докатать, если используемые представления специфицированы формально.
Зависимости отсутствуют.
Элементы действий разработчика
ADV_RCR*3.1D Разработчик должен представить анализ соответствия между всеми смежными
парами имеющихся представлений ФБО.
ADV_RCR.3.2D Для тех из соответствующих частей представлений, которые специфицированы
формально, разработчик должен доказать это соответствие.
Элементы содержания и представления свидетельств
ADV RCR.3.1C Для каждой смежной пары имеющихся представлений ФБО анализдолжен до
казать иди демонстрировать, что все функциональные возможности более
абстрактного представления ФБО. относящиеся к безопасности, правильно и
полностью уточнены в менее абстрактном представлении ФБО.
ADV_RCR.3.2C Для каждой смежной пары имеющихся представлений ФБО, где части одного
представления специфицированы полуформально, а другого —по меньшей мере
полуформально, демонстрация соответствия между этими частями представле
ний должна быть полуформальной.
ADV_RCR.3.3C Для каждой смежной пары имеющихся представлений ФБО, где части обоих
представлений специфицированы формально, доказательство соответствия меж
ду этими частями представлений должно быть формальным.
Элеме>ггыдействий оценщика
ADV_RCR.3.1E Оценщикдолжен подтвердить, что представленная информация удовлетворяет
всемтребованиям к содержанию и представлению свидетельств.
ADV RCR.3.2E Оценщик должен сделать независимое заключение о правильности доказательств
соответствия, избирательно верифицируя формальный анализ.
10.7 Моделирование политики безопасности (ADV_SPM)
Цели
Цель этого семейства —повыситдоверие, что функция безопасности вфункциональной специ
фикации осуществляют политики Г1БО. Эго выполняется посредством разработки модели политики
безопасности, которая основана на подмножестве политик ПБО, и установления соответствия между
функциональной спецификацией, моделью политики безопасности и этим подмножеством политик
ПБО.
Ранжирование компонентов
Компоненты в этом семействе ранжированы на основе степени формализации, требуемой от
модели ПБО. и степени формализации, требуемой при установлении соответствия между моделью
ПБО ифункциональной спецификацией.
Замечания по применению
В то время как ПБО может включать в себя любые политики, модели ПБО традиционно пред
ставляют только подмножества этих политик, потому что моделирование некоторых политик в насто
ящее время не предстаатяется выполнимым. Современное состояние вопроса определяет политики,
которые могутбыть смоделированы, и автору ПЗ/ЗБ следует идентифицироватьконкретные функции
(А