Правило 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 имеет значение (), субъекту target назначается уровень целостности исполняемого файла image. Если поле image имеет значение (), поле level должно иметь значение, отличное от ().

Если поле levelR имеет значение (), уровень целостности levelR принимается равным уровню целостности субъекта target.

Чтобы задать уровни целостности 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"

}

}