В связи с выходом приказа ФСТЭК России № 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
Комментарий удален модератором