Формальная и неформальная политики безопасности

5.1.1. Неформальная политика безопасности

Для неформальной политики безопасности широкое распростране­ние получило описание правил доступа субъектов к объектам в виде таб­лицы, наглядно представляющей правила доступа. Обычно такая таблица подразумевает, что субъекты, объекты и типы доступа определены. Это позволяет составить таблицу, содержащую колонку типов доступа и ко­лонку соответствующего отношения, которое должно соблюдаться между субъектом и объектом для данного типа доступа (см. таблицу 5).

Таблица 5

Выражение неформальной политики безопасности

Тип доступа	Отношение (субъект, объект)
Чтение	Больше
Выполнение	Больше
Запись	Равно

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

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

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

5.1.2. Формальная политика безопасности

Для лучшего понимания принципов, используемых при создании формальных политик безопасности, рассмотрим основные математиче­ские методы, применяемые при формальном анализе вообще и формаль­ном описании политик безопасности ABC в частности.

При анализе функционирования систем (не обязательно ABC), об­ласть применения которых является критичной, желательно рассмотреть все возможные поведения системы - ее реакции на все возможные вход­ные данные.

Хотя количество всех возможных реакций системы слишком велико для исследования, существует два метода, позволяющих уменьшить коли­чество реакций, которые необходимо рассмотреть за счет группировки «схожих» реакций системы. Получается, что для рассмотрения всех воз­можных реакций системы необходимо рассмотреть лишь небольшое ко­личество входных воздействий.

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

незначительные изменения в выходных данных. Это позволяет проанали­зировать (протестировать) поведение системы, основанной на физических законах конечным количеством тестов.

Первый метод заключается в доказательстве того, что система всегда «работает корректно», второй заключается в демонстрации того, что сис­тема никогда не выполняет неверных действий.

При использовании первого метода используется комбинация анали­за и эмпирического тестирования для определения таких реакций систе­мы, которые могут привести к серьезным сбоям - например, функциони­рование системы при граничных условиях или при условиях, не оговорен­ных в качестве возможных для компонентов системы. В качестве примера можно привести требование описания поведения системы в ответ на вход­ное воздействие «выключение питания».

Второй метод выдвигает гипотезу о том, что система делает что-то некорректное, и на этой основе ведется анализ реакций системы с выявле­нием состояний, в которых возможно проявление данной некорректности. Доказательство корректности работы системы сводится к демонстрации того, что данные состояния недостижимы, то есть к доказательству от противного.

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

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

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

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

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

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

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

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

К модели безопасности должны предъявляться требования, общие для всех моделей:

• адекватность;

• способность к предсказанию;

• общность.