ГОСТ Р ИСО/МЭК 15408-3-2013
А.5 Дополнительный материал по формальным методам
ФормальныеметодыдаютматематическоепредставлениеоФБОиихрежиме
функционирования по требованиям ADV_FSP.6«Полная полуформальная функциональная
спецификация с дополнительной формальной спецификацией». ADV_SPM.1 «Формальная модель
политики безопасности ОО», и ADV_TDS.6 «Полный полуформальный модульный проект с
формальным высокоуровневым представлением». Существуют два аспекта формальных методов:
язы к специф икации,
который используется для формального выражения, и
доказат ельст во т еорем,
которое математически доказывает полноту и правильность формальной спецификации.
Формальная спецификация выражается в формальной системе, основанной на устоявшихся
математических понятиях. Эти математические понятия используются для определения четко
определенной семантики, синтаксиса и правил логических выводов. Формальная система является
абстрактной системой тождеств и отношений, которые можно описать, указав формальный алфавит,
формальный язык с использованием этого алфавита, основанный на формальном синтаксисе, и
набор формальных правил для построения логических выводов из предложений на формальном
языке.
Оценщику следует рассмотреть идентифицированные формальные системы с целью
удостовериться, что:
-Семантика, синтаксис и правила построения выводов формальной системы определены или
определения даются в ссылках.
-Каждая формальная система сопровождается пояснительным текстом, который содержит
определенную семантику, а именно:
1)в пояснительном тексте приводится определение терминов, сокращений и аббревиатур,
которые используются в ином контексте, нежели общепринятый;
2)использование формальной системы и полуформальной системы условных обозначений
используется в сочетании с пояснительным текстом в неформальном стиле изложения, приемлемом
для однозначного понимания:
3)формальная система способна отражать правила и характеристики применяемых ПФБ,
функциональных возможностей безопасности и интерфейсов ФБО (с указанием подробной
информации о последствиях, исключениях и сообщениях об ошибках), их подсистем или модулей,
подлежащих спецификации в семействе доверия, для которого используются условные обозначения;
4)в условных обозначениях предоставляются правила определения значения синтаксически
верных конструкций языка.
Вкаждойформальнойсистемеиспользуетсяформальныйсинтаксис,который
устанавливает правила для однозначной узнаваемости конструкций.
В каждой формальной системе устанавливаются правила доказательств, которые
5)поддерживают логические обоснования хорошо известных математических понятий,
6)помогают предотвратить возникновение противоречий.
Если разработчик использует формальную систему, которая уже прошла оценку, оценщик
может положиться на уровень формализованности и стойкости системы и сосредоточить внимание на
245