Приложение А (справочное). Примеры перевода элементов математического описания формальной модели управления доступом в формализованное (машиночитаемое) описание

Приложение А
(справочное)

Примеры
перевода элементов математического описания формальной модели управления доступом в формализованное (машиночитаемое) описание

А.1 Введение

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

А.2 Пример перевода элементов состояния абстрактного автомата

Пусть даны следующие элементы состояния абстрактного автомата математического описания формальной модели управления доступом:

S - множество субъектов доступа;

О - множество объектов;

С - множество контейнеров;

Е = О U С - множество объектов доступа (сущностей), где О  С = ;

Н _Е: Е  2 ^E - функция иерархии сущностей;

RA = {read _a, write _a} - множество видов доступа, где read _a - доступ на чтение, write _a - доступ на запись;

А  S х (Е U S) х RA - множество реализуемых доступов субъектов доступа к сущностям и субъектам доступа;

RR = {read _r, write _r, execute _r, own _r} - множество видов прав доступа;

Р  S х (Е U S) х RR - множество реализуемых прав доступа субъектов доступа к сущностям и субъектам доступа;

(LI, ) - решетка уровней целостности, где - отношение частичного порядка на множестве уровней целостности LI;

(LC, ) - решетка уровней конфиденциальности, где - отношение частичного порядка на множестве уровней конфиденциальности LC;

i _e: E  LI - функция, задающая уровень целостности каждой сущности;

i _s: S  LI - функция, задающая уровень целостности каждого субъекта доступа;

f _e: E  LC - функция, задающая уровень конфиденциальности каждой сущности;

f _s: S  LC - функция, задающая уровень доступа каждого субъекта доступа.

В машиночитаемом описании формальной модели на языке, поддерживаемом формальным методом Event-B, для элементов неизменяемой части состояний используются статические множества (sets), константы (constants) и аксиомы (axioms). Изменяющиеся элементы состояний приводятся в блоке переменных (variables). В блоке инвариантов (invariants) - условий и требований на переменные, которые должны быть выполнены в каждом состоянии - каждой переменной задается тип.

context С0

sets

AIIEntitiesAndSubjects // множество всех субъектов доступа и сущностей

AccessRights // множество видов доступа RR

Accesses // множество видов прав доступа RA

Integrity // уровни целостности решетки LI

Confidentiality // уровни конфиденциальности решетки L

constants

AllSubjects // множество всех возможных субъектов доступа

AIIEntities // множество всех возможных сущностей

ReadR // право доступа read _r

WriteR // право доступа write _r

ExecuteR // право доступа execute _r

OwnR // право доступа own _r

ReadA // право доступа read _a

WriteA // право доступа write _a

axioms

@ AIIEntitiesAndAIISubjectsTypes partition(AIIEntitiesAndSubjects,

AllSubjects, AIIEntities)

@AccessRightsTypes partition(AccessRights, {ReadR}, {WriteR}, {ExecuteR}, {OwnR})

@AccessesTypes partition(Accesses, {ReadA}, {WriteA})

machine М0 sees С0

variables

Subjects // множество субъектов доступа S

Objects // множество объектов О

Containers // множество контейнеров С

Entities // множество сущностей Е

EntityHierarchy // функция иерархии сущностей Н _Е

SubjectAccessRights // множество реализуемых прав доступа субъектов

// доступа к сущностям и субъектам доступа Р

SubjectAccesses // множество реализуемых доступов субъектов

// доступа к сущностям и субъектам доступа А

Entitylnt // функция, задающая уровень целостности

// каждой сущности i _e

Subjectlnt // функция, задающая уровень целостности

// каждого субъекта доступа i _s

EntityCnf // функция, задающая уровень конфиденциальности

// каждой сущности f _e

SubjectCnf // функция, задающая уровень конфиденциальности

// каждого субъекта доступа f _s

invariants

@SubjectsType Subjects  AIISubjects

@EntitiesType Entities  AIIEntities

@ObjectsAndContainersType partition(Entities, Objects, Containers)

@EntityHierarchyType EntityHierarchy  Entities (Entities)

