Институт системного программирования им. В.П. Иванникова РАН


AstraVer Toolset: инструменты дедуктивной верификации моделей и механизмов защиты ОС

Сбои в программном обеспечении (ПО) ответственных систем, таких как, системы защиты информацией, системы управления самолётом или опасным производством, могут привести к неприятным и даже катастрофическим последствиям. По этой причине разработка такого ПО находится под контролем сертифицирующих органов, которые требуют применения лучших практик, закреплённых в международных стандартах (DO-178С, ISO/IEC 15408 и т.д.).

Например, стандарт ГОСТ Р ИСО/МЭК 15408-3-2013 "Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий" требует, чтобы при разработке наиболее критичного ПО решались следующие задачи:

  • формальное моделирование политики безопасности;
  • формальное доказательство внутренней непротиворечивости модели политики безопасности и недостижимости небезопасных состояний;
  • разработка полуформальной или формальной функциональной спецификации;
  • формальное или полуформальное доказательство соответствия между моделью политики безопасности и функциональной спецификацией;
  • формальное или полуформальное доказательство соответствия между различными представлениями целевого ПО, такими как функциональная спецификация, проект ПО и его реализация.

Для решения этих задач применительно к средствам защиты информации (СЗИ) операционных систем (ОС) в ИСП РАН разработана методика и инструменты дедуктивной верификации моделей и механизмов защиты ОС. Эта методика и инструменты проходили испытания в рамках совместных работ по верификации средств защиты информации в ОС Astra Linux Special Edition, разрабатываемой компанией АО "НПО РусБИТех".

Astraver. Инструменты дедуктивной верификации моделей и механизмов средств защиты информации

Предложенная методика предполагает применение двух нотаций и, соответственно, двух семейств инструментов верификации для моделирования сущностей разных уровней:

  • для формализации политики безопасности СЗИ ОС предлагается использовать язык Event-B;
  • для формализации требований к компонентам реализации СЗИ ОС предлагается использовать язык ACSL.

Event-B и Rodin

Каждая спецификация на Event-B состоит из контекстов и машин. Контексты содержат статическую, неизменяемую часть спецификации: определения констант, множеств и аксиом. Машины содержат динамическую часть: переменные, инварианты, события. Значение переменных формируют текущее состояние спецификации, а инварианты ограничивают его.

События предназначены для модификации текущего состояния определенным образом и при условии определённых ограничений. Каждое событие состоит из параметров, охранных условий (guards), действий (actions). Охранные условия ограничивают значения параметров операции и переменных машины, тем самым уменьшая число состояний, в которых данное событие может случиться. Действия модифицируют текущее состояние за счёт присваивания переменным новых значений. Также Event-B позволяет декомпозировать спецификаций для упрощения их понимания, развития и поддержки с помощью техники пошагового уточнения.

Инварианты на состояние системы позволяют описать как ограничения на внутреннюю согласованность данных, так и формализовать понятие "безопасного" состояния (ГОСТ Р ИСО/МЭК 15408-3-2013, ADV_SPM.1.2C). Спецификации на Event-B разрабатываются и верифицируются с помощью инструментов платформы Rodin, разрабатываемой под свободной лицензией ETH Zurich, Systerel, Clearsy, University of Newcastle и University of Southampton.

Для каждого требующего доказательства случая — однозначность выражений, сохранность инвариантов в результате изменения состояния, корректность проведённого пошагового уточнения — Rodin генерирует соответствующие утверждения. Чтобы полностью верифицировать модель, нужно доказать все сгенерированные утверждения. Для этого Rodin позволяет использовать различные инструменты для автоматического доказательства (например, SMT решатели), а также проводить интерактивное доказательство.

ACSL и AstraVer Toolset

Формальную спецификацию интерфейсов компонентов на языке Си предлагается описывать на специальном языке ACSL (ANSI/ISO C Speci??cation Language). ACSL – это язык спецификации поведения Си-программ, позволяющий записывать контрактные спецификации в диапазоне от наиболее низкоуровневых, таких как «данная функция требует на вход корректно инициализированный указатель на int», до высокоуровневых, например «данная функция требует на вход непустой связный список значений типа int и возвращает наибольшее из этих значений». Мощности языка ACSL достаточно для полной спецификации многих функций, его можно также использовать и для задания частичных спецификаций. Дедуктивная верификация основана на переводе исходного кода на языке Си, аннотированного спецификациями проверяемых свойств, во множество логических формул, общезначимость которых эквивалентна корректности исходной программы в соответствии с заданными свойствами (если при вызове функции было выполнено её предусловие, то функция завершится и её результат будет удовлетворять её постусловию). Эти логические формулы, также известные как условия верификации, могут быть проверены на выполнимость с помощью различных инструментов — автоматических, таких как (Z3, CVC, Alt-Ergo, Vampire, E-Prover и др.), или требующих участия со стороны пользователя, таких как интерактивные средства доказательства теорем Coq и PVS.

Имеющиеся инструменты дедуктивной верификации не поддерживают все возможности языка Си, используемые в ядрах ОС. В связи с этим в ИСП РАН был разработан новый набор инструментов дедуктивной верификации AstraVer Toolset. Набор основан на открытой платформе верификации Си-программ Frama-C (CEA-LIST, Франция) и системе дедуктивной верификации Why3 (INRIA, Франция) и включает в себя следующие новые возможности:

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

Astraver. Инструменты дедуктивной верификации моделей и механизмов средств защиты информации

Страница инструмента

Разработчик/участник

Компиляторные технологии

Перейти к списку всех технологий