AstraVer Toolset » Инструменты дедуктивной верификации моделей политик безопасности

Набор инструментов предназначен для верификации моделей политик безопасности в соответствии с требованиями с ГОСТ Р ИСО/МЭК 15408-3 [1] в части семейства требований доверия «Моделирование политики безопасности» (ADV_SPM).

В настойщий момент разработка моделей ведётся на формальном языке Event-B. Для разработки и верификации моделей используется инструментальная среда, основанная на платформе Rodin, разрабатываемой под свободной лицензией ETH Zurich, Systerel, Clearsy, University of Newcastle и University of Southampton.

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

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

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

[1] ГОСТ Р ИСО/МЭК 15408-3-2013. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности.