19,23,25 Язык описания политик безопасности

Корт С. С, Боковенко И. Н.

СЦЗИ СПбГТУ

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

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

закрытые политики безопасности — все разрешенные виды доступа должны быть специфицированы;

открытые политики безопасности — все запрещенные виды доступа должны быть специфицированы;

гибридные политики безопасности;

гибридные политики безопасности с разрешенными противоречиями.

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

Язык описания политик безопасности состоит из следующих компонентов:

1. Множества.

1.1. объектов. Obj — множество объектов. Объекты могут быть сгруппированы по типам Т (types).

1.2. субъектов, которым может быть предоставлен доступ:

1.2.1. U — пользователи — отдельные пользователи, работающие с системой;

1.2.2. G — группы — множества пользователей. Субъект s является членом группы G непосредственно, если он определен как член группы G, и косвенно, если существует последовательность s₁, s₂, … ,s_n, n > 1, так что s_i непосредственный член s_i+1 для i=1, .... n-1. Единственным ограничением на членство в группе является ацикличность, т.е. ес­ли s_i член s_j, то s_j, не может быть членом s_i.

1.2.3. R — роли — именованные списки привилегий, необходимые для работы в системе. Роль есть именованный список привилегий, необходимых для выполнения некоторых обязанностей в системе. Также как и группы, роли могут быть организованы в иерархию.

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

1.3. действии А субъектов над объектами, и множество знаковых авторизованных типов SА =

2.Отношения над множествами субъектов и объектов — предикаты:

2.1. Иерархического членства субъектов и объектов:

dirin и in Аргументы — переменные субъектов, s₁ и s₂ Отражают концепцию прямого н

косвенного членства.

typeof. Аргументы — переменные объекта o и типа t. Отражает группирование объектов.

2.2. Доступа субъектов к объектам:

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

cando Первый аргумент данного предиката — переменная объекта, второй — субъекта, а третий — знаковая авторизация. Данный предикат определяется офицером безопасности системы.

do. Аргументы данного предиката такие же, как у предиката саndo. Представляет авторизацию, которую имеет каждый субъект для каждого объекта. Реализует политику разрешения конфликтов.

dorcando. Аргументы данного предиката такие же, как у предиката cando. Представляет авторизацию, определяемую системой с использованием логических правил.

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

2.3. Роли субъектов

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

2.4. Конфликтов спецификации авторизации

error. Аргументы отсутствуют. Отражает ошибки в спецификации и использовании ав­торизации.

Если p — описанный выше предикатный символ с корректным количеством и типом переменных

t₁,...,t_n то р(t₁,...,t_n) есть атом. Литеры отображают атомы или их отрицание. Например: cando(OT, ST, SAT) и -cando(ОТ, 5Т, 5АТ) являются литерами.

3. Правила, составляющие спецификацию политики безопасности (авторизации).

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

В описываемом языке определены следующие правила:

3.1. Осуществленное действие.

done(о, s, R, a, t) <— .

где o, s, R, a, t — элементы Obj,U, 2^R, A и IN соответственно. Правило done является свершившимся фактом, и, как следствие, тело его пусто. Правило done определяется системой при выполнении доступа. Если done(o, s, R, a, t) — истинно, то пользова­тель s с ролью R осуществил действие а над объектом о во время t. Данное правило полезно для политик безопасности, в которых решение о предоставлении доступа для пользователя базируется на его предыдущих действиях.

3.2. Авторизация.

Правила, задающие начальное состояние системы:

cando (о, s, <sign> a) <— L₁ &L₂...&Ln

где о, s, а, — элементы ObjU G R A соответственно, n  0, <sign> = {+,-}, и для каждого 0 < i < n, L_i есть in или dirin или typeof литерал. Правила авторизации задаются администратором для разрешения или запрещения доступа. Литерал в правой части задаст условия, которые должны быть верифицированы для выполне­ния авторизации.

Производные правила:

dorcando(o, s, <sign> a) L₁ &L₂...&L_n

где о, s, а, — элементы ObjU G R A соответственно, n  0, <sign> = {+, -}, и для каждого 0 < i < n, L_i do, cando, done, in, dirin или typeof литерал. Все dorcando литералы в теле правила должны быть позитивными.

Правила разрешения конфликтов авторизации:

do(o, s, <sign> a)  L₁ &L₂...&L_n

