23.03.2022 13:45
IamreadyMotor 4 4100 Источник

В связи с выходом приказа ФСТЭК России № 76 от 02.06.2020 «Об утверждении Требований по безопасности информации, устанавливающих уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий» создание и доказательство безопасности формальных математических моделей средств защиты информации (СЗИ) является обязательным шагом для прохождения сертификации продуктов от 4 уровня доверия и выше.

Что это значит простым языком? Теперь, чтобы пройти сертификацию во ФСТЭК разработчикам ПО в области информационной безопасности необходимо моделировать работу своих продуктов с помощью математических или программных решений.

В принципе эта задача не такая уж и сложная, если у Вас в штате есть сотрудники с профильным образованием, в ином случае подготовка формальной модели может вызвать ряд трудностей, о которых расскажу далее.

Первое и самое основное - Вам придется самим определять до какого уровня абстракции Вы будете моделировать работу своих продуктов. Фактически регулятор не дает четких объяснений того, что он "хочет" видеть в Ваших моделях, только общие рекомендации. Классические критерии безопасной системы: Изолированность, Полнота, Верифицируемость остаются не параметризованными; то есть нам до конца не известно что именно является отражением этой самой Изолированности, Полноты и Верифицируемости?

В целом это опять же решаемый вопрос, если у Вас в штате имеются "толковые ребята", которые адекватно смогут оценить какую часть системы действительно надо моделировать, а какую нет, во избежание создания избыточных моделей, на разработку которых затрачивается непростительно много времени и часть которых может просто уйти "в стол".

Допустим с полнотой модели Вы как-то разобрались, что дальше?
А дальше переходим к выбору среды моделирования. Здесь, к счастью, все более не менее определено: официальные представители регулятора рекомендуют открытую платформу для верификации и моделирования Rodin в нотации Event-B. Платформа позволяет моделировать и проверять логику работы Вашего ПО, подсвечивая "опасные" участки кода.

Здесь сложности могут возникнуть только с освоением самой среды, потому как все мануалы написаны на английском. Сама среда является довольно мощным инструментом моделирования, имеет ряд особенностей в установке, но с этим также реально разобраться (ссылку на отличное вводное методическое пособие, выпущенное в этом году студентами ИТМО, даю ниже).

Отображение интерфейса Event-B.
Отображение интерфейса Event-B.

Несмотря на то, что Rodin заслуженно стал лидером в решении задач формальной верификации, он не единственный.

Существуют также такие инструменты, как СPN Tools (теория сетей Петри), SPIN (темпоральная логика, автоматы Бюхи), Coq (теория исчисления конструкций), Isabelle (теория логики высшего порядка) и ряд иных менее профильных решений. Все они имеют свои особенности и основаны хоть и на "соседствующих", но все же различных математических теориях.

На этом у меня все. Далее планирую ряд статей, где подробно расскажу о применении математического аппарата, который можно выбрать, если у Вас нет времени разбираться в существующих программных решениях (возможно для кого-то это будет более простой путь решения задачи построения формальных моделей).

И несколько полезных ссылок, которые могут пригодиться:

Комментарии (4)


  1. Gordon01
    23.03.2022 15:08
    #24194955
    -1

    Всегда было очень интересно как можно формально верифицировать код на с/с++

    Много на прошлой работе теоретизировали насчёт это верификации, но до дела так и не добрались.

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


    1. Shaman_RSHU
      24.03.2022 10:04
      #24197273
      -1

      Берется SAST, сертифицированный ФСТЭК. И его отчёт может служить основанием для заключения. То, что SAST всё делает формально - не важно, главное, что у него есть сертификат ФСТЭК.


  1. kovserg
    23.03.2022 19:37
    #24195941

    Как с помощью Event-B доказать корректность Bogosort?


  1. kozlyuk
    24.03.2022 00:49
    #24196615
    +1

    Event-B и подобные — это формальная верификация модели, а не кода. С точки зрения продукта это проверка требований, выраженных в терминах модели, а не того, как они реализованы. Очевиден разрыв между тем, что смоделировано, и кодом, который будет реально пытаться это сделать.

    Полнота модели — это не только не включить лишнее, но и не упустить важное (если мы хотим, чтобы модель была реально полезной). Например, что пользователь не должен быть способен сделать то, на что у него нет прав — очевидный инвариант безопасности в модели контроля доступа. Но вот в системе есть механизм повышения прав (как UAC в Windows). Можно сделать модель как положено: с эффективными и допустимыми правами, с действием повышения прав; инвариант будет, что эффективные права не могут выходить за рамки допустимых. А можно ограничиться текущим набором прав и не выдвигать инварианта, что текущий набор не может стать шире начального, потому что может же легальным образом. Даже если модель все учитывает, можно просто забыть проверит все нужные свойства. В результате к формальному доказательству нужно неформальное пояснение, что мы доказываем и почему (и как — бывают неочевидные преобразования).

    Я делал модель безопасности на Event-B для сертификации ФСТЭК. Делал на совесть и это было очень интересно, но это не помогло найти ошибок и описание не получилось строже и понятнее документации.