Правило execute модели безопасности Mic

execute <ExecuteImage | ExecuteLevel>

type ExecuteImage =

{ image : Sid

, target : Sid

, level : Level | ... | ()

, levelR : Level | ... | ()

}

type ExecuteLevel =

{ image : Sid | ()

, target : Sid

, level : Level | ...

, levelR : Level | ... | ()

}

Назначает субъекту target уровень целостности level и задает минимальный уровень целостности субъектов и ресурсов, из которых этот субъект может принимать данные (levelR). Код субъекта target содержится в исполняемом файле image.

Если значение level не задано (level : ()), субъекту target назначается уровень целостности исполняемого файла image. Если значение image не задано (image : ()), должно быть задано значение level.

Если значение levelR не задано (levelR : ()), то значение levelR равно level.

Чтобы задать уровни целостности level и levelR, используются значения типа Level. Определение типа Level см. в "Правило create модели безопасности Mic".

Правило возвращает результат "разрешено", если назначило субъекту target уровень целостности level и задало минимальный уровень целостности субъектов и ресурсов, из которых этот субъект может принимать данные (levelR).

Правило возвращает результат "запрещено" в следующих случаях:

• Значение level превышает уровень целостности исполняемого файла image.
• Значение level несравнимо с уровнем целостности исполняемого файла image.
• Значение levelR превышает значение level.
• Значения level и levelR несравнимы.
• Исполняемому файлу image не назначен уровень целостности.
• Значение image или target вне допустимого диапазона.

Пример:

/* Запуск процесса класса updater.Manager будет разрешен,

* если при инициации запуска этому процессу будет назначен

* уровень целостности LOW, а также будет задан минимальный

* уровень целостности процессов и ресурсов, из которых этот

* процесс может принимать данные (LOW). Иначе запуск процесса

* класса updater.Manager будет запрещен. */

execute src=Einit, dst=updater.Manager, method=main {

mic.execute { target : dst_sid

, image : ()

, level : "LOW"

, levelR : "LOW"

}

}