Представление системы семантически осмысленного ролевого управления доступом в виде цветной сети Петри | ПДМ. 2013. № 1(19).

Представление системы семантически осмысленного ролевого управления доступом в виде цветной сети Петри

Рассматривается механизм внесения изменений в систему семантически осмысленного ролевого управления доступом в рамках СК-РУД модели одновременно несколькими администраторами. С использованием математического аппарата сетей Петри описываются процессы перехода системы между состояниями и обосновывается условие безопасности переходов.

Representation of semantic role based access control system by a colored Petri net.pdf Введение Система семантически осмысленного ролевого управления доступом основана на модели ролевого управления доступом с семантическим контекстом СК-РУД [1] и позволяет автоматизировать назначение и отзыв ролей пользователям при наступлении в системе ряда определённых событий. Классическая модель ролевого управления доступом RBAC [2], расширением которой является модель СК-РУД, содержит описание процессов внесения изменений в конфигурацию в предположении, что в каждый момент времени в системе действует не более одного субъекта с административными привилегиями. В системах ролевого управления доступом в компьютерных системах с десятками тысяч пользователей и тысячами привилегий администрирование, как правило, осуществляется несколькими пользователями. Данный подход получил название «распределённого администрирования» системы. Применение классического подхода для описания функционирования таких систем может привести к конфликтам между действиями различных администраторов. Примерами таких конфликтов могут быть ситуации, когда два администратора одновременно вносят изменения в учётную запись пользователя или заявка на назначение роли зарегистрирована и назначена одному из администраторов раньше, чем другому администратору назначена заявка на отзыв роли, взаимоисключающей первую роль. Исходя из этого, целесообразно рассмотреть вопрос формального описания процессов распределённого администрирования в системах ролевого управления доступом и определения условий безопасного перехода системы между состояниями. 1. Основные понятия и определения В данной работе используются следующие обозначения для элементов СК-РУД модели: P — множество привилегий или полномочий; A — множество атрибутов учетных записей пользователей; V = {(vj)}, где i — номер атрибута из A; j Е [1, N]; N — число возможных различных значений атрибута aj Е A; va/ues : A ^ 2V — функция, задающая для каждого атрибута множество его допустимых значений; U — множество атрибут-пользователей (множество векторов вида (uxi,... , uxna), где ux Е va/ues (aj)); R — множество ролей системы; UA : U ^ 2r — функция, задающая для каждого пользователя множество ролей, на которые он может быть авторизован; S — множество сессий пользователей системы; PA : R ^ 2P — функция, задающая для каждой роли множество привилегий. При этом для каждой привилегии p Е P существует роль r Е R, такая, что p Е PA(r); user : S ^ U — функция, задающая для каждой сессии пользователя, от имени которого она авторизована; ro/es : S ^ 2r — функция, задающая для пользователя множество ролей, на которые он авторизован в данной сессии. При этом в каждый момент времени для каждой сессии s Е S выполняется условие ro/es(s) Е UA(user(s)); CR — множество предварительных условий назначения ролей; AP — множество административных привилегий; AR С 2ap — множество административных ролей; APA : AR ^ 2ap — функция, задающая для каждой административной роли множество административных привилегий; при этом для каждой привилегии p Е AP существует роль r Е AR, такая что p Е APA(r); can_assign : AR ^ CR х 2R — функция, определяющая для каждой административной роли множество ролей, которые могут быть назначены пользователю с использованием данной административной роли при выполнении заданных предварительных условий CR; can_revoke : AR ^ 2R — функция, определяющая для каждой административной роли множество ролей, которые могут быть отозваны у пользователя с использованием данной административной роли. Определение 1. Две роли r1,r2 Е R называются статически взаимоисключающими, если они не могут быть назначены пользователю одновременно: для s Е S выполняется неравенство | {r1,r2} П ro/es(s) 1. Определение 2. Две роли r1,r2 Е R называются динамически взаимоисключающими, если они не могут быть активированы сессией пользователя одновременно: для u Е U выполняется неравенство | {r1 ,r2} П UA(u) 1. Определение 3. Иерархией ролей «по предусловию» RH [1] будем называть заданное на множестве ролей R отношение строгого порядка «>». При этом по определению (для пользователя u Е U) если (r1,r2) Е RH, r1 > r2 и cri (u) = true, то cr2 (u) = true и cri (u) = cri (z1(u),... , cr2 (u),... , (u)). Роль r1 будем называть предком r2 «по предусловию». Определение 4. Пусть t : U ^ {false, true} — функция, такая, что tj(u)=true тогда и только тогда, когда tj G values^) и для u G U выполняется условие ux = tj, где aj G A, 1 ^ i ^ |A|. Пусть car : U ^ {false, true} — функция, такая, что car (u) =car (ti (u) ,... , tna (u)), u G U, r G R, где car(y1,..., yna) — булева функция от na переменных, na G {1,..., |A|}. Тогда CA = {car1,... , cart} —множество функций, определяющих, при каких ограничениях на атрибуты учетной записи пользователя ему может быть назначена некоторая роль rj G R. Дадим основные понятия и определения теории цветных сетей Петри (ЦСП), которые потребуются для дальнейшего описания результатов исследования [3]: Qc — множество цветов; TK — множество токенов. По определению токен — это кортеж вида tk = (x1,... , xn), где Xj — переменная некоторого заданного цвета. Цвета токенов могут быть простыми или составными. Множество допустимых значений для токенов составных цветов — это декартово произведение множеств допустимых значений для входящих в его состав простых цветов; Ctfc : TK ^ Qc — функция окрашивания, задающая для каждого токена его цвет; Pl — множество мест (элементов pl G Pl, каждый из которых содержит один или несколько токенов определенного цвета); Срг : Pl ^ Qc — функция, определяющая множество допустимых цветов для данного места. Множество цветов токенов, которые могут содержаться на месте pl, называется типом места pl. Множество токенов на месте pl называется содержимым места и обозначается tk(pl). Определение 5. Пусть Pl — конечное множество мест. Пусть Nj(plj) —количество токенов каждого из цветов на месте plj G Pl в момент времени j, где 1 ^ i ^ | Pl |. Пусть в момент времени j + 1 существует такое 1 ^ k ^ |Pl|, что Nj+1(plfc) = Nj (pl^). Тогда будем говорить, что количество токенов на месте pl^ изменилось в результате активации перехода. Множество переходов будем обозначать T. Определение 6. Дуга —это пара вида (plj,tj), где plj G Pl, tj G T. Множество всех дуг будем обозначать Ac. Каждый переход инцидентен некоторой дуге, задающей правила его активации в зависимости от токенов, расположенных на местах, инцидентных той же дуге. Дуги могут принадлежать к одному из следующих трех типов: — NA — нормальные дуги; — RA — ингибиторные дуги; — 1A — только чтение. Дугу типа i будем обозначать acj. Будем различать два направления дуг: — входящие дуги, соединяющие место pl Pl и переход t T; — исходящие дуги, соединяющие переход t G T и место pl G Pl. Входящие дуги могут принадлежать к любому из трёх перечисленных типов и связаны с функциями чтения или удаления токена с места pl. Исходящие дуги всегда имеют тип NA и связаны с функциями добавления токенов на место pl. Определение 7. Для каждой дуги ac Ac определим значение количественной функции E, задающей для каждых места pl G Pl и перехода t G T, инцидентных дуге ac, количество токенов заданных цветов для возможности активации перехода t, которое либо должно содержать место р/, когда ac — входящая дуга, либо размещается на месте р/, когда ac — исходящая дуга: E(ac) = m1 ■ tk1 + m2 ■ tk2 + ■ ■ ■ + mn ■ tkn, где mj — целые неотрицательные числа; tkj — токены цвета i Е Cp1 (р/); n = |Cp1 (р/) |. Пример 1. Количественная функция E(ac) = 3 ■ (tk1) + 2 ■ (tk2) задаёт для дуги ac условие активации перехода, инцидентного данной дуге: место р/ Е P/, инцидентное дуге, должно содержать три токена цвета tk1 и два токена цвета tk2. Примечание. Если коэффициент mj количественной функции равен 1, то вместо 1 ■ tk будем писать tk. 2. Представление системы семантически осмысленного ролевого управления доступом в виде ЦСП 2.1. Цвета токенов и мест В работе используются следующие цвета для обозначения элементов СК-РУД модели: — USER(u) —идентификатор пользователя. Допустимыми значениями для токенов данного цвета являются все пользователи u Е U; — ROLE (r) —идентификатор роли. Допустимыми значениями для токенов данного цвета являются все роли r Е R; — ADMROLE(ar) —идентификатор административной роли. Допустимые значения: ar Е AR; — SESSION(s) —идентификатор сессии. Допустимые значения: s Е S; — ACOND(car) —идентификатор атрибут-условия назначения роли. Допустимые значения: car Е CA; — COMMAND (command) —идентификатор действия. Допустимые значения: command Е {assign_ro/e, revoke_ro/e, auto_assign_ro/e, auto_revoke_ro/e, take-_ro/e, remove_ro/e, auto_reca/cu/ate}; — ROLE_ACOND(car, r) —сопоставление роли и правила ее автоматического назначения. Множество допустимых значений — декартово произведение ACOND х х ROLE; — USER_ROLE(u, r) — назначение роли пользователю. Множество допустимых значений — USER х ROLE; — UAS(u, r, s) —текущая роль пользователя в сессии. Множество допустимых значений — USER х ROLE х SESSION; — USER_ADMROLE(u,ar) —назначение административной роли. Множество допустимых значений — USER х ADMROLE; — CMD (command, u1, u2, r, s) —токен действия, выполняемого сессией s от имени пользователя u1 . Множество допустимых значений — декартово произведение COMMAND х USER х USER х ROLE х SESSION. Если u1 = u2, то сессия выполняет операцию над пользователем, от имени которого она активирована. Рассмотрим цвета мест и токенов, которые могут на них содержаться: — ETG — генератор токенов. Хранит множество действий, разрешённых в текущем состоянии системы. Для выполнения каждого перехода необходимо, чтобы в ETG содержался токен соответствующего действия. Допустимым цветом токенов для данного места является CMD; — UA — авторизованные роли. Токен (u, r) на этом месте означает, что пользователь u авторизован на роль r. Допустимый цвет токенов USER_ROLE; — AUA — авторизованные административные роли. Токен (u, ar) на этом месте означает, что пользователь u авторизован на административную роль ar. Допустимый цвет токенов USER_ADMROLE; — UAS — активация роли сессией пользователем. Каждый токен (u,r, s) на этом месте означает, что сессия s активирована от имени пользователя u, обладающего ролью r. Допустимый цвет токенов UAS; — RCA — правила назначения ролей. Токен (car, r) означает, что роли r соответствует условие назначения car. Допустимый цвет токенов ROLE_ACOND. 2.2. Количественные и ограничительные функции Количественная и ограничительная функции дуг используются для представления системы ролевого управления доступом в виде ЦСП, так как данные функции представляют возможность моделировать ограничения взаимного исключения ролей и иерархические связи между ролями, задавая пред- и постусловия переходов системы между состояниями. Рассмотрим, каким образом происходит активация перехода, связанного с дугой заданного типа и направления. Для возможности активации перехода t по входящей дуге ac^A = (pl, t) каждое место pl, соединённое с переходом t дугой acNA, должно содержать токенов заданных цветов не меньше, чем указано количественной функцией дуги E(ac), т. е. не менее mj токенов цвета tkj. Переход в момент времени j возможен, если для всех мест pl, инцидентных дуге ac, и для всех цветов i выполняется неравенство Nj(pl, i) ^ mj, где Nj(pl, i) — количество токенов цвета i на месте pl в момент времени j, а коэффициенты mj задаются количественной функцией дуги E(ac). В результате активации перехода токены удаляются из места pl: для всех 1 ^ i ^ n выполняется Nj+1(pl, i) = Nj (pl, i) — mj. Пример 2. Необходимым условием перехода, в результате которого сессия s от имени администратора admin назначит роль r пользователю u, является наличие токена цвета CMD(assign_role, admin, u, r, s) на месте ETG. После активации перехода соответствующий токен удаляется, предотвращая повторное назначение роли. Таким образом, значение количественной функции для входящей нормальной дуги, соединяющей место ETG и переход assign_role, равно (CMD). Переход по исходящей дуге ac^A в момент времени j активируется в результате завершения всех входящих переходов, инцидентных данной дуге. В результате активации перехода по исходящей дуге ac^A = (t,pl) соответствующее количество токенов, равное m1 •tk1 +m2-tk2 + • • -+mn-tkn, добавляется на место pl: Nj+1(pl, i) = Nj (pl, i)+mj. Пример 3. Результатом перехода, в рамках которого сессия от имени администратора admin назначает роль r пользователю u, является помещение токена цвета USER_ROLE(u,r) на место UA, означающее, что данный пользователь авторизован на роль r. Таким образом, значение количественной функции для соответствующей исходящей нормальной дуги равно (USER_ROLE). Для возможности активации перехода t по входящей дуге acRA = (pl, t) в момент времени j каждое место pl, соединённое с переходом t, должно содержать токенов заданного цвета и значения не меньше, чем указано количественной функцией дуги E(acRA). Переход в момент времени j возможен, если для всех мест, инцидентных дуге ac, и для всех цветов i выполняется неравенство Nj (pl, i) ^ mj. В результате активации перехода количество токенов на месте pl не изменяется: Nj+1(pl, i) = Nj (pl, i). Пример 4. Если для некоторой роли r Е R существует роль r' ^ r, то необходимым условием перехода, в результате которого сессия от имени администратора назначит роль r пользователю u, является наличие токенов цвета USER_ROLE(u, r) на месте UA для каждой из ролей-предков r. Каждый из токенов означает, что данный пользователь авторизован на соответствующую роль. После завершения перехода то-кены USER_ROLE остаются на месте UA. Таким образом, значение количественной функции для дуги RA равно | {r' : r' ^ r} | -(USER_ROLE). Для входящей дуги ингибиторного типа ac/A = (р/, t) все коэффициенты mj, за исключением одного mj, равны нулю. Для возможности активации перехода t по входящей дуге ac/A = (р/, t) типа IA каждое место входа р/, соединённое с переходом t, должно содержать не более mj токенов заданного цвета j. В результате активации перехода по дуге ac/A количество токенов на месте р/ не изменяется: Nj+1 (р/, i) = Nj (р/, i). Пример 5. Пусть для роли r существуют статически взаимоисключающие роли. Тогда необходимым условием перехода, в результате которого сессия от имени администратора назначит роль r пользователю u, является отсутствие токенов цвета USER_ROLE(u, r) на месте UA, означающее, что данный пользователь не авторизован на роли, взаимоисключающие с r. Таким образом, значение количественной функции для соответствующей входящей ингибиторной дуги равно (USER_ROLE). Введём определение ограничительной функции дуги G. Определение 8. Множество ограничительных функций дуги G — это множество, включающее в себя ограничения на значения токенов, которые должны находиться на местах, инцидентных входящей дуге, для того чтобы стала возможна инициация перехода, инцидентного дуге. Пусть vp : TK ^ {true, false} — одна из следующих функций: — assignedr : U ^ {true, false} — функция, такая, что assignedr(u) = true тогда и только тогда, когда r Е UA(u); — car : U ^ {true, false}—функция, такая, что car(u) = true тогда и только тогда, когда атрибуты пользователя u Е U соответствуют атрибут-условию назначения роли r Е R; — static_conf/ict_ro/er : R ^ {true, false} — функция, такая, что static_conf/ict_-ro/er (r') = true тогда и только тогда, когда r' является статически взаимоисключающей для r; — dynamic_conf/ict_ro/er : R ^ {true, false} — функция, такая, что dynamic_-conf/ict_ro/er (r') = true тогда и только тогда, когда r' является динамически взаимоисключающей для r; — can_assignar : R ^ {true, false} — функция, такая, что can_assignar(r) = true тогда и только тогда, когда для r Е R и ar Е AR выполняется условие r Е Е can_assign(ar); — can_revokear : R ^ {true, false} — функция, такая, что can_revokear(r) = true тогда и только тогда, когда для r Е R и ar Е AR выполняется условие r Е Е can_revoke(ar); — prec_ro/er : R ^ {true, false} — функция, такая, что prec_ro/er(r') = true тогда и только тогда, когда r > r' в иерархии RH. Пусть Gac : P/ ^ {true, false} — функция, такая, что Gac(p/) = Gac(vp(tk1 , tk'),..., vp(tkm,tkm)), ac Е Ac, р/ Е P/, р/ инцидентно ac, tk1,...,tkm, tk', ...,tk^ Е TK, Ctk(tk1) С Cp1(p/), где 1 ^ i ^ m и Gac(y1,...,ym) —булева функция от m переменных. Тогда {Gac(pl1),... , Gac(plt)} —множество функций, определяющих, при каких условиях может быть активирован переход, инцидентный соответствующей дуге. Если с некоторой входящей дугой ac G Ac связана ограничительная функция Gac, то соответствующий дуге переход t может быть активирован только в том случае, если для всех мест, инцидентных данной дуге, Gac(pl) = true. Количественная и ограничительная функции для i-й дуги j-го типа обозначаются как Eij и Gj соответственно. Пример 6. Пусть для некоторой роли r G R существует r' ^ r. Тогда необходимым условием перехода, в результате которого сессия от имени администратора admin назначит роль rj пользователю u, является наличие на месте UA токена цвета USER_ROLE, имеющего значение (u,rj), для которого assignedri(u) = true. После завершения перехода токен (u,rj) остается на месте UA. Таким образом, значение ограничительной функции входящей дуги RA равно Gac = assignedri (u). Пример 7. Пусть rj,rj- G R — две статически взаимоисключающие роли. Тогда необходимым условием перехода, в результате которого сессия от имени администратора admin назначит роль rj пользователю u, является отсутствие на месте UA токе-на цвета USER_ROLE со значением (u,rj), для которого assignedri(u) = true. Таким образом, значение ограничительной функции входящей ингибиторной дуги равно Ga(—assignedri(u)), где — — оператор логического отрицания. По определению [3], цветная сеть Петри (ЦСП) —это кортеж CPN = (Qc,TK, Pl, T, Ac, Ctfc, Cpi, G, E). Состояние ЦСП в каждый момент времени задается размещением токенов на каждом из Pl мест. Определение 9. Состояние ЦСП Mn называется достижимым из состояния M0, если существует конечная последовательность переходов t0,t1,... ,tn-1 G T, переводящая ЦСП из состояния M0 в состояние Mn. Начальное состояние M0 является достижимым по определению. Переход сети в новое состояние может быть активирован только в том случае, если хотя бы для одного из переходов t T выполнены все предусловия, задаваемые ограничительными и количественными функциями дуг. В данной работе для описания системы СК-РУД используются следующие функции дуг и ограничений: E1NA = CMD(assign_role, u, u', r, s); E2ra = E 11ra = E40ra = E43ra = E58ra = USER_ ADMROLE(u', ra); E 3/a = E19ja = USER_ROLE (u,rc); E 4ra = E 20ra = USER_ROLE (u,rpc); E5/A = E 6na = E9NA = E14/A = E15/A = E17NA = E21/A = E22NA = E 24NA = = E 28/a = E 29/a = E 31NA = E 45/A = E 55/A = E63/A = USER(u); E 7na = E8ra = E 12ra = E 16na = E 23na = E 26ra = E 30na = E 33ra = E41ra = = E48ra = E53/a = E59ra = USER_ROLE(u, r); E10NA = E39na = E57ra = CMD(revoke_role, u, u', r, s); E13/A = E 27/a = E 42ra = E 60RA = USER_ROLE (u,rd); E 18na = E56na = CMD(auto_assign_role, u, system, r, s); E25na = CMD(auto_revoke_role, u, system, r, s); E32na = CMD(take_role, u, u, r, s); E 34ia = UAS (u,rdc,s); E35na = E37na = E38na = E61ra = UAS(u, r, s); E36NA = CMD(remove_role, u, u, r, s); E44/a = E46na = CMD(revoke_role,u,u',rd, s); E47ra = E51ra = CMD(auto_reca/cu/ate, u, system, r, s); E49/a = E50na = CMD(auto_revoke_ro/e, u, system, r, s); E 52ra = ROLE _ACOND(car ,r); E 54/a = USER_ROLE (u,roid); E62/a = CMD(revoke_ro/e, u, u, r, s) + CMD(auto_revoke_ro/e, u, system, r, s); G2 = (u', ra) : can_assignra (r) = true; G3 = (u,rc) : static_conf/ict_ro/er(rc) = false; G4 = (u,rpc) : prec_ro/er(u) = true; G11 = (u',ra) : can_revokera (r) = true; G13 = (u,rd) : prec_ro/er(rd) = false; G19 = (u,rc) : static_conf/ict_ro/er(rc) = false; G20 = (u,rpc) : prec_ro/er(u) = true; G27 = (u,rd) : prec_ro/er(rd) = false; G33 = (u,r) : assignedr(u) = true; G34 = (u,rdc, s) : dynamic_conf/ict_ro/er(rdc) = false; G40 = (u',ra) : can_revokera (r) = true; G42 = (u,rd) : prec_ro/er(rd) = true; G43 = (u',ra) : can_revokera (rd) = true; G48 = (u,r) : car(u) = false; G52 = (car, r) : car(u) = true; G53 = (u,r) : car(u) = true; G54 = (u,roid) : caro1d(u) = false. 3. Переходы сети Петри между состояниями Рассмотрим переходы следующих типов: — назначение роли (assign_ro/e): сессия s администратора u' назначает пользователю u Е U роль r; — отзыв роли (revoke_ro/e): роль r отзывается у пользователя u сессией s администратора u'; — автоматическое назначение роли (auto_assign_ro/e): роль r назначается пользователю u по атрибут-условию car; — автоматический отзыв (auto_revoke_ro/e): роль r отзывается у пользователя u, если он более не удовлетворяет условию car; — перерасчёт списка ролей пользователя при изменении его атрибутов (auto_reca/cu-/ate): в системе создаётся очередь команд на отзыв и назначение ролей в соответствии с новыми атрибутами учётной записи пользователя; — активация (take_ro/e): активация роли r сессией s от имени пользователя u; — деактивация (remove_ro/e): роль r удаляется из списка активных ролей для заданной сессии s пользователя u. Переход может быть совершён в любой момент, если он разрешён в данном состоянии действующими ограничениями. Любой из данных переходов переводит систему в новое состояние. Рассмотрим подробнее переходы в системе ролевого управления доступом, представленной в виде ЦСП. Каждый из рассматриваемых переходов в ЦСП описывается следующим образом: сначала перечисляются входящие дуги с указанием в скобках их типа и связанных количественных и ограничительных функций. Результат перехода описывается с помощью перечисления исходящих дуг с указанием их количественных функций. 3.1. Переход «Назначение роли» Правила активации перехода: — (Дуга с количественной функцией E1 na.) Существует токен (assign_role, u, u', r, s) на месте ETG, означающий, что необходимо выполнить назначение роли r пользователю u сессией от имени администратора u'. — (E2ra). На месте AUA должен существовать токен (u',ra), для которого can_assignra(r) = true (ограничительная функция G2). — (E31A). Место UA не содержит токенов (u,rc), для которых static_conflict_-roler (rc) = true (G3: пользователю не назначены роли, взаимоисключающие с ролью r). — (E4ra). Место UA содержит токены (u,rpc), для которых prec_roler(rpc) = true (G4: пользователю назначены все роли, необходимые для назначения роли r). — (E5/a). Место UB не содержит токена (u) (над пользователем в данный момент не выполняется никаких действий). Результат перехода: данный переход (E7Na) помещает токен (u, r) на место UA, что означает авторизацию пользователя u на роль r. На время выполнения перехода на место UB помещается токен (u) (E6na), чтобы блокировать одновременное выполнение любых других действий над пользователем u. После активации перехода команда (assign, u, u', r, s) удаляется с места ETG (E 1Na). После выполнения перехода (E8Ra) токен (u) удаляется с места UB (E9Na). 3.2. Переход «Отзыв роли» Правила активации перехода: — (E10NA). Существует токен (revoke_role, u, u', r, s) на месте ETG, означающий, что необходимо выполнить отзыв роли r у пользователя u сессией от имени администратора u'. — (E11RA). На месте AUA существует токен (u',ra), для которого can_revokera(r) = = true (G11). — (E 12ra). Место UA содержит токен (u,r) (нельзя отозвать роль, если она не назначена). — (E 13/a). Место UA не содержит множество токенов {(u,r^)}, таких, что prec_roler(rd) = true (G13: нельзя отозвать роль, предварительно не отозвав роли, которые от неё зависят). — (E141A). Место UAS не содержит токена (u,r, s) (G14: нельзя отозвать роль, если она активирована сессией пользователя). — (E 15/a). Место UB не содержит токена (u) (над пользователем в данный момент не выполняется никакой операции). Результат перехода: данный переход (E 17na) удаляет токен (u, r) с места UA, что означает отзыв роли r у пользователя u. На время выполнения перехода на место UB помещается токен (u) (E 16na), чтобы блокировать одновременное выполнение любых других действий над пользователем u. После активации перехода команда (revoke_role, u, u', r, s) удаляется с места ETG (E10NA). После выполнения перехода токен (u) удаляется с места UB. 3.3. Переход «Автоматическое назначение роли» Правила активации перехода: — (E 18na). Существует токен (auto_assign_ro/e, u, system, r, s) на месте ETG, означающий, что необходимо выполнить назначение роли r пользователю u сессией от имени пользователя system. — (E 19/a). Место UA не содержит токенов (u, rc), для которых static_conf/ict_-ro/er (rc) = true (G19: пользователю не назначены роли, взаимоисключающие с ролью r). — (E20ra). Место UA содержит токены (u,rpc), для которых prec_ro/er(rpc) = true (G20: пользователю назначены все роли, необходимые для назначения роли r). — (E21/a). Место UB не содержит токена (u) (над пользователем в данный момент не выполняется никаких действий). Результат перехода: данный переход (E23Na) помещает токен (u, r) на место UA, что означает авторизацию пользователя u на роль r. На время выполнения перехода на место UB помещается токен (u) (E22na), чтобы блокировать одновременное выполнение любых других действий над пользователем u. После активации перехода команда (auto_assign_ro/e, u, system, r, s) удаляется с места ETG (E 18na). После выполнения перехода токен (u) удаляется с места UB (E24Na). 3.4. П е р е х о д « А в т о м а т и ч е с к и й о т з ы в р о л и » Правила активации перехода: — (E25na). Существует токен (auto_revoke_ro/e, u, system, r, s) на месте ETG, означающий, что сессии от имени пользователя system необходимо выполнить отзыв роли r у пользователя u. — (E26ra). Место UA содержит токен (u,r) (нельзя отозвать роль, если она не назначена). — (E27/a). Место UA не содержит множество токенов {(u,r^)}, таких, что prec_ro/er (r^) = true (нельзя отозвать роль, предварительно не отозвав роли, которые от неё зависят). — (E28/a). Место UAS не содержит токена (u,r, s) (G14: нельзя отозвать роль, если она активирована одной из сессий пользователя). — (E29/a). Место UB не содержит токена (u) (над пользователем в данный момент не выполняется никаких действий). Результат перехода: данный переход (E31Na) удаляет токен (u, r) с места UA, что означает отзыв роли r у пользователя u. На время выполнения перехода на место UB помещается токен (u) (E30na), чтобы блокировать одновременное выполнение любых других действий над пользователем u. После активации перехода команда (auto_revoke_ro/e, u, system, r, s) удаляется с места ETG (E25NA). После выполнения перехода токен (u) удаляется с места UB. 3.5. Переход «Активация роли» Правила активации перехода: — (E32na). Существует токен (take_ro/e, u, u, r, s) на месте ETG, означающий, что сессия s от имени пользователя u активирует роль r. — (E33ra). Место UA содержит токен (u,r) (сессия пользователя может активировать только те роли, на которые он авторизован). — (E34/a). Место UAS не содержит множество токенов {(u,rdc,s)}, таких, что dynamic_conf/ict_ro/er (rdc) — true (G34: сессия пользователя не может активировать роль r, если для этой сессии в настоящий момент активированы роли, динамически взаимоисключающие с ролью r). Результат перехода: данный переход (E35Na) помещает токен (u,r, s) на место UAS, что означает активацию роли r сессией s от имени пользователя u. 3.6. Переход «Деактивация роли» Правила активации перехода: — (E36NA). Существует токен (remove, u, u, r, s) на месте ETG, означающий, что сессия s пользователя u деактивирует роль r. — (E37Na). Место UAS содержит токен (u, r, s) (сессия пользователя не может деак-тивировать роль, которая не активирована для данной сессии). Результат перехода: данный переход (E38Na) удаляет токен (u, r, s) с места UAS, что означает деактивацию роли r сессией s от имени пользователя u. 3.7. Переход «Перерасчет зависимых ролей при удалении роли» Правила активации перехода: — (E39NA). Существует токен (revoke_role, u, u', r, s) на месте ETG, означающий, что необходимо выполнить команду отзыва роли r у пользователя u сессией от имени администратора u'. — (E40ra). На месте AUA существует токен (u',ra), для которого can_revokera(r) = = true (G40). — (E41ra). Место UA содержит токен (u,r) (нельзя отозвать роль, если она не назначена). — (E42ra). Место UA содержит хотя бы один токен (u, rd), такой, что prec_roler (rd) = = true. — (E43ra). На месте AUA существует токен (u', r^), для которого can_revoker^ (rd) = = true (G43). — (E441A). Не существует токена (revoke_role, u, u', rd, s) на месте ETG. — (E45/a). Место UB не содержит токена (u) (над пользователем в данный момент не выполняется никаких действий). Результат перехода: данный переход (E46NA) добавляет токен (revoke, u, u', rd, s) на место ETG, что означает команду на отзыв роли r^, зависимой от роли r, у пользователя u. 3.8. Переход «Перерасчет ролей для удаления при изменении атр ибутов» Правила активации перехода: — (E47ra). Существует токен (auto_recalculate, u, system, r, s) на месте ETG, означающий, что атрибуты учётной записи пользователя u были изменены и требуется перерасчет его ролей. — (E48Ra). Место UA содержит хотя бы один токен (u,r), такой, что car(u) = false. — (E491A) Не существует токена (auto_revoke_role, u, system, r, s) на месте ETG. Результат перехода: данный переход (E50Na) добавляет токен (auto_revoke_-role, u, system, r, s) на место ETG, что означает команду на автоматический отзыв роли r у пользователя u. 3.9. Переход «Перерасчет ролей для назначения п р и и з м е н е н и и а т р и б у т о в » Правила активации перехода: — (E51ra). Существует токен (auto_reca/cu/ate, u, system, r, s) на месте ETG, означающий, что атрибуты учётной записи пользователя u были изменены и требуется перерасчет его ролей. — (E52Ra). Место RCA содержит хотя бы один токен (car, r), такой, что car (u) = true. — (E53/a). Место UA не содержит токен (u,r), такой, что car(u) = true. — (E54/a). Место UA не содержит ни одного токена (u,ro1d), такого, что caro1d(u) = = false (данное условие гарантирует, что расчет назначений ролей начнётся только после окончания отзыва всех старых ролей). — (E55/a). Место UB не содержит токена (u) (над пользователем в данный момент не выполняется никаких действий). Результат перехода: данный переход (E56Na) добавляет токен (auto_assign_ro/e, u, system, r, s) на место ETG, что означает переход «Автоматическое назначение роли» r пользователю u. 3.10. Переход «Удаление роли из списка активных в результате её отзыва у пользователя» Правила активации перехода: — (E57ra). Существует токен (revoke_ro/e, u, admin, r, s) на месте ETG, означающий, что необходимо выполнить команду отзыва роли r у пользователя u сессией от имени администратора admin. — (E58ra). На месте AUA существует токен (admin,ra), для которого can_revo-kera (r) = true (G58). — (E59ra). Место UA содержит токен (u,r) (нельзя отозвать роль, если она не назначена). — (E60RA). Место UA не содержит токенов (u,rd), таких, что prec_ro/er(rd) = true. — (E61ra). Место UAS содержит токен (u, r, s) (роль в данный момент времени активирована). — (E62/a). Не существует токенов (remove_ro/e, u, u, r, s) и (remove_ro/e, u, system, r, s) на месте ETG. — (E63/a). Место UB не содержит токена (u) (над пользователем в данный момент не выполняется никаких действий). Результат перехода: данный переход (E64Na) добавляет токен (remove_ro/e, u, system, r, s) на место ETG, что означает команду на деактивацию роли r, активированной пользователем u в рамках сессии s. Таким образом, описаны переходы между состояниями в системе семантически осмысленного ролевого управления доступом, заданной в рамках СК-РУД-модели. В отличие от системы, основанной на классической модели RBAC, возможность осуществления перехода зависит не только от текущего состояния системы, но и от переходов, выполненных на предыдущих шагах. 4. Доказательство безопасности системы семантически осмысленного ролевого управления доступом, представленной в виде ЦСП Представление системы ролевого управления доступа в виде ЦСП позволяет осуществить формальное доказательство безопасности системы. Назовём состояние системы безопасным в рамках СК-РУД-модели, если оно не противоречит ограничениям, накладываемым на составляющие её множества и функции, и каждому пользователю u G U назначены только роли, не противоречащие условиям CR и CA. Переформулируем определение с учётом перечисленных в п. 1 элементов СК-РУД-модели. Определение 10. Состояние системы в рамках СК-РУД-модели называется безопасным, если в нем выполняются следующие свойства: — P1 : у каждого пользователя активны только те роли, на которые он авторизован: в каждый момент времени для каждой сессии s G S выполняется условие roles(s) С С UA(user(s)) (условие определения функции roles); — P2: если prec_roler(r') = true, то роль r может быть назначена пользователю u только в том случае, если он также авторизован на роль r' (определение 3 иерархии «по предусловию» и определение предусловий CR [4]); — P3: пользователь может быть авторизован только на те атрибут-роли, атрибут-условиям которых соответствуют значения его атрибутов: для любого пользователя u G U если r G UA(u), то car(u) = true (ограничение в определении 4 атрибут-условия); — P4: пользователь не может быть одновременно авторизован на две статически взаимоисключающие роли: для любого пользователя u G U если r1,r2 G UA(u), то static_con/lict_roleri (r2) = false (определение 1 статически взаимоисключающих ролей); — P5: у любой сессии пользователя не могут быть одновременно активированы две динамически взаимоисключающие роли: для сессии любого пользователя s S если r1,r2 G roles(s), то dynamic_con/lict_roleri(r2) = false (определение 2 динамически взаимоисключающих ролей). Определение 11. Переход системы из состояния в состояние называется безопасным, если он удовлетворяет следующим ограничениям: — T1: переход «Активация роли» сессией пользователя может быть осуществлён только для тех ролей, на которые соответствующий пользователь авторизован в настоящий момент времени; — T2: переход «Назначение роли» r пользователю u сессией от имени администратора admin может произойти только в том случае, если can_assignr(admin) = true; — T3: переход «Назначение роли» r пользователю u может быть осуществлён только в том случае, если prec_roler(r2) = true и пользователь в настоящий момент времени авторизован на роль r2; — T4: переход «Назначение роли» r пользователю u может быть осуществлён только в том случае, если он в настоящий момент времени не авторизован на одну или более статически взаимоисключающих ролей; — T5: переход «Активация роли» r пользователю u может быть осуществлён только в том случае, если в настоящий момент времени в этой сессии не активны роли, динамически взаимоисключающие с r; — T6: переход «Отзыв роли» r у пользователя u сессией от имени администратора admin может быть осуществлён только в том случае, если can_revoker (admin) = = true; — T7: переход «Отзыв роли» r2 у пользователя u может быть осуществлён только в том случае, если prec_roler (r2) = true и пользователь в настоящий момент времени авторизован на роль r. Утверждение 1. Для системы ролевого управления доступом, начальное состояние M0 которой является безопасным, все состояния M, достижимые из M0 в результате конечного числа переходов, удовлетворяют свойству P1 . Для пользователя могут быть активными только те роли, на которые он авторизован. Доказательство. Входящая дуга A33 между UA и переходом take_ro/e даёт возможность выполнить переход take_ro/e для пользователя u только в том случае, если токен (u,ry) находится на месте UA (гарантирует выполнение ограничения T1). Наличие токена (u, ry) на месте UA означает, что пользователь u авторизован на роль ry. Следовательно, множество ролей, активированных сессией пользователя, является подмножеством множества ролей, на которые он авторизован. ■ Утверждение 2. Для системы ролевого управления доступом, начальное состояние M0 которой является безопасным, все состояния M, достижимые из M0, удовлетворяют свойству P2. Доказательство. Рассмотрим ограничение последовательного назначения ролей, согласно которому, если некоторая роль rx имеет зависимость от назначения подмножества ролей, то роль rx может быть назначена пользователю только в том случае, если все роли ry, такие, что prec_ro/erx(ry) = true, назначены данному пользователю. Предположим, что ограничение не выполняется для некоторого состояния M, достижимого из M0. Предположим, что {r1, r2,... , rn} — такие роли, что prec_ro/erx (rj) = true, 1 ^ i ^ n. Согласно предположению, в состоянии M место UA содержит токен (u,rx), но не содержит все токены множества {(u,rj) : 1 ^ i ^ n}. Предположим, что M — первое состояние, в котором роль rx назначена пользователю. Это означает, что состояние M было достигнуто при выполнении перехода assign_ro/e (auto_assign_ro/e) из состояния M', в котором токены (u,rj) также отсутствовали на месте UA. Однако дуга A3 (A19) и соответствующее ограничение G3 (G19) prec_ro/erx (rj) не позволяет активировать переход assign_ro/e (auto_assign_ro/e), гарантируя выполнение ограничения T3. Следовательно, состояние M не может быть достигнуто. Противоречие. ■ Утверждение 3. Для системы ролевого управления доступом, начальное состояние M0 которой является безопасным, все состояния M, достижимые из M0, удовлетворяют свойству P3. Доказательство. Рассмотрим ограничение последовательного отзыва ролей, согласно которому, если для ролей из множества {r1, r2,... , rn} роль rx входит в предварительное условие их назначения, то роль rx может быть отозвана только в том случае, если все роли {r1, r2,..., rn}, такие, что prec_ro/eri(rx) = true, отозваны у пользователя. Предположим противное: ограничение не выполняется для некоторого состояния M, достижимого из M0. Пусть {r1, r2,... , rn} — такие роли, что prec_ro/eri (rx) = true, 1 ^ i ^ n. Согласно предположению, в состоянии M место UA содержит токен (u,rx), но не содержит всех токенов из множества {(u,rj)}, где 1 ^ i ^ n. Предположим, что M — первое состояние, в котором роль rj, 1 ^ i ^ n, отозвана у пользователя. Это означает, что состояние M было достигнуто при выполнении перехода revoke_ro/e (auto_revoke_ro/e) из состояния M', в котором все токены (u,rj) присутствовали на месте UA. Однако дуга A13 (A27) и соответствующее ограничение G13 (G27) prec_ro/eri (rx) не позволяет активировать переход revoke_ro/e (auto_revoke_ro/e), гарантируя выполнение ограничения T7. Следовательно, состояние M не может быть достигнуто. Противоречие. ■ Утверждение 4. Для системы ролевого управления доступом, начальное состояние M0 которой является безопасным, все состояния M, достижимые из M0, удовлетворяют свойству P4. Доказательство. Предположим противное: в системе существует пользователь u, для которого ограничение на запрет одновременного назначения статически взаимоисключающих ролей не выполняется, т. е. u может быть одновременно авторизован на роли rx и ry, такие, что static_con/lict_rolerx (ry) = true. Следовательно, токены (u,rx) и (u,ry) могут одновременно находиться на месте UA. Пусть M0 — состояние системы непосредственно перед выполнением перехода assign_role, добавляющего токен (u, ry) на место UA. Пусть также в состоянии M0 пользователь u авторизован на роль rx (токен (u,rx) находится на месте UA, а токен (u, ry) отсутствует на данном месте). Пусть ry — первая роль, для которой не выполняется ограничение P4. Ингибиторная дуга A3 связана с функцией E3 : (u, rc) и ограничением перехода G3: static_con/lict_roler(rc) = true, отсюда следует, что выполняется условие T4 и переход assign_role не может быть активирован. Следовательно, свойство P4 выполняется для любого состояния M, достижимого из M0. ■ Утверждение 5. Для системы ролевого управления доступом, начальное состояние M0 которой является безопасным, все состояния M, достижимые из M0, удовлетворяют свойству P5. Доказательство. Предположим противное: в системе существует пользователь u, для которого ограничен

Ключевые слова

ролевое управление доступом, автоматизация управления ролями, сети Петри, RBAC, automated role management

Авторы

ФИООрганизацияДополнительноE-mail
Семенова Наталья АндреевнаМосковский государственный институт электроники и математики (г. Москва)аспиранткаnatasha_sem@inbox.ru
Всего: 1

Ссылки

Семенова Н. А. Семантическая ролевая модель управления доступом // Прикладная дискретная математика. 2012. №2(16). С. 50-64.
http://csrc.nist.gov/rbac/rbacSTD-ACM.pdf — National Institute of Standards and Technology, Proposed Standard for Role-Based Access Control.
Котов В. Е. Сети Петри. М.: Наука, 1984. 160с.
Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. М.: Горячая линия-Телеком, 2011. 320 с.
 Представление системы семантически осмысленного ролевого управления доступом в виде цветной сети Петри | ПДМ. 2013. № 1(19).

Представление системы семантически осмысленного ролевого управления доступом в виде цветной сети Петри | ПДМ. 2013. № 1(19).

Полнотекстовая версия