Глава 4. Event-B спецификация базового уровня МРОСЛ ДП-модели

Как отмечено в главе 1, компонент доверия ADV_SMP.1 «Формальная модель политики безопасности» требует наличия формальной модели политики безопасности, причем язык представления формальной модели может быть либо математическим, либо формализованным. Базовый уровень МРОСЛ ДП-модели был изложен на математическом языке в главе 3. В данной главе рассматривается перевод базового уровня модели на формализованный язык формального метода Event-B [21], который позволит использовать автоматические и интерактивные инструменты для ее верификации. Глава рассчитана на читателя, который впервые сталкивается с текстом на языке Event-B, так что все основные используемые конструкции будут поясняться по ходу их появления. При желании ознакомиться с Event-B предлагается обратить внимание на Приложение Б либо ознакомиться с официальной документацией [37].

Имеется несколько формальных методов, при помощи которых можно было бы представить МРОСЛ ДП-модель в формализованном виде. Примерами таких методов являются ASM [38], Alloy [39], В [40], Event-B, TLA+ [41], VDM [42], Z [43]. Нами был выбран формальный метод Event-B, так как он отличается простым и понятым языком, спецификации на котором разрабатываются и верифицируются с помощью хорошо апробированной платформы Rodin [44]. Кроме того, Event-B хорошо себя зарекомендовал как средство специфицирования так называемых систем, управляемых событиями (event-driven systems). Так как ОС может рассматриваться как подобная система, то выбор Event-B для специфицирования механизма управления доступом ОС представляется весьма разумным. При этом структура спецификаций на Event-B хорошо соответствует компонентам МРОСЛ ДП-модели, что упрощает задачу перевода модели на данный формализованный язык.

4.1. Формальные спецификации

Под формальной спецификацией некоторой системы далее подразумевается автоматная модель (здесь термины «модель» и «спецификация» используются как синонимы), которая состоит из следующих частей:

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

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

В Event-B каждая спецификация состоит из компонентов двух типов: контекстов и машин (рис. 4.1). Контексты содержат статическую, неизменяемую часть спецификации: определения множеств и констант, а также аксиомы, являющиеся предикатами, в виде которых описываются типы и свойства констант и множеств. Аксиомы принимаются истинными без доказательства.

В отличие от контекстов машины содержат динамическую часть спецификации. Машины имеют доступ к элементам контекста через механизм «видения», что позволяет использовать определенные там константы и множества. В машинах содержатся переменные, инварианты, события. Переменные, как и константы, соответствуют математическим объектам: они могут быть множествами, бинарными отношениями, функциями, числами, принимать значения логического типа и т. д. Значение переменных формируют текущее состояние спецификации, а инварианты — предикаты, определенные на множестве переменных спецификации, — ограничивают его.

Контекст Множества Константы Аксиомы Машина Переменные Инварианты События Другие контексты Другие машины использует использует расширяют уточняют используют

Рис. 4.1. Структура спецификации на Event-B

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

Верификация спецификаций на Event-B осуществляется при помощи формального математического доказательства с использованием включенных в состав платформы Rodin автоматических и интерактивных средств. Интерактивные средства позволяют проводить доказательства вручную, причем их корректность затем проверяется одним из компонентов платформы. Автоматическое же доказательство осуществляется средствами встроенных инструментов, а также SMT-решателями, которые добавляются в Rodin с помощью плагина, входящего в состав AstraVer Toolset. Возможна и комбинация интерактивного и автоматического доказательств, при которой утверждение для доказательства перед подачей на вход автоматическим инструментам сначала вручную разбивается на несколько более простых частных случаев.

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

4.2. Связь элементов МРОСЛ ДП-модели и элементов Event-B спецификации

Основными компонентами МРОСЛ ДП-модели, которые необходимо перевести на формализованный язык Event-B, являются определяемые в ней функции и множества (а также элементы этих множеств), условия консистентности и правила перехода системы из состояния в состояние. Функции и множества определяют множество всех возможных состояний системы G^* , переход между которыми (то есть изменение значений данных функций и множеств) задается соответствующими правилами. Условия и требования формируют свойства, которые должны выполняться в каждом состоянии системы.

Данные компоненты модели хорошо соответствуют конструкциям языка Event-B (рис. 4.2): требования и условия могут быть выражены в виде инвариантов, правила перехода системы из состояния в состояние — в виде событий, а определенные в модели множества и функции — в виде констант, множеств, переменных. Однако из-за особенностей Event-B некоторые компоненты МРОСЛ ДП-модели реализованы в спецификации иначе, а другие не реализованы совсем. Кроме того, в спецификации также присутствуют дополнительные элементы, введенные для упрощения записи некоторых свойств. Причины подобных исключений будут описаны далее в тексте данной главы.

Структуры данных Условия, свойства, требования Состояния Правила переходов системы из состояния в состояние: - параметры; - ограничения на исходное состояние; - ограничения на результирующее состояние Event-B Множества, константы Аксиомы Переменные Инварианты События: - параметры; - охранные условия; - действия

Рис. 4.2. Соответствие между компонентами МРОСЛ ДП-модели и Event-B

4.3. Контекст

Начнем рассмотрение Event-B спецификации базового уровня МРОСЛ ДП-модели с контекста — части спецификации, в которой содержатся неизменяемые в процессе функционирования системы сущности — определения констант, множеств, аксиом.

