5.3.2 На начальном этапе проектирования КСЗ должна быть построена модель защиты, задающая принцип разграничения доступа и механизм управления доступом. Эта модель должна содержать:
- непротиворечивые ПРД;
- непротиворечивые правила изменения ПРД;
- правила работы с устройствами ввода и вывода;
- формальную модель механизма управления доступом.
Спецификация части КСЗ, реализующего механизм управления доступом и его интерфейсов, должна быть высокоуровневой. Эта спецификация должна быть верифицирована на соответствие заданным принципам разграничения доступа.
Для высоких классов защищенности СВТ должно быть предусмотрено, чтобы высокоуровневые спецификации КСЗ были отображены последовательно в спецификации одного или нескольких нижних уровней вплоть до реализации высокоуровневой спецификации КСЗ на языке программирования высокого уровня. При этом методами верификации должно быть доказано соответствие каждого такого отображения спецификациям высокого (верхнего для данного отображения) уровня, а также соответствие объектного кода тексту КСЗ на языке высокого уровня. Этот процесс может включать в себя как одно отображение (высокоуровневая спецификация - язык программирования), так и последовательность отображений в промежуточные спецификации с понижением уровня вплоть до языка программирования. В результате верификации соответствия каждого уровня предыдущему должно достигаться соответствие реализации высокоуровневой спецификации КСЗ модели защиты [из 5.3.2 ГОСТ Р 50739-95]
