Security analysis of systems with simple trajectories functioning within framework of the base role dp-model.pdf На основе базовой ролевой ДП-модели (БР ДП-модели) [1, 2] рассматриваютсяусловия передачи прав доступа и реализации информационных потоков по памяти дляслучая, когда на траекториях функционирования системы субъект-сессии не получаютдоступа владения друг к другу с использованием информационных потоков по памятик функционально ассоциированным с субъект-сессиями сущностям.Определение 1. Пусть G0 = (PA0, user0, ro/es0, A0, F0, HEo) -состояние системыE(G*, OP), в котором существуют пользователь x . U0 и право доступа к сущности(e,a) . Р0. Определим предикат simp/e_can_share((e, a), x, G0), который будетистинным тогда и только тогда, когда существуют состояния G1, . .. , Gn и правилапреобразования состояний op1,...,o p N, такие, что G0 hopi G1 Ьор2 ... hopN GN, гдеN ^ 0, является простой траекторией без кооперации доверенных и недоверенныхсубъект-сессий для передачи прав доступа, и существует субъект-сессия . Sn , такая,что userN(sx) = x и выполняется условие (e,a) . de_facto_rightsN(sx).Определение 2. Пусть G0 = (PA0, user0, ro/es0, A0, F0, HEo) -состояние системыE(G*, OP), в котором существуют сущности или недоверенные пользователиx,y . N^ U E0, где x = у. Определим предикат simp/e_can_write_memory(x, у, G0),который будет истинным тогда и только тогда, когда существуют состояния G1,. .. , Gnи правила преобразования состояний op1, ... , opN, такие, что G0 hopi ... GN, гдеN ^ 0, является простой траекторией без кооперации доверенных и недоверенныхсубъект-сессий для передачи прав доступа, и выполняется условие (x', у', writem) . ,где верно следующее: если x . E0, то x' = x; если x . N^, то x' . SN и userN(x') = x;если у . E0, то у' = у; если у . N^, то у' . SN и userN(у') = у.В рамках определений 1 и 2 возможно обоснование следующих теорем.Теорема 1. Пусть G0 = (PA0, user0, ro/es0, A0, F0, HEo) -состояние системыE(G*, OP), в котором существуют недоверенный пользователь x . Nu и право доступак сущности (e,a) . Р0. Предикат simp/e_can_share((e, a), x, G0) является истиннымтогда и только тогда, когда выполняется одно из следующих условий:1. Выполняется условие (e,.) . PA0(UA0(x)), где . . {a, ownr}.2. Существует субъект-сессия или недоверенный пользователь у . Nu U S0, истиненпредикат simp/e_can_access_own(x, у, G0), и выполняется одно из условий:- или у . Nu и (e,a) . PA0(UA0(y));- или у . NS П S0 и (e,a) . PA0(UA0(user0(y)));- или у . П S0 и (e, a) . PA0(ro/es0(y)).3. Существуют последовательности недоверенных субъект-сессий или недоверенныхпользователей x 1, . . . , x m . Nu U (Ns П S0), субъект-сессий или недоверенныхпользователей у1, ... ,ym . Nu U S0, где m ^ 2, таких, что x 1 = x, yi . is/and(xi), где1 ^ i ^ m, и выполняется одно из условий:- или ym . Nu и (e, ownr) . PA0(UA0(ym));- или ym . Ns П S0 и (e, ownr) . PA0(UA0(user0(ym)));- или ym . Ls П S0 и (e, ow n ) . PA0(ro/es0(ym)).При этом справедливо равенство is_simp/e_bridge(xm, ym-1, ym) = true, и длякаждого 2 ^ i ^ m справедливо равенство или is_bridge(xi, yi- 1, yi) = true, илиis_simp/e_bridge(xi, yi-1, yi) = true.Теорема 2. Пусть G0 = (PA0, user0, ro/es0, A0, F0, HEo) -состояние системыE(G*,OP), в котором существуют сущности или недоверенные пользователиx,y . N^ U E0, где x = у. Предикат simp/e_can_write_memory(x, у, G0) истинентогда и только тогда, когда существует последовательность недоверенных пользователейили сущностей ei , . . . , em G Nj U E0, где ei = x, em = y и m ^ 2, таких, чтовыполняется одно из условий:1. m = 2 и (x', y', writem) G F0, где выполняются условия:- если x G E0, то x' = x;- если x G Njj , то x' G S0 и user0(x') = x;- если y G E0, то y' = y;- если y G Nj , то y' G S0 и user0(y') = y.2. Для каждого i = 1 ,..., m - 1 выполняется одно из условий:- ei G Nj U S0, ei+i G Nj U E0 и (ei, e'+i, writem) G F0, где верно следующее: если ei G S0, то ej = ei; если ei G Nj , то ej G S0 и user0(ej) = ei; если ei+i G E0, то ei+i = ei+i; если ei+i G N j , то ei+i G S0 и user0(ei+i) = ei+i;- ei G Nj U S0, ei+i G E0 \ S0 и истинен предикат simp/e_can_share((ei+i , a), ei, G0),где a G {writer, appendr}, и верно следующее: если ei G Nj , то ei = ei; если ei G S0, то ei = user0(ei);- ei+i G Nj US0, ei G E0\S0 и истинен предикат simp/e_can_share((ei, readr), ei+i , G0),где верно следующее: если ei+i G Nj , то ei+i = ei+i; если ei+i G S0, то ei+i = user0(ei+i);- ei G Nj U (Ns П S0), ei+i G Nj U S0 и истинен simp/e_can_access_own(ei, ei+i , G0),где верно следующее: если ei G Nj , то ei = ei; если ei G NS П S0, то ei = user0(ei);- ei+i G Nj U(NsПS0), ei G Nj US0 и истинен предикат simp/e_can_access_own(ei+i ,ei, G0), где верно следующее: если ei+i G Nj , то ei+i = ei+i; если ei+i G Ns П S0, то ei+i = user0(ei+i).

Скачать электронную версию публикации