Первым определенным в контексте элементом является конечное (ключевое слово finite Event-B) множество Union, которое не имеет аналога в модели. Оно служит общим множеством, элементы которого могут быть сущностями, субъект-сессиями, ролями или административными ролями МРОСЛ ДП-модели. Другими словами, множество Union является базовым типом, который имеют элементы упомянутых выше множеств (в некотором смысле это аналог базового класса Object из языков программирования Java, C#):

sets
  Union
axioms
  @UnionIsFinite
    finite(Union)

Каждой аксиоме поставлена в соответствие метка (в данном случае меткой является @UnionIsFinite), которая служит в качестве ее идентификатора. В Event-B метки присутствуют также у инвариантов, охранных условий и действий событий. Мы будем использовать данные метки, чтобы ссылаться на интересующие нас элементы спецификации.

Следующим определяемым множеством является множество Names, которое соответствует множеству возможных имен сущностей, ролей, административных ролей NAMES модели NAMES модели (здесь и далее курсивом отмечаются элементы математической нотации МРОСЛ ДП-модели):

sets
  Names

Множество Accesses соответствует множеству видов прав доступа R_a . Элементы этого множества — это доступ на чтение ReadA ( read_a в модели) и доступ на запись WriteA ( write_a ), выражаемые в виде констант:

Accesses
constants
  ReadA
  WriteA
axioms
  @AccessesPartition
    partition(Accesses, {ReadA}, {WriteA})

Предикат partition(S,x,y) является сокращенной формой записи утверждения, что некоторое множество S состоит из непересекающихся подмножеств x и y:

S = x \cup y x \cap y = \emptyset

То есть вместо одной аксиомы с меткой @AccessesPartition можно было бы написать следующие две аксиомы, которые были бы ей эквивалентны (где \{ReadA\} — множество из одного элемента):

axioms
  @AccessesType1
    Accesses = {ReadA} ∪ {WriteA}
  @AccessesType2
    {ReadA} ∩ {WriteA} = ∅

Множество AccessRights соответствует множеству видов доступа R_r . Элементы этого множества — это право доступа на чтение Read (read_r) , право доступа на запись Write (write_r) , право доступа на выполнение Execute (execute_r) , право доступа владения Own (own_r) :

sets
  AccessRights
constants
  Read
  Write
  Execute
  Own
axioms
  @AccessRightsPartition
    partition(AccessRights, {Read}, {Write}, {Execute}, {Own})

Константа Root соответствует корневой сущности-контейнеру ROOT модели. Данная константа является элементом общего множества Union:

constants
  Root
axioms
  @RootType
    Root ∈ Union

Константа SRoot не имеет прямого аналога в модели. Она соответствует корневой субъект-сессии, т. е. субъект-сессии, которая является первой (или самой верхней) субъект-сессией в иерархии:

constants
  SRoot
axioms
  @SRootType
    SRoot ∈ Union

Константа SpecialAdmRoles соответствует множеству специальных административных ролей SAR. Элементами данного множества являются константы EntitiesAR (административная роль entities_admin_role), SubjectsAR (subjects_admin_role), UsersAR (users_admin_role), RolesAR (roles_admin_role), ARolesAR (admin_roles_admin_role).

constants
  SpecialAdmRoles
  EntitiesAR
  SubjectsAR
  UsersAR
  RolesAR
  ARolesAR
axioms
  @SpecialAdmRolesType
    SpecialAdmRoles ⊆ Union
  @SpecialAdmRolesAreFinite
    finite(SpecialAdmRoles)
  @SpecialAdmRolesContent
    partition(SpecialAdmRoles, {EntitiesAR}, {SubjectsAR}, {UsersAR}, {RolesAR}, {ARolesAR})

Хотя SpecialAdmRoles и является множеством, в спецификации оно объявлено как константа, так как множества (определяемые в блоке sets контекста) в Event-B по определению непересекающиеся и могут рассматриваться как аналоги типов. SpecialAdmRoles не является новым типом — далее можно будет увидеть, что оно является подмножеством множества административных ролей, которые в свою очередь являются подмножеством множества ролей, а множество ролей — подмножеством общего типа Union.

Константа CommonRole описывает общую роль учетных записей пользователей COMMON_ROLE модели:

constants
  CommonRole
axioms
  @CommonRoleType
    CommonRole ∈ Union

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

axioms
  @InductionAxiom
    ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s

4.4. Машина

На этом разбор контекста спецификации завершен. Рассмотрим теперь динамическую часть спецификации, которая в Event-B называется машиной, а именно определенные в ней переменные, инварианты и события.

4.4.1. Переменные и инварианты

Большинство переменных спецификации прямо соответствуют переменным, определенным в МРОСЛ ДП-модели, но кроме них в машине также присутствуют дополнительные переменные, заданные для удобства выражения некоторых свойств. Одной из подобных дополнительных переменных является CurrUnion, которая объединяет все текущие учетные записи пользователей (переменная UserAccs), субъект-сессии (Subjects), сущности (Entities) и роли (Roles) в единое общее множество, которое, в свою очередь, имеет тип Union. Данная переменная позволяет использовать в спецификации множество всех еще не созданных элементов Union. В качестве примера, немного забегая вперед, отметим, что данное множество используется в событии по созданию нового объекта create_object в качестве его типа.

Каждой переменной обязательно соответствует один инвариант, в котором задается ее тип. Прочие инварианты, в тексте которых используется переменная, как правило, описывают ее свойства. Инварианты должны быть выполнены в каждом состоянии системы, и это является одним из основных свойств спецификации, которое требуется доказать на этапе ее верификации. В данном случае инвариант с меткой @CurrUnionType задает тип переменной CurrUnion (подмножество определенного в контексте множества Union), а инвариант с меткой @CurrUnionPartition — ее свойство (множество CurrUnion состоит из четырех непересекающихся подмножеств UserAccs, Subjects, Entities, Roles). При этом второй инвариант также является инвариантом, задающим тип для этих четырех переменных:

variables
  CurrUnion
  UserAccs // U: множество учетных записей пользователей
  Subjects // S: множество субъект-сессий учетных записей
  пользователей
  Entities // E: множество сущностей
  Roles // Общее множество для обычных и административных ролей,
  не имеет прямого аналога в модели
invariants
  @CurrUnionType
    CurrUnion ⊆ Union
  @CurrUnionPartition
    partition(CurrUnion, UserAccs, Subjects, Entities, Roles)

В виде комментариев рядом с именами переменных в секции variables приведены соответствующие им сущности из МРОСЛ ДП-модели.

Множество сущностей Entities состоит из сущностей-объектов (переменная Objects) и сущностей-контейнеров (Containers). Аналогичным образом разделены роли: имеется общее множество ролей Roles, которое состоит из обычных (OrdRoles) и административных ролей (AdmRoles):

variables
  Objects // О: множество объектов
  Containers // С: множество контейнеров
  OrdRoles // R: множество ролей
  AdmRoles // AR: множество административных ролей
invariants
  @EntitiesPartition
    partition(Entities, Objects, Containers)
  @RolesPartition
    partition(Roles, AdmRoles, OrdRoles)

В соответствии с текстом МРОСЛ ДП-модели множества учетных записей пользователей и субъект-сессий должны быть конечными (это учтено еще в контексте в аксиоме с меткой @UnionIsFinite) и непустыми:

invariants
  @UserAccsAreNotEmpty
    UserAccs ≠ ∅
  @SubjectsAreNotEmpty
    Subjects ≠ ∅

Функция Direct ставит в соответствие каждой сущности и роли ее метку (@DirectType), которая может быть прямой (значение TRUE) или косвенной (FALSE).

Для упрощения описания свойств функции Direct для каждой сущности определяется вспомогательная функция EntityMP, ставящая им в соответствие сущность-контейнер, которая называется точкой монтирования (@EntityMPType). Если метка сущности прямая, то ее точкой монтирования является корневой каталог (@Direct1), иначе — сущность-контейнер с прямой меткой (@Direct2), причем точка монтирования должна находиться выше в иерархии сущностей по отношению к ней (@Direct6).

Если метка сущности-контейнера косвенная, то у всех сущностей, содержащихся в этой сущности-контейнере, должна быть косвенная метка (@Direct4). Если у некоторой сущности-контейнера mp метка прямая, а у одной из сущностей, содержащейся в mp, косвенная, то у всех сущностей, содержащихся в mp, метка косвенная (@Direct5), при этом mp является точкой монтирования для всех этих сущностей.

Метка корневого каталога прямая (@Direct7).

Если у роли имеется право доступа к сущности с косвенной меткой, то у нее должно быть такое же право доступа и к точке монтирования этой сущности, и наоборот (@Direct8, @Direct9).

Точкой монтирования сущности с косвенной меткой является либо точка монтирования ее родителя (@Direct10), либо сам родитель (@Direct11).

При этом метка каждой роли является прямой (@Direct12).

variables
  Direct   // direct: функция, задающая метку сущности - прямая или косвенная
  EntityMP // вспомогательная функция, которая для каждой сущности с косвенной меткой ставит в соответствие точку монтирования (mount point)
invariants
  @DirectType
    Direct ∈ Entities ∪ Roles → BOOL
  @EntityMPType
    EntityMP ∈ Entities → Containers
  @Direct1
    ∀e · e ∈ Entities ∧ Direct(e) = TRUE ⇒ EntityMP(e) = Root
  @Direct2
    ∀e · e ∈ Entities ∧ Direct(e) = FALSE ⇒ Direct(EntityMP(e)) = TRUE
  @Direct3
    ∀ c · c ∈ Containers ∧ Direct(c) = FALSE ⇒ c ∉ ran(EntityMP)
  @Direct4
    ∀ e, p · e ∈ dom(EntityNames) ∧ p ∈ dom(EntityNames(e))
      ∧ Direct(p) = FALSE
        ⇒ Direct(e) = FALSE
  @Direct5
    ∀ e, mp · e ∈ dom(EntityNames) ∧ mp ∈ dom(EntityNames(e))
      ∧ Direct(mp) = TRUE ∧ Direct(e) = FALSE
        ⇒ (∀ child · child ∈ dom(EntityNames)
          ∧ mp ∈ dom(EntityNames(child))
            ⇒ Direct(child) = FALSE)
  @Direct6
    ∀ e, p · e ∈ dom(EntityNames) ∧ p ∈ dom(EntityNames(e))
      ∧ Direct(e) = FALSE
        ⇒ (∃  E · E ⊆ Containers ∧ Root ∉ E ∧ Parent[E] ∪ {p} =
          E ∪ {Root} ∧ EntityMP(e) ∈ E ∪ {Root})
  @Direct7
    Direct(Root) = TRUE
  @Direct8
    ∀ e, a, r · e ∈ Entities ∧ Direct(e) = FALSE ∧ r ∈ Roles
      ∧ a ∈ AccessRights ∧ e ↦ a ∈ RoleRights(r)
        ⇒ EntityMP(e) ↦ a ∈ RoleRights(r)
  @Direct9
    ∀ e, a, r · e ∈ Entities ∧ Direct(e) = FALSE ∧ r ∈ Roles
      ∧ a ∈ AccessRights ∧ EntityMP(e) ↦ a ∈ RoleRights(r)
        ⇒ e ↦ a ∈ RoleRights(r)
  @Direct10
    ∀ e, p · e ∈ dom(EntityNames) ∧ p ∈ dom(EntityNames(e))
      ∧ Direct(e) = FALSE ∧ Direct(p) = FALSE
        ⇒ EntityMP(e) = EntityMP(p)
  @Direct11
    ∀ e, p · e ∈ dom(EntityNames) ∧ p ∈ dom(EntityNames(e))
      ∧ Direct(e) = FALSE ∧ Direct(p) = TRUE
        ⇒ EntityMP(e) = p
  @Direct12
    ∀ r · r ∈ Roles ⇒ Direct(r) = TRUE

Функция EntityNames определена для всех сущностей, за исключением корневого каталога, и ставит им в соответствие множество пар вида сущность-контейнер — имя, под которым сущность хранится в данной сущности-контейнере. Множество необходимо для поддержки механизма жестких ссылок: сущности-объекты могут храниться одновременно в нескольких сущностях-контейнерах или же в одной сущности-контейнере с разными именами.

Функция Parent определена для всех сущностей-контейнеров, за исключением корневого каталога, и ставит им в соответствие другую сущность-контейнер, которая находится непосредственно выше в иерархии сущностей, т. е. родительский каталог.

EntityNames должна удовлетворять следующим свойствам, выраженным в виде инвариантов:

  • множество не может быть пустым, так как только у корневого каталога нет соответствующего родительского каталога (инвариант с меткой @EntityNames1);
  • множество, соответствующее сущностям-контейнерам, должно состоять только из одной пары, так как жесткие ссылки на сущности-контейнеры не поддерживаются (@EntityNames2);
  • две разные сущности не могут храниться в одной и той же сущности-контейнере с одинаковым именем (@EntityNames3).

Инварианты с метками @EntityNames4 и @EntityNames5 устанавливают связь между функциями EntityNames и Parent. Без функции Parent вполне можно было бы обойтись, так как вся хранящаяся в ней информация об иерархии сущностей-контейнеров также присутствует и в функции EntityNames, однако функция Parent проще и с ее помощью многие свойства выражаются легче.

Так, функцию Parent удобно использовать для выражения свойства отсутствия циклов в иерархии сущностей: если бы циклы присутствовали, то существовало бы такое множество сущностей-контейнеров, что разность этого множества и множества родительских каталогов этих сущностей была бы пустым множеством. Свойство отсутствия циклов является отрицанием данного утверждения и выражается в инварианте (@NoCyclesForContainers).

variables
  EntityNames // entity_name: функция имен сущностей в составе сущностей-контейнеров
  Parent
invariants
  @EntityNamesType
    EntityNames ∈ Entities ∖ {Root} → (Containers ↔ Names)
  @ParentType
    Parent ∈ Containers ∖ {Root} → Containers
  @EntityNames1
    ∀ e · e ∈ dom(EntityNames) ⇒ EntityNames(e) ≠ ∅
  @EntityNames2
    ∀ c · c ∈ Containers ∧ c ≠ Root
      ⇒ (∃ p, n · p ∈ Containers ∧ n ∈ Names ∧ EntityNames(c) = {p ↦ n})
  @EntityNames3
    ∀ e1, e2 · e1 ∈ dom(EntityNames) ∧ e2 ∈ dom(EntityNames) ∧ e1 ≠ e2
      ⇒ EntityNames(e1) ∩ EntityNames(e2) = ∅
  @EntityNames4
    ∀ c1, c2 · c1 ∈ Containers ∧ c1 ≠ Root ∧ c2 ∈ dom(EntityNames(c1))
      ⇒ c2 = Parent(c1)
  @EntityNames5
    ∀ c1, c2 · c1 ∈ Containers ∧ c1 ≠ Root ∧ c2 = Parent(c1)
      ⇒ c2 ∈ dom(EntityNames(c1))
  @NoCyclesForContainers
    ∀ C · C ⊆ Containers ∧ C ≠ ∅ ∧ Root ∉ C ⇒ C ∖ Parent[C] ≠ ∅

Функция RoleAdmRights ставит в соответствие каждой административной роли множество пар вида роль — право доступа, которое имеет административная роль к данной роли. Данная функция имеет следующие свойства, выраженные в виде инвариантов:

  • каждая административная роль имеет право доступа на выполнение к любой существующей роли (@ExecuteToEverything);
  • специальная административная роль RolesAR является владельцем для каждой обычной роли (@RolesAR1), причем она является единственным владельцем (@RolesAR2);
  • специальная административная роль ARolesAR является владельцем для каждой административной роли (@ARolesAR1), причем она является единственным владельцем (@ARolesAR2);
  • если административная роль обладает правом доступа на чтение к роли, то она обладает правом доступа на чтение и ко всем ролям ниже в ее иерархии (@ReadSpreads).
variables
  RoleAdmRights // APA: функция административных прав доступа
  к ролям и административным ролям административных ролей
invariants
  @RoleAdmRightsType
    RoleAdmRights ∈ AdmRoles → (Roles ↔ AccessRights)
  @ExecuteToEverything
    ∀ ar, r · ar ∈ AdmRoles ∧ r ∈ Roles
      ⇒ r ↦ Execute ∈ RoleAdmRights(ar)
  @RolesAR1
    ∀ r · r ∈ OrdRoles
      ⇒ r ↦ Own ∈ RoleAdmRights(RolesAR)
  @RolesAR2
    ∀ r, ar · r ∈ OrdRoles ∧ ar ∈ AdmRoles
      ∧ r ↦ Own ∈ RoleAdmRights(ar)
        ⇒ ar = RolesAR
  @ARolesAR1
    ∀ r · r ∈ AdmRoles
      ⇒ r ↦ Own ∈ RoleAdmRights(ARolesAR)
  @ARolesAR2
    ∀ r, ar · r ∈ AdmRoles ∧ ar ∈ AdmRoles
      ∧ r ↦ Own ∈ RoleAdmRights(ar)
        ⇒ ar = ARolesAR
  @ReadSpreads
    ∀ ar, r, p · ar ∈ AdmRoles ∧ r ∈ Roles
      ∧ p ∈ Roles ∧ p ∈ RParents(r)
      ∧ p ↦ Read ∈ RoleAdmRights(ar)
        ⇒ r ↦ Read ∈ RoleAdmRights(ar)

Функция RoleName определена для всех ролей и ставит им в соответствие их имя. Данное имя должно быть уникально: не должно существовать двух различных ролей с одинаковым именем, так что в Event-B данная функция определена как тотальная инъекция (символ \mapsto ). Совместно с функцией RParents функция RoleName реализует функцию МРОСЛ ДП-модели role_name: функцию имен ролей и административных ролей в составе роли или административной роли.

variables
  RoleName
invariants
  @RoleNameType
    RoleName ∈ Roles ↣ Names

Функция RoleRights ставит в соответствие для каждой роли множество пар вида сущность — право доступа, которое имеет роль к данной сущности. С переменной RoleRights связано следующее свойство: у каждой сущности может быть только одна роль-владелец:

variables
  RoleRights // PA: функция прав доступа к сущностям ролей и административных ролей
invariants
  @RoleRightsType
    RoleRights ∈ Roles → (Entities ↔ AccessRights)
  @NoMultipleOwners
    ∀ r1, r2, e · r1 ∈ Roles ∧ r2 ∈ Roles ∧ e ↦ Own ∈ RoleRights(r1)
      ∧ e ↦ Own ∈ RoleRights(r2)
        ⇒ r1 = r2

Константа Root, соответствующая корневому каталогу, является элементом множества текущих сущностей-контейнеров:

invariants
  @RootType
    Root ∈ Containers

Функция RParents определена для всех ролей и ставит им в соответствие множество родительских ролей, в которых они непосредственно содержатся. Множество необходимо по той причине, что одна роль может одновременно содержаться в нескольких других ролях. Не у всех ролей есть родительская роль, так что поставленное в соответствие множество может быть пустым. С переменной RParents связаны следующие инварианты:

  • иерархии обычный ролей и административных ролей независимы (@RParents1 и @RParents2);
  • в иерархии ролей нет циклов (@NoCyclesForRoles).
variables
  RParents
invariants
  @RParentsType
    RParents ∈ Roles → ℙ(Roles)
  @RParents1
    ∀r · r ∈ AdmRoles ⇒ RParents(r) ⊆ AdmRoles
  @RParents2
    ∀r · r ∈ OrdRoles ⇒ RParents(r) ⊆ OrdRoles
  @NoCyclesForRoles
    ∀R · R ⊆ Roles ∧ R ≠ ∅ ⇒ (∃r · r ∈ R ∧ (∀p · p ∈ R ⇒ p ∉ RParents(r)))

Функция Shared определена на множествах сущностей-контейнеров и субъект-сессий и задает, являются ли элементы этих множеств разделяемыми контейнерами. Если бы множества Containers и Roles не были бы подмножествами общего множества-типа Union, определенного в контексте, то Event-B не позволил бы использовать в записи инварианта операцию объединения этих множеств. Каждая роль должна являться разделяемым контейнером:

variables
  Shared // shared_container: функция разделяемых записей контейнеров
invariants
  @SharedType
    Shared ∈ Containers ∪ Roles → BOOL
  @RolesAreShared
    ∀r · r ∈ Roles ⇒ Shared(r) = TRUE

Функция SParent определена для всех субъект-сессий, за исключением корневой сессии, и ставит им в соответствие другую субъект-сессию, которая находится непосредственно выше в иерархии субъект-сессий. Также на иерархии субъект-сессий должны отсутствовать циклы:

variables
  SParent
invariants
  @SParentType
    SParent ∈ Subjects ∖ {SRoot} → Subjects
  @NoCyclesForSubjects
    ∀S · S ⊆ dom(SParent) ∧ S ≠ ∅ ⇒ S ∖ SParent[S] ≠ ∅

Определенное в контексте в виде константы множество Special-AdmRoles должно быть подмножеством множества административных ролей:

invariants
  @SpecialAdmRolesType
    SpecialAdmRoles ⊆ AdmRoles

Константа SRoot, в свою очередь, является элементом множества текущих субъект-сессий:

invariants
  @SRootType
    SRoot ∈ Subjects

Функция SubjectAccesses описывает доступы субъект-сессий к сущностям: для каждой субъект-сессии ставится в соответствие множество упорядоченных пар вида сущность — доступ, который субъект-сессия имеет к данной сущности:

variables
  SubjectAccesses   // A: функция доступов субъект-сессий к сущностям
invariants
  @SubjectAccessesType
    SubjectAccesses ∈ Subjects → (Entities ↔ Accesses)

Функция SubjectAdmAccesses описывает доступы субъект-сессий к ролям: для каждой субъект-сессии ставится в соответствие множество упорядоченных пар вида роль — доступ, который субъект-сессия имеет к данной роли:

variables
  SubjectAdmAccesses   // AA: функция доступов субъект-сессий к ролям или административным ролям
invariants
  @SubjectAdmAccessesType
    SubjectAdmAccesses ∈ Subjects → (Roles ↔ Accesses)

Частичная функция SubjectOwner ставит в соответствие для некоторых субъект-сессий роль, которая имеет право доступа владения к данной сессии. Функция определена не для всех субъект-сессий, так как не у каждой субъект-сессии есть владелец:

variables
  SubjectOwner   // PA: частный случай функции PA, только для сессий и правда доступа владения
invariants
  @SubjectOwnerType
    SubjectOwner ∈ Subjects ⇸ Roles

Функция SubjectUser ставит в соответствие каждой субъект-сессии учетную запись пользователя, от имени которой она действует:

variables
  SubjectUser   // user: функция принадлежности субъект-сессии учетной записи пользователя
invariants
  @SubjectUserType
    SubjectUser ∈ Subjects → UserAccs

Функции UserAdmRole и UserOrdRole определены для каждой учетной записи пользователя и ставят им в соответствие индивидуальную административную роль и индивидуальную обычную роль соответственно (@UserAdmRoleType, @UserOrdRoleType). Индивидуальные роли пользователя должны содержаться в иерархии ролей независимо, т. е. у них не должно быть ни родителей, ни потомков (@UserAdmRole1, @UserAdmRole2, @UserOrdRole1, @UserOrdRole2). Одна роль не может быть индивидуальной ролью сразу нескольких учетных записей пользователей (@UserAdmRole3, @UserOrdRole3). Индивидуальная административная роль пользователя не должна быть специальной административной ролью (@UserAdmRole4). Кроме того, индивидуальная административная роль учетной записи пользователя должна обладать правами доступа на чтение и на запись как к самой себе, так и к индивидуальной обычной роли учетной записи пользователя (@UserAdmRole5, @UserAdmRole6, @UserOrdRole4, @UserOrdRole5).

variables
  UserAdmRole   // u_admin: индивидуальная административная роль учетной записи пользователя
  UserOrdRole   // u_c: индивидуальная роль учетной записи пользователя
invariants
  @UserAdmRoleType
    UserAdmRole ∈ UserAccs → AdmRoles
  @UserOrdRoleType
    UserOrdRole ∈ UserAccs → OrdRoles
  @UserAdmRole1
    ∀ u · u ∈ UserAccs ⇒ RParents(UserAdmRole(u)) = ∅
  @UserAdmRole2
    ∀  u,  r · u ∈ UserAccs ∧ r ∈ Roles ⇒ UserAdmRole(u) ∉ RParents(r)
  @UserAdmRole3
    ∀   u1,   u2 · u1 ∈ UserAccs   ∧   u2 ∈ UserAccs   ∧   u1 ≠ u2
      ⇒ UserAdmRole(u1) ≠ UserAdmRole(u2)
  @UserAdmRole4
    ∀  u · u ∈ UserAccs ⇒ UserAdmRole(u) ∉ SpecialAdmRoles
  @UserAdmRole5
    ∀ u · u ∈ UserAccs
      ⇒ UserAdmRole(u) ↦ Read ∈ RoleAdmRights(UserAdmRole(u))
  @UserAdmRole6
    ∀  u · u ∈ UserAccs
      ⇒ UserAdmRole(u) ↦ Write ∈ RoleAdmRights(UserAdmRole(u))
  @UserOrdRole1
    ∀ u · u ∈ UserAccs ⇒ RParents(UserOrdRole(u)) = ∅
  @UserOrdRole2
    ∀ u, r · u ∈ UserAccs ∧ r ∈ Roles ⇒ UserOrdRole(u) ∉ RParents(r)
  @UserOrdRole3
    ∀ u1, u2 · u1 ∈ UserAccs ∧ u2 ∈ UserAccs ∧ u1 ≠ u2
      ⇒ UserOrdRole(u1) ≠ UserOrdRole(u2)
  @UserOrdRole4
    ∀ u · u ∈ UserAccs
      ⇒ UserOrdRole(u) ↦ Read ∈ RoleAdmRights(UserAdmRole(u))
  @UserOrdRole5
    ∀  u · u ∈ UserAccs
      ⇒ UserOrdRole(u) ↦ Write ∈ RoleAdmRights(UserAdmRole(u))

Общая роль CommonRole является обычной ролью (@CommonRoleType). Общая роль находится в иерархии ролей независимо от прочих ролей (@CommonRole1, @CommonRole2). Общая роль не может быть индивидуальной ролью какой-либо учетной записи пользователя (@CommonRole3). Кроме того, индивидуальная административная роль каждой учетной записи пользователя должна обладать правами доступа на чтение и на запись к общей роли CommonRole (@CommonRole4, @CommonRole5).

invariants
  @CommonRoleType
    CommonRole ∈ OrdRoles
  @CommonRole1
    RParents(CommonRole) = ∅
  @CommonRole2
    ∀ r · r ∈ Roles ⇒ CommonRole ∉ RParents(r)
  @CommonRole3
    ∀ u · u ∈ UserAccs ⇒ CommonRole ≠ UserOrdRole(u)
  @CommonRole4
    ∀ u · u ∈ UserAccs
      ⇒ CommonRole ↦ Read ∈ RoleAdmRights(UserAdmRole(u))
  @CommonRole5
    ∀ u · u ∈ UserAccs
      ⇒ CommonRole ↦ Write ∈ RoleAdmRights(UserAdmRole(u))

4.4.2. Событие инициализации

В Event-B достижимыми называются состояния, в которых система может оказаться при переходах из некоторого начального состояния в результате выполнения произвольных последовательностей описанных в спецификации событий. Начальное состояние при этом задается событием инициализации. В спецификации базового уровня МРОСЛ ДП-модели событие инициализации на данный момент не реализовано. Поэтому для подтверждения корректности спецификации вместо доказательства сохранности инвариантов в каждом достижимом состоянии проводится доказательство сохранности инвариантов при каждом переходе от одного возможного состояния к другому возможному, где под возможным состоянием подразумевается любое состояние, при котором определенные в спецификации инварианты были бы выполнены.

4.4.3. Реализация правила перехода системы из состояния в состояние в виде события

Рассмотрим пример реализации одного из правил перехода системы из состояния в состояние МРОСЛ ДП-модели в виде Event-B события — правила delete\_subject (табл. 4.1).

Таблица 4.1. Правило перехода системы из состояния в состояние delete_subject

Исходное состояние G

Результирующее состояние G'

delete_subject(x, z)

Исходное состояние G:

  1. x, z \in S;
  2. H_{S}(z) = \emptyset;
  3. существует r \in R \cup AR: (x, r, read_{a}) \in AA, (z, own_{r}) \in PA(r).

Результирующее состояние G':

  1. S' = S \setminus \{z\};
  2. AA' = AA \setminus \{(z, r, \alpha_{a}): r \in R \cup AR, \alpha_{a} \in R_{a}\};
  3. A' = A \setminus \{(z, e, \alpha_{a}): e \in E, \alpha_{a} \in R_{a}\};
  4. для r \in R \cup AR выполняется PA'(r) = PA(r) \setminus \{(z, own_{r})\};
  5. для z' \in S такой, что z \in H_{S}(z'), справедливо равенство H_{S}'(z') = H_{S}(z') \setminus \{z\}.

Правило delete_subject обладает двумя параметрами (x и z), пронумерованным множеством предусловий (левая часть таблицы) и пронумерованным множеством постусловий (правая часть таблицы). События Event-B устроены схожим образом: событие может иметь параметры, блок охранных условий (аналог предусловий) и блок действий, в котором осуществляется изменение значений определенных в спецификации переменных.

Второе предусловие требует отсутствия у удаляемой субъект-сессии z потомков в иерархии субъект-сессий (в противном случае удаление надо начинать с них). На Event-B спецификации иерархия субъект-сессий реализована обратной функцией SParent, так что соответствующее условие @grd4 требует, чтобы удаляемая субъект-сессия delSubject не являлась родителем ни для какой другой субъект-сессии.

Третье предусловие требует наличия у субъект-сессии x доступа на чтение к роли с правом доступа владения к удаляемой субъект-сессии z. На Event-B спецификации права доступа владения к субъект-сессиям реализуются отдельной частичной функцией Subject-Owner. Так как функция частичная, то требование существования роли-владельца сводится к требованию принадлежности субъект-сессии к ее множеству определения (охранное условие @grd5). Требование наличия доступа на чтение выражается в условии @grd6.

В правиле перехода системы из состояния в состояние delete\_subject также присутствует пять постусловий, которые описывают удаление всякого упоминания субъект-сессии z из переменных состояния. Первому постусловию соответствуют действия события с метками @act1 и @act2 (все элементы множества Subjects также являются элементами общего множества CurrUnion, которого нет в МРОСЛ ДП-модели). Второе и третье постусловия описывают удаление всех доступов, которые имела удаляемая субъект-сессия к ролям и сущностям — @act4 и @act6. Удаление информации о роли-владельце из четвертого постусловия осуществляется в действии @act5. Обновление иерархии субъект-сессий из пятого постусловия — в @act6.

Необъясненным осталось только охранное условие с меткой @grd3, которое требует, чтобы удаляемая субъект-сессия не была корневой субъект-сессией. Понятие корневой субъект-сессии отсутствует в МРОСЛ ДП-модели, оно было добавлено в Event-B спецификацию исключительно для облегчения выражения некоторых связанных с иерархией субъект-сессий свойств.

event delete_subject
  any subject delSubject
  where
    @grd1 subject ∈ Subjects
    @grd2 delSubject ∈ Subjects
    @grd3 delSubject ≠ SRoot
    @grd4 ∀ s · s ∈ dom(SParent) ⇒ SParent(s) ≠ delSubject
    @grd5 delSubject ∈ dom(SubjectOwner)
    @grd6 SubjectOwner(delSubject) ↦ ReadA ∈ SubjectAdmAccesses(subject)
  then
    @act1 CurrUnion := CurrUnion ∖ {delSubject}
    @act2 Subjects := Subjects ∖ {delSubject}
    @act3 SubjectUser := {delSubject} ⩤ SubjectUser
    @act4 SubjectAccesses := {delSubject} ⩤ SubjectAccesses
    @act5 SubjectOwner := {delSubject} ⩤ SubjectOwner
    @act6 SubjectAdmAccesses := {delSubject} ⩤ SubjectAdmAccesses
    @act7 SParent := {delSubject} ⩤ SParent
end

4.4.4. Использование вспомогательных параметров

Предусловия и постусловия правила перехода системы из состояния в состояние МРОСЛ ДП-модели delete\_subject достаточно просты и транслируются на Event-B без заметных изменений. Однако ситуация обстоит несколько иначе с некоторыми другими правилами. Рассмотрим пример правила перехода системы из состояния в состояние create\_object (табл. 4.2).

Таблица 4.2. Правило перехода системы из состояния в состояние create_object

Исходное состояние G

Результирующее состояние G'

create_object(x, y, yd, name, z)

Исходное состояние G:

  1. x \in S;
  2. y \notin E;
  3. z \in C;
  4. [(x, z, write_{a}) \in A, существует r \in R \cup AR такая, что (x, r, read_{a}) \in AA и (z, execute_{r}) \in PA(r)];
  5. name \in NAME \setminus (\{“”\} \cup \{entity\_name(z, y'): y' \in H_{E}(z)\});
  6. (x, user(x)\_c, write_{a}) \in AA;
  7. H_{E}(z) = \{y' \in H_{E}(z): direct(y') = yd\};
  8. [если yd = true, то direct(z) = true].

Результирующее состояние G':

  1. E' = E \cup \{y\} (O' = O \cup \{y\}, C' = C);
  2. entity\_name'(z, y) = \{name\};
  3. direct'(y) = yd;
  4. если yd = true, то PA'(user(x)\_c) = PA(user(x)\_c) \cup \{(y, own_{r})\}; если yd = false и c \in C такая, что direct(c) = true, H_{E}(c) = \{y' \in H_{E}(y): direct(y') = false\} и y < c, то для всех r' \in R \cup AR выполняется PA'(r') = PA(r') \cup \{(y, \alpha_{rj}): (c, \alpha_{rj}) \in PA(r')\};
  5. H_{E}'(z) = H_{E}(z) \cup \{y\}, H_{E}'(y) = \emptyset.