где о, s, а, — элементы ObjU G R A соответственно, n  0, <sign> = {+, -}, и для каждого 0 < i < n, L_i cando, dorcando, done, in, dirin или typeof литерал. Все dorcando литералы в теле правила должны быть позитивными. Разрешающее прави­ло разрешает или запрещает доступ субъекту системы. Данное правило использует­ся в случае, если правила cando и dorcando не дают положительной или отрицатель­ной авторизации. В этом случае правило do задает принудительную авторизацию или авторизацию по умолчанию.

Правила контроля доступа:

grant(o, u, rs, <sign> a)  L₁ &L₂...&L_n,

где для каждого 0 < i < n, L_i, cando, dorcando, done, do, in, dirin или typeof литерал. Если grant(o, u, R, +a) — истинно, то пользователь и с активной ролью R может вы­полнить действие а над объектом о. Аналогично, если grant(o, u, R, +a) — истинно, то действие запрещено.

3.3. Правило целостности.

errorOL₁ &L₂...&L_n.

где для каждого 0 < i < n, L_i grant, cando, dorcando, done, do, in, dirin или typeof литерал. При добавлении нового правила r вычисляется правая часть правила, и r принимается только, если в результате обработки правила не генерируется ошибка. Данное правило является специфическим для приложения. В общем случае правило целостности говорит о том, что ни один из субъектов не может иметь доступ и отсутствие доступа к объекту.

С использованием описанного языка авторизации закрытые (открытые) политики безопасности могут быть специфицированы с использованием только положительных (отрицательных) авторизации.

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

• Порождение (правила, регулирующие распространение прав доступа вдоль иерархии субъектов). Для решения этой проблемы могут быть применены следующие подходы:

• запрет распространения прав доступа для потомков;

• запрет перекрытия — все авторизации распространяются, не считаясь с конфликта­ми;

• перекрытие субъектами-потомками — авторизация для субъекта s перекрывает авто­ризацию для супер-субъекта s";

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

• Разрешение конфликтов (правила, определяющие авторизацию, в случае наличия конфликтной авторизации). Существует четыре подхода к решению данной задачи:

• запрет конфликтов — наличие конфликта рассматривается как ошибка;

• запрет имеет преимущество — запрет доступа реализуется преимущественно над его разрешением;

• разрешение имеет преимущество — разрешение доступа реализуется преимущест­венно над его запретом;

• отсутствие преимущества — ничто не имеет первенства, окончательный результат не имеет решения.

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

Существует ряд моментов, которые следует отметить перед непосредственным описанием политик безопасности:

Поскольку в описываемых моделях роли отсутствуют, предикат grant не используется.

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

По этой же причине (простота описываемых моделей) предикат error не используется.

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

Для всех моделей введем общие положения, касающиеся алфавита языка описания авторизации:

giG i  Z	Существуют группы пользователей gш, принадлежащие множеству групп пользователей G
gi-1 gi i  Z	Иерархия групп пользователей, а значит и субъектов, определяется включением одной группы в другую.
oObj;sSubj;sG;oG	Субъекты могут принадлежать к какой-либо группе gi, объекты не имеют принадлежности к группам, иерархия объектов косвенно определяется через иерархию субъектов(см. правила авторизации.
r, w A ==>+r,-r,+w, -w  SA	Существуют права чтения и записи, принадлежащие множеству знаковой авторизации.
a = r v w	Для удобства "а" означает чтение или запись

Операция create (создание объекта субъектом) в данных моделях может рассматриваться как одновременное чтение и запись объекта субъектом.

Рассмотрим общую схему построения набора предикатных правил, составляющих спецификаций авторизации рассматриваемых моделей безопасности:

Начальное состояние системы задается предикатами cando и предикатами вида

in(s,g)  (принадлежностью субъектов группам g_i). Начальное состояние задает администратор.

Политика разрешения конфликтов реализуется с помощью предикатов do конструкциями вида

Y  X₁ ^ Х₂^ Х₃^,...,где Y — предикат do(...),

а X_i, предикат cando(...), cando(...), in(...), in(...),dirin(...), dirin(...)

Т.е. на наличие конфликтов проверяется начальное состояние системы.

Собственно правила функционирования модели задаются с помощью предикатов dorcando конструкциями вида

Y X₁^ Х₂^ Х₃^..., где Y-предикат dorcando(...), а X_i, — предикат do(...), do(...), in(...), in(...),dirin(...), dirin(...)

Перейдем к описанию моделей безопасности на языке описания политик безопасности.