Модель невыводимости

Рассмотрим модель невыводимости, также базирующуюся на рассмотрении информационных потоков в системе. Модель невыводимости выражается в терминах пользователей и информации, связанных с одним из двух возможных уровней секретности (высокий и низкий).

Система считается невыводимо безопасной, если пользователи с низкими уровнями безопасности не могут получить информацию с высоким уровнем безопасности в результате любых действий пользователей с высоким уровнем безопасности. Другими словами, в таких системах утечка информации не может произойти в результате посылки высокоуровневыми пользователями высокоуровневой информации к низкоуровневым пользователям. Интуитивно это определение относится не к информационным потокам, а к разделению информации. Однако такое определение безопасности не предохраняет информацию высокоуровневых пользователей от просмотра низкоуровневыми пользователями. Данное определение требует, чтобы низкоуровневые пользователи не были способны использовать доступную им информацию для получения высокоуровневой информации (это объясняет, почему определение названо невыводимостью).

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

- набор пользователей с высоким или низким уровнем безопасности;

- набор возможных последовательностей системных вводов информации от пользователей и выходных реакций системы.

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

Если множество вводов от пользователей в машину связано со множеством выводов, получаемых пользователями от машины каким-либо разумным образом (возможно, основываясь на времени их поступления), то тогда можно рассматривать выходную последовательность как трассировку (traces, см. модель невмешательства) системы. Безопасность невыводимости может быть определена в соответствии со множеством всех трассировок системы и множеством вводов и выводов, видимых пользователями.

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

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

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