Постусловие номер 4 правила create\_object описывает изменение функции PA. Данное описание включает в себя большое число различных условий и достаточно сложно, чтобы его можно было выразить в виде действий Event-B события, которые в основном выглядят как простые присваивания. Существует два способа решения данной проблемы. Первый — использование нотации задания множества вида \{x \mid P\} , с помощью которой можно задать множество, состоящее из всех элементов x, удовлетворяющих предикату P. Пример использования — присваивание переменной S множества, состоящего из всех таких элементов x, которые либо принадлежат множеству A, либо множеству B:

S := \{ x \mid x \in A \lor x \in B \}.

В данном конкретном случае можно было вполне обойтись без нотации задания множества и напрямую присвоить переменной S объединение множеств A и B:

S := A \cup B.

В случае с четвертым постусловием правила create\_object подобной простой альтернативы нет, а предикат P будет заметно сложней: на самом деле он станет настолько сложным, что в нем будет весьма затруднительно разобраться, и особенно заметно усложнится процесс доказательства сохранности инвариантов, в которых присутствует измененная переменная.

Второй способ заключается в объявлении вспомогательного параметра события, значение которого присваивается нужной переменной в виде действия Event-B события. При этом в виде охранных условий на значение объявленного параметра описываются свойства, которым должно соответствовать новое значение переменной, а также связь между текущим и новым значениями. В данном способе единый предикат P, о котором шла речь выше, разбивается на отдельные охранные условия, работать с которыми становится проще.

