Группа А. Верифицированная защита

Данная группа характеризуется применением формальных методов верификации корректности работы механизмов управления доступом (дискреционного и мандатного). Требуется, чтобы было формально пока­зано соответствие архитектуры и реализации ТСВ требованиям безопас­ности.

Класс А1. Формальная верификация. Критерий защиты класса А1 не определяет дополнительные по сравнению с классом ВЗ требования к ар­хитектуре или политике безопасности компьютерной системы. Дополни­тельным свойством систем, отнесенных к классу А1, является проведен-

ный анализ ТСВ на соответствие формальным высокоуровневым специ­фикациям и использование технологий проверки с целью получения вы­соких гарантий того, что ТСВ функционирует корректно.

Наиболее важные требования к классу А1 можно объединить в пять групп:

• Формальная модель политики безопасности должна быть четко определена и документирована, должно быть дано математическое дока­зательство того, что модель соответствует своим аксиомам и что их доста­точно для поддержания заданной политики безопасности.

• Формальная высокоуровневая спецификация должна включать абстрактное определение выполняемых ТСВ функций и аппаратный и/или встроенный программный механизм для обеспечения разделения доменов.

• Формальная высокоуровневая спецификация ТСВ должна демон­стрировать соответствие модели политики безопасности с использовани­ем, где это возможно, формальной технологии (например, где имеются проверочные средства) и неформальной во всех остальных случаях.

• Должно быть неформально показано и обратное - соответствие элементов ТСВ формальной высокоуровневой спецификации. Формальная высокоуровневая спецификация должна представлять собой универсаль­ный механизм защиты, реализующий политику безопасности. Элементы этого механизма должны быть отображены на элементы ТСВ.

• Должны быть использованы формальные технологии для выявле­ния и анализа скрытых каналов. Неформальная технология может быть использована для анализа скрытых временных каналов. Существование оставшихся в системе скрытых каналов должно быть оправдано.

Более строгие требования предъявляются к управлению конфигура­цией системы и конкретному месту дислокации (развертывания) системы.

Перечисленные требования не затрагивают группы Политика безо­пасности и Подотчетность и сконцентрированы в группе Гарантии с соот­ветствующим описанием в группе Документация.