Глава 6. Модели безопасности 6. 1. Основные понятия

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

Немного о математической логике, которую будем использовать при рассмотрении моделей.

В логике существует понятие предикатов первого и второго порядка.

Логика первого порядка (исчисление предикатов) - формальное ис­числение, допускающее высказывания относительно переменных, фикси­рованных функций, и предикатов. Расширяет логику высказываний. В свою очередь является частным случаем логики высшего порядка.

Логика высказываний (или пропозициональная логика) - это фор­мальная теория, основным объектом которой служит понятие логического высказывания. С точки зрения выразительности, её можно охарактеризо­вать как классическую логику нулевого порядка. Логика высказываний является простейшей логикой, максимально близкой к человеческой логи­ке неформальных рассуждений и известна ещё со времён античности.

Базовыми понятиями логики высказываний являются пропозицио­нальная переменная - переменная, значением которой может быть логиче­ское высказывание, - и (пропозициональная) формула, определяемая ин­дуктивно следующим образом:

• Если Р - пропозициональная переменная, то Р - формула.

• Если А - формула, то -<А — формула.

• Если А и В - формулы, то (^ ~~* Щ — формула.

• Других соглашений нет.

Знаки ""'j Л, V _и _^ (отрицание, конъюнкция, дизъюнкция и имплика­ция) называются пропозициональными связками. Подформулой называет­ся часть формулы, сама являющаяся формулой. Собственной подформу­лой называется подформула, не совпадающая со всей формулой.

Язык логики первого порядка строится на основе сигнатуры, со­стоящей из множества функциональных символов ^и множества преди­катных символов V. С каждым функциональным и предикатным симво­лом связана арность, то есть число возможных аргументов (Арность пре-

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

• Символы переменных (обычно x,y,z,xl,yl,zl,x2,y2,z2, и т. д.),

• Пропозициональные связки: V, Л, ->, —^

• Кванторы: всеобщности Уи существования 3,

• Служебные символы: скобки и запятая.

Перечисленные символы вместе с символами из V и Т образуют Алфавит логики первого порядка. Более сложные конструкции определя­ются индуктивно:

Терм есть символ переменной, либо имеет вид A*i, ■■ ■, *п)_? где f -функциональный символ арности n, a *ii - ■ ■ ■> *п - термы.

Атом имеет вид где р - предикатный символ арности п,

a *i 1- - - 1 *п - термы.

Атом в математической логике - простейший случай формулы; фор­мула, которую нельзя расчленить на подформулы.

Предикат (n-местный, или п-арный) - это функция с множеством значений {0,1} (или «ложь» и «истина»), определённая на множестве М — Aii х М₂ х... х М_п Таким образом, каждый набор элементов мно­жества М он характеризует либо как «истинный», либо как «ложный».

Предикат можно связать с математическим отношением: если п при­надлежит отношению, то предикат будет возвращать на ней 1.

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

Предикат называют тождественно-истинным и пишут:

Р(х₁,...,х_п) = \

если на любом наборе аргументов он принимает значение 1. Предикат называют тождественно-ложным и пишут: Р(х₁,...,х_п) = 0_?

если на любом наборе аргументов он принимает значение 0.

Предикат называют выполнимым, если хотя бы на одном наборе ар­гументов он принимает значение 1.

Так как предикаты принимают только два значения, то к ним приме­нимы все операции булевой алгебры, например: отрицание, импликация, конъюнкция, дизъюнкция и т.д.

Формула - это либо атом, либо одна из следующих конструкций: ->F, Fi V F?, Fi Л F₂, Fi —> F₂, VxF, EtaF _где p pi Y2 - формулы, а х -

переменная.

Переменная х называется связанной в формуле F, если F имеет вид \/з;С?либо 3xG или же представима в одной из форм -i#, F\ V F₂, Fi A F₂, Fi —► F₂^ причем х уже связанна в H, Fl и F2. Если х не связанна в F, ее называют свободной в F. Формулу без свободных пе­ременных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

Логика второго порядка - расширяет логику первого порядка, позво­ляя проводить квантификацию общности и существования не только над атомами, но и над предикатами.

Логика второго порядка не упрощается к логике первого порядка.

Логика первого порядка подходит для описания рутинных свойств системы, то есть тех, ради которых ABC создается. Так как свойства безо­пасности системы являются дополнительным всеобъемлющим требовани­ем, то необходимо применение логики второго порядка. Ядро безопасно­сти ABC гарантирует безопасность системы вне зависимости от того, ка­кие функции ядра и в какой последовательности задействованы. При этом свойства безопасности системы в целом могут быть описаны следующим выражением:

Va.(E pos:P(a), (l)

где pos - множество всех возможных последовательностей вызовов функ­ций, предоставляемых ядром безопасности системы;

Р() - предикат, определяющий выходную реакцию в системе в зави­симости от входного воздействия.

Выражение (1) является предикатом второго порядка и определяет следующее свойство: любая операция, выполняемая пользовательским программным обеспечением, преобразуется в последовательность вызовов функций ядра безопасности системы (функций в множестве pos = свойст­во полноты) и при условии защиты программного обеспечения ядра сис­темы от модификации (= свойство изоляции), свойство Р() является свой­ством системы в целом. Доказательство безопасности системы сводится к демонстрации инвариантности модели системы по отношению к некото­рому свойству безопасности, определяемому предикатом Р. Таким обра­зом, для синтеза защищенной вычислительной системы необходимо вы­полнение следующих условий:

• свойства безопасности системы должны быть реализованы с помощью ядра безопасности системы;

• данные свойства должны быть выражены предикатом второго порядка (1).

В анализируемых далее моделях безопасности предикат Р конкрети­зируется, а вместо исследования выражений, описываемых логикой второ­го порядка, изучаются модели состояний системы. Для модели системы необходимо доказать следующую теорему, называемую основной теоре­мой безопасности: «Если система начинает работу в безопасном состоя­нии и все переходы системы из состояния в состояние являются безопас­ными, то система является безопасной».

Таким образом, необходимо ввести понятия, пригодные для описа­ния свойств состояния системы. Самыми естественными понятиями, с по­мощью которых можно описать состояние системы, являются понятия субъекта, объекта и доступа, которые и являются основой описания со­стояния моделей безопасности защищенных ABC.

Сущность - любая именованная составляющая компьютерной сис­темы.

Объект - пассивная сущность, используемая для хранения и полу­чения информации. Возможные примеры объекта:

• Записи;

• Сегменты;

• Файлы;

• Терминалы;

• Узлы сети;

• Биты;

• Байты...

Субъект - активная сущность. Она может инициировать запросы к ресурсам и использовать их для выполнения каких-либо вычислительных заданий. В процессе исполнения субъекты исполняют операции. Примеры субъектов:

• Пользователь;

• Процесс;

• Устройство...

Взаимодействие субъекта и объекта, в результате которого произво­дится перенос информации между ними, называется доступом. Существует две фундаментальные операции, переносящие информацию между ними:

• Операции чтения - такая операция, результатом которой являет­ся перенос информации от объекта к субъекту;

• Операция записи - такая операция, результатом которой являет­ся перенос информации от субъекта к объекту.

Основной характеристикой субъекта является уровень безопасности.

Уровень безопасности - иерархический атрибут, который может быть ассоциирован с сущностью компьютерной системы для обозначения степени ее чувствительности по безопасности. Эта степень чувствитель­ности может отражать степень ущерба от нарушений безопасности.

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

• Неклассифицированная информация;

• Конфиденциальная информация;

• Секретная информация;

• Совершенно секретная информация.

Для того, чтобы сопоставлять уровни безопасности, нужно внести математические обозначения.