Второй способ хорошо себя зарекомендовал и широко применяется в Event-B спецификации МРОСЛ ДП-модели. Рассмотрим его на примере параметра roleRights события create\_object , который был добавлен для описания постусловия номер 4 правила create\_object .

Охранное условие с меткой @grd17 задает тип параметра. Так как значение параметра впоследствии будет присвоено переменной RoleRights в действии @act5, то задаваемый тип должен соответствовать типу переменной. Тип переменной RoleRights — функция, ставящая в соответствие для каждой роли множество пар вида сущность — право доступа. Так как в результате выполнения события

create_object множество сущностей Entities изменится — в него добавится только что созданный объект, а множество сущностей Entities присутствует в описании типа переменной RoleRights, то в описании типа параметра roleRights нужно учесть данное изменение: вместо множества Entities использовать его новое значение, а именно объединение множества Entities и создаваемого объекта object. Все это учтено в задающем тип параметра охранном условии @grd17.

Все изменения переменной RoleRights, описанные в постусловии номер 4, касаются добавления некоторым ролям прав доступа к создаваемому объекту object. Данные изменения выражаются в виде охранных условий @grd19-21 на параметр roleRights.

Права доступа ко всем сущностям, за исключением объекта object, имеющиеся у ролей на момент до события create_object, должны остаться неизменны после присваивания переменной RoleRights значения параметра roleRights. Данная связь описывается в охранном условии @grd18.

