О проблеме представления формальной модели политики безопасности операционных систем

В связи с начавшимся процессом внедрения ФСТЭК России «Требований безопасности информации к операционным системам» в работе анализируются пути выполнения требований функциональной компоненты ADV_SPM.1 «Формальная модель политики безопасности», в том числе по определению языка, глубины и детализации представления модели политики безопасности управления доступом и информационными потоками. При этом приводятся предложения по составу основных элементов модели, использованию для ее верификации инструментальных средств. Практическая возможность применения предлагаемых подходов рассматривается на примере представления описания и верификации МРОСЛ ДП-модели, как основы механизма управления доступом в ОССН Astra Linux Special Edition.