Росстандарт утвердил в качестве ГОСТов созданные в ГК Astra Linux стандарты на формальные модели управления доступом:

• ГОСТ Р 59453.1-2021 «Защита информации. Формальная модель управления доступом. Часть 1. Общие положения»;
• ГОСТ Р 59453.2-2021 «Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификация формальной модели управления доступом».
Основной их автор — ГК Astra Linux, при этом в создании второго стандарта приняли участие специалисты Института системного программирования им. В.П. Иванникова Российской академии наук (ИСП РАН).
Во время разработки и обсуждения национальных стандартов с ТК 362 в ГК Astra Linux велась их апробация. Для этого эксперты проверяли, насколько им соответствует формальная модель управления доступом (МРОСЛ ДП-модель), на основе которой в ОС Astra Linux Special Edition реализован механизм защиты PARSEC. Кроме того, отрабатывались соответствующие стандартам технологии перевода этой модели с математического языка на формализованный язык метода Event-B с последующей ее верификаций инструментальными средствами Rodin и ProB.
Подробности на нашем сайте: https://clck.ru/UpBcD