В действии @act5 происходит присваивание переменной Role-Rights значения параметра roleRights, который был подробно описан в охранных условиях.

event create_object
  any subject object parent name role dLabel mountPoint roleRights depth
  where
    @grd1 object ∈ Union ∖ CurrUnion
    @grd2 subject ∈ Subjects
    @grd3 parent ∈ Containers
    @grd4 parent ↦ WriteA ∈ SubjectAccesses(subject)
    @grd5 ∃ r · r ∈ Roles ∧ r ↦ ReadA ∈ SubjectAdmAccesses(subject)
      ∧ parent ↦ Execute ∈ RoleRights(r)
    @grd6 name ∈ Names
    @grd7 ∀ e · e ∈ dom(EntityNames)
      ⇒ parent ↦ name ∉ EntityNames(e)
    @grd8 role = UserOrdRole(SubjectUser(subject))
    @grd9 role ↦ WriteA ∈ SubjectAdmAccesses(subject)
    @grd10 mountPoint ∈ Containers
    @grd11 dLabel ∈ BOOL
    @grd12 ∀ e · e ∈ dom(EntityNames) ∧ parent ∈ dom(EntityNames(e))
      ⇒ Direct(e) = dLabel
    @grd13 dLabel = TRUE ⇒ Direct(parent) = TRUE
    @grd14 dLabel = TRUE ⇒ mountPoint = Root
    @grd15 dLabel = FALSE ∧ Direct(parent) = FALSE
      ⇒ mountPoint = EntityMP(parent)
    @grd16 dLabel = FALSE ∧ Direct(parent) = TRUE
      ⇒ mountPoint = parent
    @grd17 roleRights ∈ Roles → (Entities ∪ {object} ↔ AccessRights)
    @grd18 ∀ e, a, r · e ∈ Entities ∧ a ∈ AccessRights ∧ r ∈ Roles
      ⇒ (e ↦ a ∈ roleRights(r) ↔ e ↦ a ∈ RoleRights(r))
    @grd19 dLabel = TRUE ⇒ object ↦ Own ∈ roleRights(role)
    @grd20 dLabel = TRUE
      ⇒ (∀ a, r · a ∈ AccessRights ∧ r ∈ Roles
        ∧ object ↦ a ∈ roleRights(r)
          ⇒ a = Own ∧ r = role)
    @grd21 dLabel = FALSE
      ⇒ (∀ a, r · a ∈ AccessRights ∧ r ∈ Roles
        ⇒ (mountPoint ↦ a ∈ RoleRights(r)
          ⇔ object ↦ a ∈ roleRights(r)))
    @grd22 depth ∈ ℕ → ℙ(Containers)
    @grd23 ∀ c · c ∈ Containers ⇒ (∃ i · i ∈ ℕ ∧ c ∈ depth(i))
    @grd24 depth(0) = {Root}
    @grd25 ∀ i · i ∈ ℕ ∧ i ≠ 0 ⇒ (∀ c · c ∈ depth(i) ⇒ c ≠ Root)
    @grd26 ∀ i · i ∈ ℕ
      ⇒ (∀ c · c ∈ depth(i + 1)
        ⇒ (∃ p · p ∈ depth(i) ∧ p = Parent(c)))
    theorem @grd27
      ∀ i · i ∈ ℕ ∧ (∀ c · c ∈ depth(i)
        ⇒ (∃ E · E ⊆ Containers ∧ Root ∉ E ∧ Parent[E] ∪ {c} = E ∪ {Root}))
          ⇒ (∀ c · c ∈ depth(i + 1)
            ⇒ (∃ E · E ⊆ Containers ∧ Root ∉ E ∧ Parent[E] ∪ {c} = E ∪ {Root}))
    theorem @grd28
      ∀ i · i ∈ ℕ ⇒ (∀ c · c ∈ depth(i)
        ⇒ (∃ E · E ⊆ Containers ∧ Root ∉ E ∧ Parent[E] ∪ {c} = E ∪ {Root}))
  then
    @act1 CurrUnion := CurrUnion ∪ {object}
    @act2 Entities := Entities ∪ {object}
    @act3 Objects := Objects ∪ {object}
    @act4 EntityNames(object) := {parent ↦ name}
    @act5 RoleRights := roleRights
    @act6 Direct(object) := dLabel
    @act7 EntityMP(object) := mountPoint
