В связи с выходом приказа ФСТЭК России № 76 от 02.06.2020 «Об утверждении Требований по безопасности информации, устанавливающих уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий» создание и доказательство безопасности формальных математических моделей средств защиты информации (СЗИ) является обязательным шагом для прохождения сертификации продуктов от 4 уровня доверия и выше.
Что это значит простым языком? Теперь, чтобы пройти сертификацию во ФСТЭК разработчикам ПО в области информационной безопасности необходимо моделировать работу своих продуктов с помощью математических или программных решений.
В принципе эта задача не такая уж и сложная, если у Вас в штате есть сотрудники с профильным образованием, в ином случае подготовка формальной модели может вызвать ряд трудностей, о которых расскажу далее.
Первое и самое основное - Вам придется самим определять до какого уровня абстракции Вы будете моделировать работу своих продуктов. Фактически регулятор не дает четких объяснений того, что он "хочет" видеть в Ваших моделях, только общие рекомендации. Классические критерии безопасной системы: Изолированность, Полнота, Верифицируемость остаются не параметризованными; то есть нам до конца не известно что именно является отражением этой самой Изолированности, Полноты и Верифицируемости?
В целом это опять же решаемый вопрос, если у Вас в штате имеются "толковые ребята", которые адекватно смогут оценить какую часть системы действительно надо моделировать, а какую нет, во избежание создания избыточных моделей, на разработку которых затрачивается непростительно много времени и часть которых может просто уйти "в стол".
Допустим с полнотой модели Вы как-то разобрались, что дальше?
А дальше переходим к выбору среды моделирования. Здесь, к счастью, все более не менее определено: официальные представители регулятора рекомендуют открытую платформу для верификации и моделирования Rodin в нотации Event-B. Платформа позволяет моделировать и проверять логику работы Вашего ПО, подсвечивая "опасные" участки кода.
Здесь сложности могут возникнуть только с освоением самой среды, потому как все мануалы написаны на английском. Сама среда является довольно мощным инструментом моделирования, имеет ряд особенностей в установке, но с этим также реально разобраться (ссылку на отличное вводное методическое пособие, выпущенное в этом году студентами ИТМО, даю ниже).
Несмотря на то, что Rodin заслуженно стал лидером в решении задач формальной верификации, он не единственный.
Существуют также такие инструменты, как СPN Tools (теория сетей Петри), SPIN (темпоральная логика, автоматы Бюхи), Coq (теория исчисления конструкций), Isabelle (теория логики высшего порядка) и ряд иных менее профильных решений. Все они имеют свои особенности и основаны хоть и на "соседствующих", но все же различных математических теориях.
На этом у меня все. Далее планирую ряд статей, где подробно расскажу о применении математического аппарата, который можно выбрать, если у Вас нет времени разбираться в существующих программных решениях (возможно для кого-то это будет более простой путь решения задачи построения формальных моделей).
И несколько полезных ссылок, которые могут пригодиться:
Выписка из Требований по безопасности информации, утвержденных приказом ФСТЭК России от 2 июня 2020 г. N 76: https://fstec.ru/tekhnicheskaya-zashchita-informatsii/dokumenty-po-sertifikatsii/120-normativnye-dokumenty/2126-vypiska-iz-trebovanij-po-bezopasnosti-informatsii-utverzhdennykh-prikazom-fstek-rossii-ot-2-iyunya-2020-g-n-76
Ссылка на сайт института ИСП РАН (институт поддерживает нотацию Event-B, на сайте можно найти серию полезных публикаций по этой теме) : https://www.ispras.ru/
Официальная страница платформы Rodin : Event-B.org
Ссылка на вводное методическое пособие по Event-B: RTF Template (ifmo.ru)
Моя последняя статья, где я привожу пример математического моделирования и доказательства политики дискреционного разграничения доступа (советую, там даны основы): http://www.inside-zi.ru/pages/5_2021/52.html
Ссылка на наш телеграмм канал, где будут новости по теме решения задач формальной верификации и моделирования сложных систем: https://t.me/stingraymathcenter
