Анализ безопасности информационных потоков по памяти в компьютерных системах с функционально и параметрически ассоциированнымисущностями | ПДМ. 2009. № 1(3).

Анализ безопасности информационных потоков по памяти в компьютерных системах с функционально и параметрически ассоциированнымисущностями

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

Security analysis of the information flows by memory in the computersystems with functional and parametric associated en.pdf Одной из современных моделей анализа безопасности компьютерных систем (КС) с дискреционным управлением доступа является ДП-модель с ее расширениями [1]. Дальнейшее изложение будет вестись на основе работы [1] с учетом всех определений, обозначений и теорем в ней. Сущность называется функционально-ассоциированной с субъектом, если она определяет вид преобразования данных, выполняемого этим субъектом. В ДП-моделях с функционально-ассоциированными с субъектами сущностями (ФАС ДП-моделях) анализируется ситуация, когда реализация информационного потока по памяти к сущности, функционально-ассоциированной с субъектом, приводит к изменению вида преобразования данных, реализуемого этим субъектом.В то же время в современных КС возможна реализация информационного потока по памяти от сущности, позволяющая получить права доступа различных субъектов, в том числе и доверенных. Такие сущности являются параметрически-ассоциироваными с субъектами КС. Например, получение субъектом-нарушителем доступа на чтение к конфигурационному файлу или реестру, в котором хранится пароль или хэш-значение пароля субъекта КС, позволяет субъекту-нарушителю получить право доступа владения к последнему субъекту. Кроме того, в настоящее время дополнительно к классическим угрозам нарушения конфиденциальности, целостности и доступности информации рассматривают угрозу раскрытия параметров КС - возможность идентификации параметров, функций безопасности и свойств КС, знание которых позволяет реализовать нарушение безопасности [2]. Например, чтение сообщения, выдаваемого субъектом-процессом при подключении к нему, позволяет нарушителю идентифицировать программное обеспечение (ПО), реализующее данный субъект-процесс КС, и получить права доступа последнего, используя известные уязвимости в ПО.Таким образом, для обеспечения возможности анализа получения субъектом права доступа владения к другому субъекту с использованием информационного потока от сущности, параметрически-ассоциированной с последним, следует построить расширение ФАС ДП-модели, охватывающее информационные потоки указанного вида и отражающее возможность получения субъектом права доступа владения к другому субъекту в современных КС. Решение этой задачи и является целью данной работы.118Д. Н. КолеговДля этого вводится определение параметрически-ассоциированных сущностей с субъектами в КС, на их основе строится ДП-модель с функционально- и параметрически-ассоциированными с субъектами сущностями, которая является требуемым расширением ФАС ДП-модели, и в рамках этой модели формулируются и обосновываются необходимые и достаточные условия получения недоверенным субъектом права доступа владения к другому субъекту без кооперации с ним.1. ДП-модель с функционально- и параметрически-ассоциированнымис субъектами сущностямиОпределение 1. Пусть G = (S,E,R U A U F, Я) - состояние КС T,(G*,OP). Сущность е Е Е будем называть параметрически-ассоциированной с субъектом s E S в состоянии G, если чтение данных в сущности е субъектом z E S позволяет ему получить право владения к субъекту s в этом или последующих состояниях КС.Замечание 1. Сущность е Е Е, параметрически-ассоциированная с субъектом s E S, содержит аргументы операций преобразования данных, выполняемого субъектом s в этом или последующих состояниях КС.Замечание 2. В множество сущностей, параметрически-ассоциированных с субъектом s E S, могут входить сущности, на которые субъект s не имеет прав доступа. Например, сущность-пароль, параметрически-ассоциированная с недоверенным субъектом-пользователем в ОС семейства UNIX, хранится в файле /etc/shadow, правами доступа к которому могут обладать только доверенные субъекты-процессы данной ОС [3]. Кроме того, возможно создание субъектов ОС, которые препятствовали бы доступу субъектов к некоторым критичным сущностям КС, несмотря на наличие необходимых прав доступа данных субъектов к этим сущностям [4].Замечание 3. Существуют сущности, параметрически-ассоциированные с субъектом, которые не являются функционально-ассоциированными с ним. Примером такой сущности является раздел реестра ОС семейства Windows, содержащий информацию об установленных обновлениях ОС узла. Также существуют сущности, параметрически-ассоциированные с субъектом, которые являются функционально-ассоциированными с ним. Так, зная идентификатор сессии пользователя web-приложения, возможно получить его права доступа; с другой стороны, удаление данного идентификатора приводит к закрытию сессии пользователя.Наличие у субъекта данных о параметрах функционирования другого субъекта КС может позволить получить первому субъекту право доступа владения ко второму субъекту. При этом первому субъекту необходимо иметь возможность реализовать информационный поток по памяти к некоторому субъекту, позволяющему получить права доступа ко второму субъекту. Например, при получении субъектом-нарушителем пароля доверенного субъекта первому необходимо иметь возможность записи пароля в сущность-интерфейс КС. С учетом того, что доверенные субъекты не участвуют в реализации информационных потоков по времени, и того, что в современных КС, как правило, реализация информационного потока по времени от сущности, параметрически-ассоциированной с субъектом, не приводит к получению другим субъектом права доступа владения к первому, будем считать, что в КС выполняется следующее предположение.Предположение 1. Информационный поток по времени от сущности, параметрически-ассоциированной с субъектом, не приводит к получению другим субъ-Анализ безопасности информационных потоков119ектом права доступа владения к первому субъекту. Если субъект реализовал информационный поток по памяти от сущности, параметрически-ассоциированной с другим субъектом, к себе, то первый субъект получает право доступа владения ко второму субъекту. Множество сущностей, параметрически-ассоциированных с субъектом, не изменяется в процессе функционирования КС.Через ]s[c Е обозначим множество всех сущностей, параметрически-ассоциированных с субъектом s. При этом будем считать, что s e]s[.В соответствии с данным предположением модифицируем определение ФАС ДП-модели для возможности анализа условий получения субъектом права доступа владения к другому субъекту с использованием реализации информационного потока по памяти от сущности, параметрически-ассоциированной с последним субъектом. Модифицированную ФАС ДП-модель будем называть ДП-моделъю с функционалъно-и параметрически-ассоциированными с субъектами сущностями, или ФПАС ДП-моделью. Модификация состоит в добавлении к правилам преобразования состояний ФАС ДП-модели правила know(x,y, z), определенного в таблице: аргументом операции является состояние G, значением - состояние G', параметрами - сущности х, у, z.Условия и результаты применения правила know(x, у, z)ФПАС ДП-моделиПравилоИсходное состояние G = (S,E,RUAUF,H)Результирующее состояние G' = (S',E',R'uA'UF',H')know(х, у, z)х,у Е S,z Е E,z Е ]у[ и или х = z, или (z,x,writem) E FS' = S,E' = E,A' = A,H' = H,F' = F,R' = RU (x, y, ownr)Замечание 4. Правило know(x,y, z) является монотонным, то есть применение данного правила не приводит к удалению ребер или вершин из графа доступа.Замечание 5. Как и правило control{x,y,z) ФАС ДП-модели, правило know(x,y, z) отражает возможность одним субъектом получить право доступа владения к другому субъекту путем реализации информационного потока.Рассмотрим условия получения недоверенным субъектом права доступа владения ownr к другому субъекту без кооперации с ним для случая, когда в КС T.(G*,OP) используются правила преобразования состояний know{x,y,z) и control{x,y,z).2. Анализ условий получения субъектом права доступа владенияк другому субъектуОпределение 2. Траекторию функционирования КС S(G*, OP) будем называть траекторией без кооперации доверенных и недоверенных субъектов для передачи прав доступа, если при ее реализации используются монотонные правила преобразования состояний, и доверенные субъекты:•·не дают недоверенным субъектам права доступа к сущностям;•·не берут у недоверенных субъектов права доступа к сущностям;•·используя информационные потоки по памяти к сущностям, не получают право доступа владения к субъектам;•используя информационные потоки по памяти от сущностей, не получают право доступа владения к субъектам.•·120•·Д. Н. Колегов•·Таким образом, в КС T.(G*,OP) на траекториях без кооперации доверенных и недоверенных субъектов для передачи прав доступа доверенные субъекты:•·не инициируют выполнения следующих правил преобразования состояний: take_right(ar,u,x,e), grant_right(ar,u,x,e), control (и, у, z), know (и, у, z);•·доверенные субъекты могут выполнять монотонные правила преобразования состояний: own_take(ar,u,e), create_entity(и, е,е'), create_subject(u,e,e'), rename_entity(и, е,е'), access _read(u,e), access_write(u,e), access _append(u,e), find(u,e,e'), post(u,e,e'), pass(u,e,e') с условиями и результатами применения в соответствии с правилами преобразования БК ДП-модели,•·где и Е Ls - доверенный субъект, х Е Ns - недоверенный субъект, у - субъект, что z Е]у[ или z Е [у], z, е, е' - сущности, ar E Rr - право доступа.•·Определение 3. Траекторию функционирования КС S(G*, OP) будем называть траекторией без кооперации доверенных и недоверенных субъектов для передачи прав доступа и реализации информационных потоков, если она является траекторией без кооперации доверенных и недоверенных субъектов для передачи прав доступа, и при ее реализации используются правила преобразования состояний:•·take_right(ar,x,y,z), grant_right(ar,x,y, z), own_take(ar,x,y) с условиями и результатами применения в соответствии с правилами преобразования базовой ДП-модели;•·create _entity(x ,y, z), create_subject(x, у, z), rename _entity(x ,y, z), flow(x,y,y', z), find(x,y,z), post(x,y, z), pass(x,y, z), access _read(x,y), access_write(x,y), access_append(x,y) с условиями и результатами применения в соответствии с правилами преобразования БК ДП-модели;•·control(x, у, z), know(x, у, z) с условиями и результатами применения в соответствии с правилами преобразования ФАС ДП-модели и таблицей.Определение 4. Пусть имеются Go = (So, Eq, Rq U Aq U Fo, Ho) - состояние КС S(G*, OP), недоверенный субъект х Е NsdSo ж у Е So, где х ф у. Определим предикат can_steal_own(x,y,Go, Ls), который будет истинным тогда и только тогда, когда существуют состояния G\,... , Gn = (Sn, En, Ддг U An U F^, H^) и правила преобразования состояний ор\,... , opN такие, что Go \~ap\ G\ \~ap2 ■ ■ ■ \~opN Gn является траекторией без кооперации доверенных и недоверенных субъектов для передачи прав доступа и реализации информационных потоков и (х, у, ownr) E Rn, где N ^ 0. При этом в последовательности правил ор\,... , орм отсутствуют правила вида grant_right(ar, у, s, e), take_right(ar,y, s,e), control(y, s,e'), know(y, s,e'), где ar E Rr, s E Ns Г\ S0, e,e' E E0 и е' Е [s] или е' E]s[ (субъект у не передает другим субъектам любые имеющиеся у него права доступа к любым сущностям и не получает с использованием правил control(x,y,z) и know(x,y,z) право доступа владения ownr к другим субъектам).Определение 5. Пусть имеются Go = (So, E0, Ro U A0 U F0, H0) - состояние КС S(G*, OP), недоверенный субъект х Е NsdSo и у Е So, где х ф у. Определим предикат directly_can_share_own(x, у, Go, Ls), который будет истинным тогда и только тогда, когда существует последовательность субъектов s\,... , sm Е So, где s\ = х, sm =уи т ^ 2, таких, что для каждого % = 1,..., т - 1 выполняется одно из условий:1))Si E Ns Г) So, Si E [si+i] или Si e]si+i[;2))истинен предикат can_share(ownr, Si, Sj+i, Go, Ls)',3))существует сущность е Е [sj+i], что предикат can_write_memory(si,e,Go, Ls) является истинным;1)Анализ безопасности информационных потоков1214) существует сущность е g]sj+i[, что предикат can _write _memory{e, Si,Go, Ls) является истинным.Лемма 1. Пусть имеются Go = (So,Eo,Ro U Aq U Fo,Hq) - состояние КС Tj(G*,OP), недоверенный субъект x G Ns Г\ So и у G 5*0, где х ф у, и истинен предикат directly_can_share_own(x, у, Go, Ls). Тогда истинен предикат can_share_own(x, у, G0, Ls).Доказательство. Пусть истинен предикат directly_can_share_own(x, у, Go, Ls), тогда по определению 5 существует последовательность субъектов s\,... , sm в So, где S\ = x, sm = у и т ^ 2, таких, что для каждого i = 1, ...,т - 1 выполняется одно из условий 1-4 определения 5. Докажем, что для такой последовательности S\,... ,sm предикат can_share_own(x,y,Go,Ls) является истинным. Проведем доказательство этого утверждения индукцией по длине т.Пусть т = 2, тогда возможно четыре случая.Первый случай: х G Ns Г\ So, x G [у] или х Е]у[. Если х G [у], то пусть opi = control{x,y,x). Тогда Go \~opi G\, (x,y,ownr) G R\ и предикат can_share_own(x,y,Go,Ls) истинен. Если х E]y[, то пусть op\ = know(x,y,x). Тогда Go \~opi G\ и (x,y,ownr) E R\ и предикат can_share_own(x,y,Go,Ls) также истинен.Во втором случае истинен предикат can_share(x,y,Go, Ls). Следовательно, истинен предикат can_share_own(x, у, Go, Ls).В третьем случае имеется х Е Ns П So, существует сущность е G [у] и истинен предикат can_write_memory(x,e,Go,Ls). Пусть ар\ = control(x,y,e), тогда G0 \~api G\, (x,y,ownr) E R\ и предикат can_share_own(x,y,Go,Ls) истинен.В четвертом случае имеется х Е Ns П So, существует сущность е Е]у[ и истинен предикат can_write_memory(e,x,Go,Ls). Пусть ар\ = know(x,y,e), тогда Go \~api G\, (x,y,ownr) E R\ и предикат can_share_own(x,y,Go,Ls) истинен.Докажем индуктивный шаг. Пусть т>2и доказываемое утверждение верно для всех последовательностей субъектов длины к < т. Докажем, что оно верно и для всех таких последовательностей длины т.Рассмотрим последовательность субъектов s\,...,sm в So, где s\ = x, S2 = = z и sm = у. Пусть z E Ns П So- Тогда по предположению индукции существуют правила преобразования состояний ор\,... ,орн, такие, что Go \~opi Gi \~ap2 ... \~opN GN, и верно, что (х, z, ownr), (z,y,ownr) E Rn , где N ^ 0. Положим орм+1 = take_right(ownr,x,z,y). Тогда Gn \~op(N+i) Gn+i = = (Sn+i, En+i, Rn+i U An+i U Fn+i, Hn+i) и (x,y,ownr) E Rn+i, следовательно, предикат can_share_own{x,y,Go,Ls) истинен.Если z E Ls П So, то (z,y,ownr) E До, и по предположению индукции предикат can_share_own(x, z,Go, Ls) истинен. Следовательно, существуют правила преобразования состояний opi,...,opN, такие, что Go \~opi G\ \~ap2 ■■■ \~opN Gn, и (x,z,ownr) E Rn, где N ^ 0. Аналогично получаем истинность предиката can_share_own(x, у, Go, Ls). Лемма доказана. ■Определим и обоснуем алгоритмически проверяемые необходимые и достаточные условия истинности предиката can_steal_own(x,y,Go,Ls).Теорема 1. Пусть имеется Go = (So,Eo,Ro U Aq U Fo,Hq) - состояние КС Yj(G*,OP), и (x,y,ownr) E Nr, где x E Ns П So, У Е S0 и х ф у. Тогда предикат can_steal_own(x,y,Go, Ls) является истинным, если и только если существует по-122Д. Н. Колеговследовательность субъектов s\,... , sm в So, где s\ = х, sm = ц и m ) 2, таких, что выполняется одно из условий.Условие 1. т = 2 и истинен предикат directly_can_share_own(x, у, G0,LS).Условие 2. т > 2 и для каждого г = 1,..., т - 2 выполняется одно из условий:~ Si, Si+i G iVs П 5*0, Si ф у и предикаты directly_can_share_own(si, si+i,G0, Ls), directly_can_share_own(si+i, Si+2, Gq, Ls) являются истинными;•·i < m - 2, Si, Si+2 G NsdSo, Si, Si+2 ф У и являются истинными предикаты directly_-can_share_own(si, s^+i, Go, £,s) и directly_can_share_own(si+2, Si+i, Go, Ls);•i < m - 2, Si+\,Si+2 G iVs П 5*0, Sj+i 7^ y, Si+2 ф у и являются истинными предикаты directly_can_share_own(si+i, Si, Go, Ls), directly_can_share_-own(si+2, si+i, G0, Ls);•Si+\ G Ns П 5*0, Si+\ ф у и являются истинными предикаты directly_can_share_-own(si+\, Si, Go, Ls), directly_can_share_own(si+\, Si+2, Go, Ls).•·Доказательство. Докажем достаточность выполнения условий теоремы для истинности предиката can_steal_own(x,y,Go, Ls)- Если выполнено первое условие теоремы, то в соответствии с леммой истинен предикат can_share_own(x,y,Go,Ls)-Следовательно, предикат can_steal_own(x, у, Go, Ls) также является истинным. Если выполнено второе условие теоремы, то тогда существует последовательность субъектов si,...,sm в S0, где si = х, sm = у, х ф у и т > 2.•·Проведем доказательство индукцией по длине т последовательности субъектов. Пусть т = 3. Возможны два случая. Первый случай: х, S2 G Л^Лб'о и истинны предикаты directly_can_share_own{x,S2, Go, Ls), directly_can_share_own(s2, y, Go, Ls). Тогда в соответствии с леммой существуют состояния G\,... ,Gn = (Sn, En, Rn U Aj^ U Fn,Hn) и правила преобразования состояний ор\,... ,ор^, такие, что Go \~opi Gi hopa ^opN GN и (x,s2,ownr), (s2,y,ownr) G RN, где N ^ 0. Пусть opN+i = = take_right(ownr,x,s2,y) и GN hop(w+1) GN+1, где Gw+i = (SN+1,EN+1,RN+1 U An+i U F/v+i, Hn+i)- Тогда (x, y, ownr) G Rn+i и предикат can_steal_own(x, y, Go, Ls) является истинным. Второй случай: S2 G Ns П So и истинны предикаты directly_can_share_own(s2, x, Go, Ls), directly_can_share_own(s2, у, Go, Ls). Тогда в соответствии с леммой существуют состояния G\,... ,Gn = (Sn, En, Rn U An U Fn, Hn) и правила преобразования состояний ор\,... , opN, такие, что Go \~api G\ \~ap2 \~opN Gn и (s2,x,ownr), (s2,y,ownr) G Rn, где N ^ 0. Пусть opN+i = = grant_right(ownr,s2,x,y) и GN 1-^(^+1) GN+i, где GN+i = (Sn+i,En+i,Rn+i U An+i U Fn+i, Hn+i). Тогда (x, y, ownr) G Rn+i и предикат can_steal_own(x, y, Go, Ls) является истинным.•·Докажем индуктивный шаг. Пусть т > 4 и утверждение теоремы верно для всех последовательностей субъектов длины к < т. Докажем, что утверждение теоремы верно для всех таких последовательностей длины т. Пусть имеется последовательность субъектов S\,..., sm в So, где s\ = x, S2 = z, S3 = w и sm = у. Возможно четыре случая.•·Первый случай: x,z G Ns П So и истинны предикаты directly_can_share_-own(x,z,Go,Ls), directly_can_share_own(z,w, Go, Ls). Тогда в соответствии с леммой существуют состояния G\,... , Gn = (Sn, En, Rn U An U Fn, Hn) и правила преобразования состояний ор\,... ,opN, такие, что Go \~ap\ G\ \~ap2 ■■■ \~opN Gn и (х, z, ownr), (z, w, ownr) G Rn, где N ^ 0. По предположению индукции существуют состояния GN+i, ■■■ , Gn+k = (Sn+k, En+k, Rn+k U An+k U Fn+k, Hn+k) и правила преобразования состояний орлг+i, , opn+k, такие, что Gjv+i l~op(w+i) Gn+2 K>p(w+2)•·Анализ безопасности информационных потоков•·123•· \-op(N+K) GN+K и (w,y,ownr) G Rn+k , где К ^ 0. Положим opN+K+i = = take_right(ownr,x,z,w), opn+k+2 = take_right(ownr,x,w,y), тогда•·Gn+K \~op(N+K+l) Gn+K+1 \~op(N+K+2) Gn+K+2 = (Sn+K+2, En+K+2, Rn+K+2 U•·An+k+2 U Fn+k+2,Hn+k+2) и (x,y,ownr) G Rn+k+2- Следовательно, предикат can _share _own(x, y, Go, Ls) истинен.•·Второй случай: x,w G N$ П 5*0 и истинны предикаты directly_can_share_-own(x,z,Go,Ls), directly_can_share_own{w,z, Go, Ls). Тогда в соответствии с леммой существуют состояния G\,... , Gn = (Sn, En, Rn U An U Fn, Hn) и правила преобразования состояний ор\,... ,opN, такие, что Go K>pi G\ \~ap2 ■■■ \~opN Gn и (x, z, ownr), (w, z, ownr) G Rn, где N ^ 0. По предположению индукции существуют состояния GN+i,... , GN+K = (Sn+k, EN+K, Rn+k U An+k U Fn+k, Hn+k) и правила преобразования состояний opn+i, ■ ■ ■ , opn+k, такие, что Gn+i \~op(N+i) Gn+2 K>p(w+2) \-op(N+K) Gn+k и (w,y,ownr) G Rn+k, где К ^ 0. Положим орм+к+г = = grant_right(ownr,w, z,y), opn+k+2 = take_right(ownr,x, z,y), тогда Gn+k \~op(n+k+i) Gn+k+i \~op(n+k+2) Gn+k+2 = (Sn+k+2, En+k+2, Rn+k+2 U An+k+2 U Fn+k+2,Hn+k+2) и (x,y,ownr) G Rn+k+2- Следовательно, предикат can _share _own(x, y, G0, Ls) истинен.•·Третий случай: w,z G N$ П So, z ф у и истинны предикаты directly_can_-share_own(z,x,Go,Ls), directly_can_share_own(w,z, G0, Ls). Тогда в соответствии с леммой существуют состояния G\,... ,Gn = (Sn, En, Rn U An U Fn,Hn) и правила преобразования состояний ор\,... ,opN, такие, что Go l~opi G\ \~ap2 ■■■ \~opN Gn и (z, x, ownr), (w, z, ownr) G Rn, где N ^ 0. По предположению индукции существуют состояния Gw+i, , Gn+k = (Sn+k, En+k, Rn+k U An+k U Fw+k, Hn+k) и правила преобразования состояний opN+\, ■ ■ ■, opn+k, такие, что Gn+i \~op(N+i) GN+2 ^op(N+2) \-op(N+K) GN+K и (w,y,ownr) G Rn+k, где К ^ 0. Положим орлч-йг+i = grant_right(ownr,w, z,y), opn+k+2 = grant_right(ownr,z,x,y), тогда Gn+k \~op(n+k+i) Gn+k+i \~op(n+k+2) Gn+k+2 = (Sn+k+2, En+k+2, Rn+k+2 U ^4w+k+2 U Fn+k+2,Hn+k+2) и (x,y,ownr) G Rn+k+2- Следовательно, предикат can _share _own(x, y, G0, L^) истинен.•·Четвертый случай: z G iV^ П 5*0, z ф у и истинны предикаты directly_can_-share_own(z, x, Go, Ls), directly_can_share_own(z,w, Go, Ls). Тогда в соответствии с леммой существуют состояния G\,... , Gn = (Sn, En, Rn U An U Fn, Hn) и правила преобразования состояний ор\,... ,opN, такие, что Go \~api G\ \~ap2 ■■■ \~opN Gn и (z, х, ownr), (z, w, ownr) G Rn, где N ^ 0. По предположению индукции существуют состояния GN+i, ■■■ , Gn+k = (Sn+k, En+k, Rn+k U An+k U Fn+k, Hn+k) и правила преобразования состояний opN+i, ■ ■ ■ , opn+k, такие, что Gn+i \~op(N+i) Gn+2 \~op(N+2) \-op(N+K) GN+K и (w,y,ownr) G Rn+k, где К ^ 0. Положим opN+K+i = = take_right(ownr, z,w,y), opn+k+2 = grant_right(ownr, z,x,y), тогда Gn+k \~op(n+k+i) Gn+k+i \~op(n+k+2) Gn+k+2 = (Sn+k+2, En+k+2, Rn+k+2 U An+k+2 U Fn+k+2,Hn+k+2) и (x,y,ownr) G Rn+k+2- Следовательно, предикат can_share_own(x, y, Go, Ls) истинен.•·Индуктивный шаг доказан. Доказательство достаточности выполнения условий теоремы для истинности предиката can_steal_own(x, у, Go, Ls) закончено.•·Докажем необходимость выполнения условий теоремы для истинности предиката can_steal_own(x, у, G0, Ls).•·Пусть истинен предикат can_steal_own(x,y,Go,Ls). Тогда по определению существуют состояния G\,... , Gn = (Sn, En, Rn U An U Fn, Hn) и правила преобразования состояний ор\,... , opN, такие, что Go \~opi G\ \~ap2 ■ ■ ■ \~opN Gn, и (х, у, ownr) G Rn,•·124•·Д. Н. Колегов•·где N ^ 0. Выберем среди последовательностей правил преобразований ту, у которой длина N является минимальной. Следовательно, (x,y,ownr) ^ Rn-i- При этом в последовательности правил ор\,... , орм отсутствуют правила вида grant_right(a, у, s, е), take _right[a ,y, s, е), control (у, s, е1), know (у, s, е1), где alpha Е Rr, s Е NsC\So, е, е' Е Е0 и е' Е [s] или е' E]s[. Проведем доказательство индукцией по числу N.•·Пусть N = 0, тогда (х,у, ownr) E Ro и условие 1 теоремы выполнено. Пусть N = 1, тогда х Е Ns П So, у Е SO, (x,y,ownr) ф. Rq и существует правило преобразования состояний ор\, такое, что G0 K>pi G\ и (x,y,ownr) E R\. Из определения правил преобразования состояний следует, что возможны шесть случаев:•·х Е [у] и ор\ = control{x,y,x)\•·х Е]у[ и ор\ = know(x,y,x);•·существует сущность е Е [у], такая, что (x,e,writem) E Fq и ор\ = control{x,y,e)\•существует сущность е Е]у[, такая, что (e,x,writem) E Fq и ор\ = know(x,y,e);•·существует субъект z E Ns П So, такой, что (x,z,ownr), (x,z,ownr) E Ro и ор\ =take_right(ownr,x,z,y);•существует субъект z E Ns П 5*0, такой, что (z, х, ownr), (х, z, ownr) E Ro и ор\ = grant _right(ownr,z, x, у).•·Все шесть случаев соответствуют условиям 1 и 2 теоремы.•·Пусть N > 2 и утверждение теоремы верно для всех последовательностей преобразований состояний длины / < N. Тогда х Е Ns П «So, У & So, (x,y,ownr) ф Rn-i и существует правило преобразования состояний орм, такое, что Gjv-i \~opN Gn и (x,y,ownr) Е Rn-•Из определения правил преобразования состояний и минимальности N следует, что выполняется одно из условий:•·существует сущность е Е [у], такая, что (х, е, writem) E Fjv_i и орм = control{х, у, е);•·существует сущность е Е]у[, такая, что (e,x,writem) E F^_i и орм = know(x,y,e);•·существует субъект z E Ns П So, такой, что [x,z,ownr),[z,y,ownr) E Rn-i и орм = take_right(ownr,x,z,y);•·существует субъект z E Ns П So, такой, что (z, х, ownr), (z, у, ownr) E Rn-i и °Pn = grant_right(ownr, z, x, y).Если выполнено первое или второе условие, то выполнено первое условие теоремы. Рассмотрим случай выполнения третьего условия, когда (x,z,ownr), (z,y,ownr) E Rn-i и 0Pn = take_right(a,x, z,y). Доказательство для случая выполнения четвертого условия проводится аналогично доказательству для случая выполнения третьего условия.Так как длина N минимальна, то в последовательности преобразований состояний не использовались правила вида create_entity(x, у, z) и create_subject(x, у, z). Следовательно, z E So и истинны предикаты can_steal_own{x,z,Go,Ls) и can_steal_-own(z, у, Go, Ls) с длинами последовательностей преобразований состояний меньше N. По предположению индукции возможны четыре случая. Первый случай: истинны предикаты directly_сап_share_own(x, z, G0, Ls) и directly_can_share_own(z, y, G0, Ls). Следовательно, второе условие теоремы выполнено.Второй случай: истинен предикат directly_can_share_own(x,z, Go, Ls) и существует последовательность субъектов s\,... , sm в So, где s\ = z, sm = у и т ^ 2, таких, что выполняется условие 2. Следовательно, существует последовательность субъектов S\,... , sm, sm+\ в 5*0, где S\ = x, $2 = z, sm+\ = у, таких, что выполняется условие 2 теоремы.Анализ безопасности информационных потоков125Третий случай: истинен предикат directly_can_share_own(z, у, Go, Ls) и существует последовательность субъектов S\,... , sm в So, где S\ = х, sm = z ж m ^ 2, таких, что выполняется условие 2. Следовательно, существует последовательность субъектов Si,... , sm, sm+i в So, где Si = х, sm = z, sm+\ = у, таких, что выполняется условие 2 теоремы.Четвертый случай: существуют последовательности субъектов s\,...,sm и Si,... , s'n в So, где S\ = x, sm = s'i = z, s'n = у и m,n ^ 2, для которых выполняется условие 2. Следовательно, существует последовательность субъектов s'[,... ,s'^l+n_1 в So, где s" = x, s'ln+n_l = у, таких, что выполняется условие 2 теоремы.Индуктивный шаг доказан. Доказательство необходимости выполнения условия теоремы для истинности предиката can_steal_own(x,y,Go,Ls) закончено. Теорема доказана. ■ЛИТЕРАТУРА

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

компьютерная безопасность , математические модели безопасности , дискреционные модели , анализ безопасности , права доступа , информационные потоки

Авторы

ФИООрганизацияДополнительноE-mail
Колегов Денис Николаевич Томский государственный университет аспирант d.n.kolegov@gmail.com
Всего: 1

Ссылки

Девянин П. Н. Анализ безопасности управления доступом и информационными потоками в компьютерных системах. М.: Радио и связь, 2006. 176 с.
Девянин П. Н. Модели безопасности компьютерных систем: Учеб. пособие для студ. высш. учеб. заведений. М.: Издательский центр «Академия», 2005. 144 с.
Робачевский А. Операционная система UNIX. СПб.: БХВ-Петербург, 2000. 528 с.
Качанов М. А., Колегов Д. Н. Расширение функциональности системы безопасности ядра Linux на основе подмены системных вызовов // Прикладная дискретная математика. 2008. № 2. С. 76 - 80.
 Анализ безопасности информационных потоков по памяти в компьютерных системах с функционально и параметрически ассоциированнымисущностями             | ПДМ. 2009. № 1(3).

Анализ безопасности информационных потоков по памяти в компьютерных системах с функционально и параметрически ассоциированнымисущностями | ПДМ. 2009. № 1(3).

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