end

4.4.5. Использование математической индукции

При доказательстве сохранности инвариантов иногда требуется использовать пятую аксиому Пеано натуральных чисел, а именно аксиому индукции: если какое-либо предложение доказано для 0 (база индукции) и если из допущения, что оно верно для натурального числа п, вытекает, что оно верно для следующего за п натурального числа (индукционное предположение), то это предложение верно для всех натуральных чисел. Рассмотрим использование доказательства по индукции в Event-B на примере события create_object.

Для доказательства сохранности одного из инвариантов для события create\_object потребовалось использовать следующее свойство: для каждой сущности-контейнера существует путь до корневого каталога. На Event-B данное свойство можно выразить так: для каждой сущности-контейнера c существует множество сущностей-контейнеров E (которое и задает требуемый путь), не включающее в себя корневой каталог, такое, что множество непосредственных родителей в иерархии сущностей для всех сущностей-контейнеров из множества E в объединении с сущностью-контейнером c равно объединению множества E и корневого каталога Root:

\forall c \cdot c \in Containers \Rightarrow (\exists E \cdot E \subseteq Containers \land Root \notin E \land Parent[E] \cup \{c\} = E \cup \{Root\})

Рассмотрим данное свойство с помощью рис. 4.3 на примере пути от сущности-контейнера c до корневого каталога. Тогда множество E, которое будет соответствовать данному пути, будет состоять из элементов \{x,p,c\} . Множество непосредственных родителей в иерархии сущностей для всех сущностей-контейнеров из множества E, выражаемое в виде \mathit{Parent}(E) , можно вычислить следующим образом:

