Модель невмешательства

Невмешательство - ограничение, при котором ввод высоко уровневого пользователя не может смешиваться с выводом низкоуровневого пользователя.

Модель невмешательства рассматривает систему, состоящую из четырех объектов: высокий ввод (high–in), низкий ввод (low–in), высокий вывод (high–out), низкий вывод (low–out).

Рассмотрим систему, вывод которой пользователю u определен функцией out(u, hist.read(u)), где hist.read(u) – история ввода системы (traces), чей последний ввод был read(u) (команда чтения, исполненная пользователем u). Для определения безопасности системы необходимо определить термин очищения (purge) историй ввода, где purge удаляет команды, исполненные пользователем, чей уровень безопасности не доминирует над уровнем безопасности u. Функция clearence(u) – определяет степень доверия к пользователю

Определение: purge –функция users × traces →traces такая, что:

 purge(u, <>) = <>, где о - пустая история ввода;

 purge(u, hist.command(w)) = purge(u, hist.command(w)), если
command(w) – ввод, выполненный пользователем w; clearence(u)≥clearence(w);

 purge(u, hist.command(w)) = purge(u, hist), если command(w) - ввод, выполненный пользователем w; clearence(u)<clearence(w).

Система удовлетворяет требованию невмешательства, если и только если для всех пользователей u, всех историй Т и всех команд вывода с out(u,T.c(u)) = out(u,purge(u,T).c(u)).

Для того, чтобы проверить, удовлетворяет ли система требованиям невмешательства, было разработано множество условий («unwinding conditions»), выполнение которых достаточно для поддержки невмешательства в модели машины состояний. Хотя верификация модели невмешательства труднее, чем верификация БЛМ, после нее в системе не остается скрытых каналов утечки информации. Модель невмешательства ближе к интуитивному понятию безопасности, чем БЛМ.

При сравнении модели невмешательства с БЛМ можно отметить:

1. БЛМ слабее, чем модель невмешательства, так как модель невмешательства запрещает многие скрытые каналы, которые остаются при реализации примитивной БЛМ.

2. Модель невмешательства слабее, чем БЛМ в том, что она разрешает низкоуровневым пользователям копировать один высокоуровневый файл в другой высокоуровневый, что БЛМ запрещает, так как при этом нарушается ее безопасность по чтению.

Было показано, что для определенных систем модель невмешательства особенно хороша в том, что если последовательность ввода Х не смешивается с последовательностью вывода Y, и Х независима от ввода других пользователей, то I (X, Y)=0, где I (X, Y) – взаимная для Х и Y информация и представляет собой поток информации от X к Y.