Верификация спецификаций архитектуры

Класс B1. должна существовать неформальная или формальная модель политики безопасности, поддерживаемой надежной вычислительной базой. Модель должна соответствовать основным посылкам политики безопасности на протяжении всего жизненного цикла системы.

Класс B2. в дополнение к B1, модель политики безопасности должна быть формальной. Для надежной вычислительной базы должны существовать описательные спецификации верхнего уровня, точно и полно определяющие ее интерфейс.

Класс B3. в дополнение к B2, должны быть приведены убедительные аргументы соответствия между спецификациями и моделью.

Класс A1. в дополнение к B3, помимо описательных, должны быть представлены формальные спецификации верхнего уровня, относящиеся к аппаратным и/или микропрограммным элементам, составляющим интерфейс надежной вычислительной базы. Комбинация формальных и неформальных методов должна подтвердить соответствие между спецификациями и моделью. Должны использоваться современные методы формальной спецификации и верификации систем, доступные Национальному центру компьютерной безопасности США. Ручное или иное отображение формальных спецификаций на исходные тексты должно подтвердить корректность реализации надежной вычислительной базы.

Конфигурационное управление

Класс B2. в процессе разработки и сопровождения надежной вычислительной базы должна использоваться система конфигурационного управления, обеспечивающая контроль за изменениями в описательных спецификациях верхнего уровня, иных архитектурных данных, реализационной документации, исходных текстах, работающей версии объектного кода, тестовых данных и документации. Конфигурационное управление должно обеспечивать соответствие друг другу всех аспектов текущей версии надежной вычислительной базы. Должны предоставляться средства генерации новых версий базы по исходным текстам и средства для сравнения версий, чтобы убедиться в том, что произведены только запланированные изменения.

Класс A1. в дополнение к B2, механизм конфигурационного управления должен распространяться на весь жизненный цикл и все компоненты системы, имеющие отношение к обеспечению безопасности, включая спецификации и документацию. Для защиты эталонной копии материалов, использующихся для генерации надежной вычислительной базы, должна использоваться комбинация физических, административных и технических мер.