Root x … y p … c Root x p c E Parent[E]

Рис. 4.3. Путь до корневого каталога от сущности-контейнера с

— глубина 0 — глубина 1 — глубина 2 — глубина 3 Root x … y p … c

Рис. 4.4. Глубина сущностей-контейнеров в иерархии сущностей

Parent[E] = Parent(x) \cup Parent(p) \cup Parent(c) = \{Root\} \cup \{x\} \cup \{p\}

Выбранное нами множество E действительно удовлетворяет свойству

Parent[E] \cup \{c\} = \{x, p, c\} \cup \{Root\},

так как

\{Root,x,p\} \cup \{c\} = \{x,p,c\} \cup \{Root\}.

Однако если бы мы выбрали для сущности-контейнера c другое множество E, например включающее в себя сущность-контейнер y, то данное свойство уже бы не выполнялось, что означало бы, что данное множество не является отображением пути до корневого каталога.

Чтобы использовать данное свойство, его нужно сначала доказать. Для этого можно использовать математическую индукцию: поставим в соответствие для каждой сущности-контейнера ее глубину (наибольшую длину пути от корневого каталога до данной сущности-контейнера) (рис. 4.4). Тогда базе индукции будет соответствовать сам корневой каталог, а свойство существования пути до корневого каталога будет доказано следующим образом: пусть c=Root, тогда нужно найти такое E, что

\exists E \cdot E \subseteq Containers \land Root \notin E \land Parent[E] \cup \{Root\} = E \cup \{Root\}

Таким E является \varnothing . Проверим это:

\varnothing \subseteq Containers \land Root \notin \varnothing \land Parent[\varnothing] \cup \{Root\} = \varnothing \cup \{Root\}

Первые два конъюнкта очевидно истинны. Так как Parent[\varnothing] = \varnothing , то третий конъюнкт на самом деле является тождеством. База индукции доказана.

Далее следует доказать индукционное предположение: при условии существовании пути до корневого каталога от любой сущности-контейнера, расположенной на глубине i, доказать, что существует путь до корневого каталога любой сущности-контейнера, расположенной на глубине i+1. Это достаточно просто: выберем случайную сущность-контейнер, расположенную на глубине i+1, и назовем ее c. По определению используемой нами функции глубины, у каждой сущности на глубине i+1 существует родительская сущность контейнер, расположенная на глубине i, — назовем ее p. Из первой части индукционного предположения известно, что для любой сущности-контейнера на глубине i существует путь до корневого каталога, назовем этот путь E. Тогда требуемый для доказательства путь до корневого каталога от сущности-контейнера для глубине i+1 будет E \cup \{p\} .

Теперь перенесем данные рассуждения на событие create_object на Event-B. Объявим функцию глубины как дополнительный параметр события depth. В охранном условии @grd22 зададим тип данного параметра: функция, ставящая для каждого натурального числа (собственно глубины) множество сущностей-контейнеров, которые находятся на данной глубине. Последующие охранные условия описывают функцию глубины более полным образом:

  • атрибут глубины должен быть у каждой сущности-контейнера (@grd23);
  • на нулевой глубине должен находиться только корневой каталог (@grd24);
  • корневой каталог не может находиться на глубине отличной от 0 (@grd25);
  • для любой сущности-контейнера на глубине i+1 существует сущность-контейнер на глубине i, которая является его родителем (@grd26).

Используя функцию глубины, можно задать индукционное предположение в виде теоремы @grd27: если существует путь до корневого каталога от любой сущности-контейнера на глубине i, то существует и для любой сущности-контейнера на глубине i+1. Данную теорему нужно доказать (мы это уже сделали неформальным образом выше), а затем совместно с базой индукции @grd24 использовать для доказательства исходного свойства существования пути до корневого каталога для любой сущности-контейнера, которое мы выразили в виде теоремы @grd28. Аналогичным образом выполняется доказательство по индукции еще для нескольких событий в спецификации МРОСЛ ДП-модели.

4.4.6. Разделение правила перехода системы из состояния в состояние на несколько событий

Следующее, о чем целесообразно упомянуть в контексте различий между МРОСЛ ДП-моделью и ее спецификацией на Event-B, это разделение некоторых правил перехода системы из состояния в состояние на два и более события. Данное действие требуется обычно в случаях, когда правило описывает логически общее действие — например, получение доступа на чтение — но направленное на разные объекты — например, доступ на чтение к сущности или роли. Рассмотрим правило перехода системы из состояния в состояние access_read (табл. 4.3).

Таблица 4.3. Правило перехода системы из состояния в состояние access_read

Исходное состояние G

Результирующее состояние G'

access_read(x, y)

Исходное состояние G:

  1. x \in S;
  2. y \in E \cup R \cup AR;
  3. существует r \in R \cup AR: (x, r, read_{a}) \in AA, [если y \in E, то (y, read_{r}) \in PA(r) и существует контейнер c \in C такой, что execute\_container(x, c, y) = true]; [если y \in R \cup AR, то (y, read_{r}) \in APA(r)].

Результирующее состояние G':

  1. если y \in E, то A' = A \cup \{(x, y, read_{a})\}, AA' = AA;
  2. если y \in R \cup AR, то AA' = AA \cup \{(x, y, read_{a})\}, A' = A.

Параметр y может быть как сущностью, так и ролью, и в зависимости от этого различаются пред- и постусловия правила. В принципе, это не препятствует прямому их переносу на Event-B, однако итоговое событие получится неоправданно усложненным. Вместо этого предлагается в данном случае разбить одно событие на два независимых, каждое из которых будет описывать отдельный частный случай — получение доступа к сущности (событие access\_read\_entity ) и получение доступа к роли (событие access\_read\_entity ):

event access_read_entity
  any subject entity
  where
    @grd1 subject ∈ Subjects
    @grd2 entity ∈ Entities
    @grd3 ∃ r · r ∈ Roles ∧ r ↦ ReadA ∈ SubjectAdmAccesses(subject)
      ∧ entity ↦ Read ∈ RoleRights(r)
    @grd4 ∃ E, c · E ⊆ Containers ∧ Root ∉ E
      ∧ ((entity ∈ dom(EntityNames) ∧ c ∈ dom(EntityNames(entity))
      ∧ Parent[E] ∪ {c} = E ∪ {Root}) ∨ (E = ∅ ∧ entity = Root))
        ∧ (∀ o · o ∈ E ∪ {entity} ∪ {Root} ⇒ (∃ r · r ∈ Roles
          ∧ r ↦ ReadA ∈ SubjectAdmAccesses(subject)
          ∧ o ↦ Execute ∈ RoleRights(r)))
  then
    @act1 SubjectAccesses(subject) := SubjectAccesses(subject)
      ∪ {entity ↦ ReadA}
end
event access_read_role
  any subject role
  where
    @grd1 subject ∈ Subjects
    @grd2 role ∈ Roles
    @grd3 ∃ r · r ∈ AdmRoles ∧ role ↦ ReadA ∈ RoleAdmRights(r)
      ∧ r ↦ Read ∈ SubjectAdmAccesses(subject)
  then
    @act1 SubjectAdmAccesses(subject) := SubjectAdmAccesses
      (subject) ∪ {role ↦ ReadA}
end

4.4.7. Отсутствующие в спецификации элементы МРОСЛ ДП-модели

