ГОСТ Р ИСО/МЭК 15408-3 — 2008
Данным классом узаконены три типа стиля изложения спецификаций: неформальный, полуфор
мальный иформальный. Функциональнаяспецификация, проект верхнего уровня, проект нижнего уровня и
модель ПБО будут изложены с применением одного или нескольких из этих стилей спецификации.
Неоднозначностьв этих спецификациях уменьшается с повышением уровняформализации стиля изложе
ния.
Неформальную спецификацию излагают кактекст на естественном языке. Под «естественным язы
ком» здесь подразумевается применение выразительных средств общения любого разговорного языка
(например, английского, немецкого, русского, французского). Неформальная спецификация не подчинена
никаким нотационным илиспециальным ограничениям, отличным от общепринятых соглашений дляэтого
языка (таких, как грамматика исинтаксис). Хотя нотационныеограничения в неформальной спецификации
не применяют, всежетребуется привести определения значений терминов, использование которых в кон
тексте отличается от общепринятого.
Полуформальную спецификацию излагают на языке с ограниченным синтаксисом иобычно сопро
вождают вспомогательным пояснительным (неформальным) текстом. Язык сограниченным синтаксисом
может бытьестественным языком с ограниченной структурой предложения иключевыми словами соспе
циальными значениями или языком схем (таких как схемы потоков данных, переходов, взаимосвязей
сущностей, структурданныхи процессов или структур программ). В обоих случаях обязателен набор со
глашений, позволяющих определитьограничения, накладываемые на синтаксис.
Формальнуюспецификацию излагаютс использованием нотации, основанной на известных матема
тических понятиях, иобычно сопровождают вспомогательным пояснительным (неформальным) текстом.
Эти математические понятия используют для того, чтобы определить синтаксис и семантику нотации и
правила доказательства, поддерживающие логическую аргументацию. Необходимо, чтобы синтаксичес
кие исемантические правила, регламентирующие формальную нотацию, определяли, какоднозначно рас
познавать конструкции иопределять ихзначение. Требуется свидетельство невозможности вывода проти
воречий. аправила, регламентирующие нотацию, необходимо определить или привести ссылку на них.
Существенное доверие может быть достигнуто обеспечением прослеживания ФБО до каждого из
представлений исоответствия модели ПБО функциональной спецификации. СемействоADV_RCR «Соот
ветствие представлений» содержит требования котображениюсоответствия между различнымипредстав
лениями ФБО, а семействоADV_SPM «Моделирование политики безопасности» — между моделью ПБО
ифункциональной спецификацией. Соответствие может принять форму неформальной илиполуформаль
ной демонстрации либоформальногодоказательства.
Когда требуется неформальная демонстрациясоответствия, это означает, что требуется толькосоот
ветствие посути. Методы демонстрации включают в себя, например использованиедвумерной таблицы с
входами, обозначающими соответствие, или подходящей для этого нотации схем проекта. Могут быть
также использованы указатели иссылки надругие документы.
Полуформальнаядемонстрация соответствия требует структурного подхода при анализе соответ
ствия. Необходимо, чтобы при этом подходе уменьшалась неоднозначность, которая может существовать
при неформальном соответствии, ограничивая интерпретациюприменяемых терминов. Могут бытьтакже
использованы указатели и ссылки надругиедокументы.
Формальноедоказательство соответствия требует, чтобы были использованы известные математи
ческие понятия для определения синтаксиса исемантики формальной нотации иправилдоказательства,
которые поддерживают логическую аргументацию. Необходимо, чтобы свойства безопасности могли быть
выражены наязыкеформальной спецификации, и былопоказано, что эти свойства удовлетворяются фор
мальной спецификацией. Могут быть также использованы указатели иссылки на другиедокументы.
ЭлементыADV_RCR.*.1Ссодержат требование, чтобы разработчик представил свидетельстводля
каждой смежной пары представлений ФБО, что все относящиеся к безопасности функциональные воз
можности более абстрактного представления ФБО уточнены в менее абстрактном представлении ФБО.
Каждый из элементов ADV_FSP.*.2E. ADV_HLD.*.2E. ADV_LLD.*.2E и ADV_IMP.*.2E содержит требова
ние. чтобы оценщик сделал заключениео том. чтоФБО. представляемыеэтимсемейством требований. —
точное иполное отображениефункциональных требований безопасности 00. Предполагается, что оцен
щик использует свидетельство, предоставленное разработчиком в соответствии сADV_RCR.*. 1C, какос
нование длятакогозаключения. Устанавливая соответствие между функциональными требованиями безо
пасности ОО икаждым из цепочки последовательных представлений ФБО, этот пошаговый процесспре
доставит, в конечном счете, более высокоедовериесоответствию наименее абстрактного представления
ФБО функциональным требованиям безопасности 00. что и является конечной целью данного класса.
54