Модель безопасности Astra Linux — основа для апробации новых ГОСТов

Федеральное агентство по техническому регулированию и метрологии (Росстандарт) утвердило национальные стандарты ГОСТ Р 59453.1-2021 «Защита информации. Формальная модель управления доступом. Часть 1. Общие положения» и ГОСТ Р 59453.2-2021 «Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификация формальной модели управления доступом». Основным их автором является ГК Astra Linux, при этом в создании второго стандарта приняли участие специалисты Института системного программирования им. В.П. Иванникова Российской академии наук (ИСП РАН).

Разработка формальной модели управления доступом и ее верификация с применением инструментальных средств — это часть требований 4 и 3 уровней доверия, согласно утвержденной приказом ФСТЭК России от 2 июня 2020 г. № 76 второй редакции «Требований по безопасности информации, устанавливающих уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий». Именно на нормативное обеспечение выполнения этих требований направлены новые национальные стандарты.

Получение сертификата ФСТЭК России по 4 уровню доверия обязательно для программных продуктов, которые применяются на значимых объектах критической информационной инфраструктуры до первого класса включительно и в автоматизированных системах управления процессами, а начиная с 3 уровня доверия — в государственных информационных системах первого класса, в том числе обрабатывающих персональные данные и гостайну.

Стандарт Р 59453.1-2021 устанавливает критерии, которым должна соответствовать формальная модель управления доступом, описанная на математическом или формализованном (машиночитаемом) языке. Кроме того, в документе можно найти определения тех ключевых терминов, что используют разработчики средств защиты информации: политик дискреционного, мандатного и ролевого управления доступом, а также мандатного контроля целостности.

Во втором ГОСТе изложены рекомендации в части перевода описания формальной модели на формализованный язык и ее верификации с применением инструментальных средств.

Во время разработки и обсуждения национальных стандартов с ТК 362 в ГК Astra Linux велась их апробация. Для этого эксперты проверяли, насколько им соответствует формальная модель управления доступом (МРОСЛ ДП-модели), на основе которой в операционной системе специального назначения Astra Linux Special Edition реализован механизм защиты PARSEC. Кроме того, отрабатывались соответствующие стандартам технологии перевода этой модели с математического языка на формализованный язык метода Event-B с последующей ее верификаций инструментальными средствами Rodin и ProB.