В тексте МРОСЛ ДП-модели приводится определение функции значений сущностей, ролей и административных ролей V, задающей возможность для каждой из них принимать значение любой конечной последовательности бит. Значение данной функции изменяется исключительно в следующих правилах перехода системы из состояния в состояние: get_user_attr, read_container, get_entity_attr, get_subject_attr, get_role_attr. Приведенные правила не изменяют значений никаких других функций и множеств, определенных в модели, и в модели не содержится никаких условий и требований, которым должна удовлетворять функция V. Как следствие, данная функция и связанные с ней правила перехода системы из состояния в состояние не были реализованы в Event-B спецификации, так как на данный момент они малополезны с точки зрения верификации спецификации.

4.4.8. Формализация свойств безопасности МРОСЛ ДП-модели

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

invariants
  @AccessesAreOnlyThroughRoles
    ∀e, s · e ∈ Entities ∧ s ∈ Subjects ∧ e ↦ ReadA ∈
      SubjectAccesses(s)
      ⇒ (∃r · r ∈ Roles ∧ r ↦ ReadA ∈ SubjectAdmAccesses(s)
      ∧ e ↦ Read ∈ RoleRights(r))

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

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

4.5. Верификация

Комплекс инструментальных средств AstraVer Toolset [45] включает в себя среду для разработки и верификации спецификаций на Event-B, основанную на платформе Rodin [44]. Спецификации на Event-B разрабатываются и верифицируются с помощью платформы Rodin. Для каждого требующего доказательства свойства спецификации Rodin автоматически генерирует соответствующие утверждения для доказательства, причем платформа решает проблему поддержки актуальности сгенерированных утверждений и выполненных доказательств в случае изменений в спецификации. Полное доказательство спецификации означает, что доказаны все сгенерированные утверждения.

Для спецификации базового уровня МРОСЛ ДП-модели было сгенерировано 831 утверждение для доказательства, часть из которых была доказана полностью автоматически, а оставшаяся часть — интерактивным образом, при котором доказательство сначала упрощалось и разбивалось на составные части вручную, а уже затем подавалось на вход инструментам автоматического доказательства теорем.

Рассмотрим следующее условие МРОСЛ ДП-модели: для каждой роли существует единственная административная роль roles\_admin\_role , обладающая к ней правом доступа владения, для каждой административной роли существует единственная административная роль admin\_roles\_admin\_role , обладающая к ней правом доступа владения. Данное условие выполняется в результате выполнения каждого правила перехода системы из состояния в состояние, так как право доступа владения к ролям или административным ролям дается только административным ролям roles\_admin\_role или admin\_roles\_admin\_role в результате применения правила вида create\_user(x,x',u) и create\_role(x,r,name,rz) , и нет правил, позволяющих изменить такую роль-владельца роли или административной роли.

Так выглядит математическое доказательство. Рассмотрим теперь тоже самое условие, однако выраженное в виде инвариантов на Event-B:

invariants
  @RolesAR1
    ∀r · r ∈ OrdRoles ⇒ r ↦ Own ∈ RoleAdmRights(RolesAR)
  @ARolesAR1
    ∀r · r ∈ AdmRoles ⇒ r ↦ Own ∈ RoleAdmRights(ARolesAR)

Для каждого изменения входящих в эти инварианты переменных в результате выполнения какого-либо события, а именно переменных OrdRoles, AdmRoles, RoleAdmRights, система верификации сгенерирует утверждения для доказательства. В данном случае утверждения будут сгенерированы для событий create_user, delete_user, create_role, create_hard_link_role, delete_role, grant_admin_rights, remove_admin_rights, так как это полный список событий, в которых каким-либо образом изменяются интересующие нас переменные. Рассмотрим данные события:

  • в событиях create_user и create_role происходит создание новых ролей (изменение множеств AdmRoles и OrdRoles), а также изменение функции доступов RoleAdmRights. Инварианты сохраняются, так как в условиях событий явно прописано добавление доступа владения к создаваемым ролям ARolesAR и RolesAR;
  • в событиях delete_user и delete_role удаляются индивидуальные роли пользователя, а также происходит удаление связанных с ними доступов в функции RoleAdmRights. Это может нарушить инварианты в случае, когда удаляемой ролью становится роль ARolesAR или RolesAR. Однако эта ситуация исключена в предусловиях данных событий и инвариантах;
  • в событиях create_hard_link_role, grant_admin_rights, remove_admin_rights изменяется функция доступов RoleAdmRights, однако в ходе доказательства можно показать, что данные изменения никак не затрагивают права доступа владения.

Следует напомнить, что доказательство на Event-B на самом деле проводится с использованием автоматических и интерактивных инструментов, которые следят за его корректностью и не позволяют допускать ошибки, а данный пример является его примерным словесным описанием.

В итоге получается, что доказательство на Event-B в целом соответствует математическому доказательству (выполняемому «вручную» аналитиком), однако является более достоверным, что иногда позволяет находить несоответствия и нестыковки в описании специфицируемой системы.

4.6. Использование уточнения

В настоящее время МРОСЛ ДП-модель имеет иерархическое представление, состоящее из серии уровней. Нижний уровень модели — базовый уровень, который используется в качестве примера в данной работе, — не зависит от новых элементов, принадлежащих более высоким уровням модели. В свою очередь, все остальные уровни модели наследуют элементы предыдущих уровней, при необходимости корректируя, а также дополняя их новыми элементами.

Event-B позволяет разрабатывать спецификации, отражающие подобную иерархическую структуру. Для этого предлагается использовать технику пошагового уточнения [46, 47]. Вместо создания единой монолитной спецификации, которая будет содержать в себе все детали моделируемой системы, уточнение предлагает разрабатывать серию связанных между собой спецификаций. В такой серии первая спецификация представляет собой некоторую базовую версию системы, которая содержит в себе только основные детали. Дополнительные детали системы шаг за шагом добавляются в остальных спецификациях серии таким образом, что каждая последующая спецификация в серии является уточнением предыдущих. Подробней с техникой уточнения можно ознакомиться в Приложениях А и В.

Как правило, на каждом уровне уточнения добавляются новые переменные, новые события, которые изменяют значения новых переменных, а также модифицируются старые события, например вводятся дополнительные охранные условия, учитывающие значения новых переменных. При этом уточнение позволяет использовать определенные ранее (на предыдущих уровнях уточнения) переменные, но не позволяет изменять их значения. Запрет на изменение старых переменных позволяет быть уверенным, что определенные и доказанные на прошлых уровнях инварианты будут выполняться и на всех последующих. Кроме этого, новые детали системы не должны противоречить старым.

Данные свойства уточнения входят в некоторое противоречие с иерархической структурой МРОСЛ ДП-модели, которая позволяет более высоким уровням при необходимости корректировать элементы предыдущих уровней. Так, например, на базовом уровне в правиле перехода системы из состояния в состояние create_user создаются ровно две индивидуальные роли пользователя. На уровне, в котором реализуется мандатное управление доступом, число создаваемых индивидуальных ролей будет другим: оно будет зависеть от мандатной метки конфиденциальности создаваемой учетной записи пользователя. На Event-B же, если на базовом уровне спецификации сказано, что в событии создается только две роли, то и на всех последующих уровнях в данном событии будут создаваться ровно две роли.

Такое явное противоречие (с точки зрения уточнения и Event-B) просто не позволяет использовать уточнение для добавления новых уровней к приведенной в данной главе Event-B спецификации базового уровня МРОСЛ ДП-модели. Для того чтобы это было возможно, подобные противоречия следует предварительно устранить. В приведенном выше примере для устранения противоречия между двумя уровнями в событии create_user спецификации базового уровня следует отметить, что создаваемых ролей будет несколько, но отдельно описать свойства только двух из них. При уточнении свойства остальных создаваемых индивидуальных ролей будут добавлены в спецификацию в виде дополнительных охранных условий соответствующих событий на уровне мандатного управления доступом.

Рассмотренный метод удовлетворяет требованиям компонента доверия ADV_SPM.1 «Формальная модель политики безопасности» наличия формальной модели политики безопасности (спецификация на формализованном языке Event-B) и ее верификации (формальное доказательство невозможности перехода спецификации в небезопасное состояние). В следующей главе будет предложен подход к формальному доказательству соответствия между функциональной спецификацией объекта оценки и формальной моделью политики безопасности.