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

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

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

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

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

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

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

• для формализации политики безопасности СЗИ ОС предлагается использовать язык 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.

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

Исполнитель

Технологии программирования