@SubjectAccessRightsType SubjectAccessRights  Subjects  (Subjects U Entities  AccessRights)

@SubjectAccessesType SubjectAccesses  Subjects  (Subjects U Entities  Accesses)

@EntityIntType EntityInt  Entities  (lntegrity)

@SubjectIntType SubjectInt  Subjects  (lntegrity)

@EntityIntCnf EntityCnf  Entities  (Confldentiality)

@SubjectCnfType SubjectCnf  Subjects  (Confidentiality)

A.3 Пример перевода описания правила перехода абстрактного автомата из состояний в состояния

Заданное в математическом описании формальной модели управления доступом правило создания субъектом доступа объекта в контейнере имеет следующий вид. Параметры правила:

х - субъект доступа;

у - создаваемый объект;

z - контейнер, в котором создается объект;

yi - уровень целостности создаваемого объекта;

ус - уровень конфиденциальности создаваемого объекта.

Условия применения правила (ограничения на значения параметров правила и элементов состояния, к которому применяется правило):

х  S - субъект доступа функционирует в текущем состоянии абстрактного автомата;

у  E - объект не существует в текущем состоянии абстрактного автомата;

z  С - контейнер существует в текущем состоянии абстрактного автомата;

(х, z, write _a)  А - субъект доступа обладает доступом на запись к контейнеру;

(х, z, execute _r)  Р - субъект доступа обладает правом доступа на выполнение к контейнеру;

yi  min(i _s(x), i _e(z)) - уровень целостности создаваемого объекта не выше уровней целостности субъекта доступа и контейнера, в котором создается объект;

ус = f _e(z) = f _s(x) - должны быть равны уровень доступа субъекта доступа и уровни конфиденциальности создаваемого объекта и контейнера, в котором создается объект.

Результаты применения правила (ограничения на значения элементов состояния, полученного в результате применения правила):

 = Е U {у} - объект как сущность добавляется во множество сущностей в последующем состоянии абстрактного автомата;

 = О U {у} - объект добавляется во множество объектов;

(z) = H _E(z) U {у} - объект добавляется в состав контейнера;

(у) =  - созданный объект не включает другие объекты или контейнеры;

 = Р U {(х, у, own _r)} - субъект доступа получает право доступа владения к созданному объекту;

(y) = yi - для созданного объекта задается его уровень целостности;

(y) = yc - Для созданного объекта задается его уровень конфиденциальности.

В машиночитаемом описании на языке, поддерживаемом формальным методом Event-B, правило может задаваться следующим событием:

event create_object

any // параметры

х у z yi ус

where // охранные условия выполнения события, соответствующие

// условиям применения правила

@grd1 х  Subjects

@grd2 у  AIIEntities \ Entities

@grd3 z  Containers

@grd4 z  WriteA  SubjectAccesses(x)

@grd5 z ExecuteR  SubjectAccessRights(x)

@grd6 yi  EntityInt(z)  yi  SubjectInt(x)

@grd7 yc = EntityCnf(z)  ус = SubjectCnf(x)

@grd8 z  dom(EntityHierarchy)

then // действия по изменению значений переменных состояния

// в результате срабатывания события, соответствующие

// результатам применения правила

@act1 Entities := Entities U {у}

@act2 Objects := Objects U {y}

@act3-4 EntityHierarchy(z) := EntityHierarchy(z) U {y}

@act5 SubjectAccessRights(x) := SubjectAccessRights(x) U {y OwnR}

@act6 EntityInt(y) := yi

@act7 EntityCnf(y) := yc

end

A.4 Пример перевода условия безопасности

Заданные в математическом описании формальной модели управления доступом ограничения на уровни целостности сущностей в составе контейнеров определяются следующим образом: для сущностей х, у  Е, если х  Н _Е(у), то i _e(x)  i _e(y) (уровень целостности сущности не выше уровня целостности контейнера, в котором она содержится). В машиночитаемом описании на языке, поддерживаемом формальным методом Event-B, ограничения на уровни целостности задаются инвариантом:

invariants

@EntityHierarchy1

x,   Entities  у  Entities  х  dom(EntityHierarchy)

EntityInt(x)  EntityInt(y)