Review lection of security models of computer system.pdf ВведениеВ соответствии с проектом ГОС ВПО третьего поколения модели безопасностикомпьютерных систем (КС) преподаются в рамках следующих дисциплин:- «Теоретические основы компьютерной безопасности» для магистров;- «Модели безопасности компьютерных систем» специальности «Компьютерная безопасность» квалификации специалист;- «Безопасность информационных и аналитических систем» специальности «Информационно-аналитические системы безопасности» квалификации специалист;- «Основы информационной безопасности» для бакалавров и других специальностейнаправления 090000 - «Информационная безопасность» квалификации специалист.Исследование формальных моделей, особенно моделей безопасности логическогоуправления доступом и информационными потоками в КС, создает предпосылки дляразвития теории компьютерной безопасности. С применением формальных моделейвозможна разработка научно-обоснованных подходов, использование которых обеспечитгарантии выполнения требований безопасности в существующих или перспективныхзащищенных КС.Основными классическими моделями, ориентированными на защиту от угроз конфиденциальностии целостности информации, а также от угрозы раскрытия параметровКС, являются модели дискреционного управления доступом, изолированнойпрограммной среды (ИПС), мандатного управления доступом, безопасности информационныхпотоков, ролевого управления доступом [1-3]. Кроме того, в настоящеевремя активно развивается семейство моделей безопасности логического управлениядоступом и информационными потоками (сокращенно ДП-моделей).Классические модели и ДП-модели построены с применением следующих основныхпонятий: субъект (subject), объект (object), контейнер (container), сущность (entity),доступ (access), право доступа (access right), информационный поток по памяти(information flow by memory) или по времени (information flow by time). При этом в современнойтеории компьютерной безопасности наибольшее развитие в области формальногомоделирования безопасности КС получил подход, заключающийся в представленииисследуемой КС в виде абстрактной системы (автомата), каждое состояниекоторой описывается доступами, реализуемыми субъектами к сущностям, а переходыКС из состояния в состояние описываются командами или правилами преобразованиясостояний, выполнение которых, как правило, инициируется субъектами. В основеданного подхода используется аксиома 1, позволяющая выделить элементы КС,необходимые для анализа ее безопасности.Аксиома 1 (основная аксиома компьютерной безопасности). Все вопросыбезопасности информации в КС описываются доступами субъектов к сущностям.Классификация и взаимосвязь рассматриваемых моделей безопасности КС приведенана рис. 1. Все они войдут в разрабатываемое автором учебное пособие «Моделибезопасности компьютерных систем», второе издание которого планируется в 2010 г.1. Модели дискреционного управления доступоми изолированной программной средыМодель Харрисона - Руззо - Ульмана (ХРУ) является одной из первых формальныхмоделей. В модели произвольная КС с дискреционным управлением доступомописывается множеством матриц доступов, каждая из которых соответствует состояниюКС, и командами преобразования матриц доступов. Каждая из команд задаетсямножеством параметров, условием выполнения и конечной последовательностьюпримитивных операторов, преобразующих матрицу доступов. Применение командыпереводит КС из состояния в последующее состояние.В модели ХРУ анализируются условия, при выполнении которых возможна проверкабезопасности КС. При этом используется следующее определение.Определение 1. Начальное состояние системы ХРУ называется безопасным относительнонекоторого права доступа r , когда невозможен переход системы в состояние,в котором право доступа r появилось в ячейке матрицы доступов, до этого r несодержавшей.Основным фактом, который доказывается в модели ХРУ, является следующая теорема.Теорема 1. Задача проверки безопасности произвольных систем ХРУ алгоритмическинеразрешима.При доказательстве теоремы 1 используется факт, обоснованный в рамках теориимашин Тьюринга: не существует алгоритма проверки для произвольной машиныТьюринга и произвольного начального слова, остановится ли машина Тьюринга в конечномсостоянии или нет. При этом строится гомоморфизм произвольной машиныТьюринга в соответствующую ей систему ХРУ, для чего все элементы и командымашины Тьюринга задаются в виде элементов и команд системы ХРУ. Например,внешний и внутренний алфавиты машины Тьюринга описываются множеством правдоступа системы ХРУ, пройденный участок ленты машины Тьюринга представляетсяРис. 1. Классификация и взаимосвязь положений моделей безопасности КСматрицей доступов (рис. 2), команды машины Тьюринга задаются командами системыХРУ. Таким образом, остановке машины Тьюринга (переходу в конечное состояние q0)соответствует утечка права доступа q0 в системе ХРУ. Значит, задача проверки безопасностипроизвольных систем ХРУ алгоритмически неразрешима.Следует отметить, что в современных КС в большинстве случаев при определениибезопасного состояния рассматривается утечка права доступа r не в произвольную, ав заданную ячейку матрицы доступов. Например, появление у администратора безопасностиправ доступа на чтение или модификацию конфигурационных файлов ОС,как правило, не будет являться нарушением безопасности, однако получение данногоправа доступа нарушителем является нарушением безопасности. Таким образом, придоказательстве теоремы 1 следует рассмотреть вопрос о существовании для произвольнойсистемы ХРУ алгоритма проверки возможности утечки права доступа в заданнуюячейку матрицы доступов. При этом целесообразно использовать следующее рассуждение.Каждой системе ХРУ поставим в соответствие другую систему ХРУ, в которойв каждую матрицу доступов M первой системы добавлен специальный субъект s0,обладающий сам к себе специальным правом доступа active Е M [s0, s0]; в каждую ко-Рис. 2. Заполнение матрицы доступов системы ХРУманду первой системы, содержащую примитивный оператор внесения права доступа г,во второй системе добавлен параметр для обозначения субъекта, который в условиикоманды проверяется на наличие у него самого к себе права доступа active, также в командудобавлен примитивный оператор внесения права доступа г в ячейку M[s0, s0].Таким образом, утечка права доступа г в первой системе происходит тогда и толькотогда, когда во второй системе происходит утечка права доступа г в ячейку M[s0, s0].Следовательно, если бы для произвольной системы ХРУ существовал алгоритм проверкивозможности утечки права доступа в заданную ячейку матрицы доступов, тосуществовал бы алгоритм проверки возможности утечки права доступа в произвольнуюячейку.Развитием модели ХРУ является модель ТМД, позволяющая за счет введения типовсубъектов и объектов расширить класс КС, для которых существует алгоритмпроверки безопасности. Очевидно, что система модели ТМД является обобщениемсистемы модели ХРУ, которую можно рассматривать как частный случай системымодели ТМД с одним единственным типом для всех объектов и субъектов. С другойстороны, следует обратить внимание на то, что любую систему модели ТМД можновыразить через систему модели ХРУ, введя для обозначения типов специальныеправа доступа и заменив проверку типов в командах проверкой наличия соответствующихправ доступа. Описание алгоритма построения для произвольной системы моделиТМД эквивалентной ей системы модели ХРУ является интересной практическойзадачей.В модели ТМД обосновывается, что алгоритм проверки безопасности существуетдля ациклических монотонных систем модели ТМД, при этом используются следующиеопределения и доказывается теорема.Определение 2. Система монотонной ТМД (МТМД) - система ТМД, в командахкоторой отсутствуют немонотонные примитивные операторы вида «удалить»... и«уничтожить». ..Определение 3. Каноническая форма системы МТМД (КФМТМД) - системаМТМД, в которой команды, содержащие примитивные операторы вида «создать»... ,не содержат условий и примитивных операторов вида «внести»...Определение 4. Система МТМД (КФМТМД) называется ациклической(АМТМД или соответственно АКФМТМД) тогда и только тогда, когда ее граф создания(определение графа создания приводится в [2]) не содержит циклов.Теорема 2. Для каждой системы МТМД существует эквивалентная ей системаКФМТМД.В доказательстве теоремы 2 приводится алгоритм построения для произвольнойсистемы МТМД эквивалентной ей системы КФМТМД. В алгоритме особо рассматриваютсяспециальным образом активизированные объекты и субъекты системы. Приэтом при построении из системы МТМД ее канонической формы в нее добавляетсяспециальный субъект sactive, имеющий специальный тип tactive, который будет обладатьспециальным правом доступа active только к активизированным объектам. Кроме того,в параметры каждой команды системы КФМТМД, не содержащей примитивныеоператоры вида «создать»..., добавляется параметр с типом tactive. Таким образом,наличие специального права доступа active у субъекта sactive к объекту может бытьиспользовано для обозначения объекта как активизированного.В результате обосновывается теорема.Теорема 3. Существует алгоритм проверки безопасности систем АМТМД.Алгоритм проверки безопасности систем АМТМД состоит из следующих трехшагов:1. Для системы АМТМД построить эквивалентную ей систему АКФМТМД.2. Используя команды, содержащие только примитивные операторы «создать»... ине содержащие условий, перейти из начального состояния системы в некоторое «развернутое» состояние, обеспечивающее минимально необходимый и достаточный дляраспространения прав доступа состав объектов.3. Используя команды, не содержащие примитивные операторы «создать»..., перейтииз «развернутого» состояния в «замкнутое» состояние, в котором дальнейшееприменение таких команд не приводит к изменениям в матрице доступов.В модели Take-Grant условия передачи прав доступа и реализации информационныхпотоков рассматриваются с использованием графов доступов, что позволяетдобиться большейнаглядности исследуемых положений модели. Модель Take-Grantизучается в два этапа. На первом этапе рассматривается классическая модель Take-Grant, в которой анализируются алгоритмически проверяемые условия передачи правдоступа. На втором этапе рассматривается расширенная модель Take-Grant, в которойанализируются условия реализации в КС информационных потоков.В классической модели Take-Grant описываются четыре де-юре правила преобразованияграфов доступов take(a,x,y, z), grant (a,x,y, z), create(a,x ,y), remove(a,x,y)и используются следующие основные определения.Определение 5. Пусть x ,y Е O0, x = y - различные объекты графа доступовG0 = (S0,O0,E 0) и a - множество прав доступа. Определим предикатcan_share(a, x, y, G0), который будет истинным тогда и только тогда, когда существуютграфы Gi = (Si, Oi, Ei), ... , GN = (SN ,ON, EN) и правила opi , ... , opN, где N ^ 0,такие, что Go \~op1 Gi ... ]r apN GN и (x, y, a) С EN.Определение 6. Островом в произвольном графе доступов G0 называется егомаксимальный tg-связный подграф, состоящий только из вершин субъектов.Определение 7. Мостом в графе доступов G0 называется проходящий черезвершины-объекты tg-путь, концами которого являются вершины-субъекты и словарнаязапись имеет вид t*, t*, t* ~д t *, t* *-1 *, где символ «*» означает многократное(в том числе нулевое) повторение.Определение 8. Начальным пролетом моста в графе доступов G0 называетсяtg-путь, началом которого является вершина-субъект, концом - объект, проходящийчерез вершины-объекты, словарная запись которого имеет вид t* ~д .Определение 9. Конечным пролетом моста в графе доступов G0 называетсяtg-путь, началом которого является вершина-субъект, концом - объект, проходящийчерез вершины-объекты, словарная запись которого имеет вид t* .Алгоритмически проверяемые необходимые и достаточные условия истинностипредиката can_shar e (a,x,y ,G0) обосновываются в следующей теореме.Теорема 4. Пусть G0 = (S0,O0,E 0) -произвольный граф доступов, x,y Е O0,x = у. Предикат can_share(a, x, y, G0) истинен тогда и только тогда, когда или(x,y,a) С Е0, или выполняются условия 1-3:1. Существуют объекты s i , . . . , s m Е O0: (si,y ,7i) С Е0 для i = 1 , . . . ,m иа = Yi U ... U Ym.2. Существуют субъекты x i ,... , x^, s'1, . . . , s 'm Е S0:а) x = xi или xi соединен с x начальным пролетом моста в графе G0, гдеi = 1 ,... , m;б) si = si или si соединен с si конечным пролетом моста в графе G0, где i = 1 ,... , m.3. В графе G0 для каждой пары (xi, si), где i = 1 ,...,m , существуют островаIi,i,... , I i,Ui, где ui ^ 1, такие, что xi Е Ii,1, si Е I iui, и существуют мосты междуостровами Ii j и Ii,j+1, где j = 1 ,... , ui - 1.Доказательство достаточности выполнения условий теоремы для истинности предикатаcan_share(a, x, y, G0) является конструктивным и состоит в обосновании возможностипередачи прав доступа по пролетам мостов, мостам и островам (фрагментдоказательства приведен на рис. 3). Формальное доказательство необходимости выполненияусловий теоремы для истинности предиката can_share(a, x, y, G0) являетсядостаточно трудоемким.Однако интересной задачей, реализующей наглядный подход к доказательствунеобходимости выполнения условий теоремы для истинности предикатаcan_share(a, x, y, G0), является обоснование того, что не существует путей между двумясубъектами, отличных от мостов и проходящих через вершины-объекты, по которымвозможна передача прав доступа. При ее решении следует рассмотреть все пути(с учетом симметрии) длины 2 между двумя субъектами, проходящие через вершины-объекты, по которым возможна передача прав доступа (рис. 4, a) и невозможна передачаправ доступа (рис. 4,б). Любой путь, соединяющий двух субъектов, проходящийчерез объекты, по которому возможна передача прав доступа, не должен содержатьфрагменты, приведенные на рис. 4,б. В то же время очевидно, что любой такой путь,состоящий только из фрагментов, приведенных на рис. 4, a, является мостом.Для того чтобы обеспечить лучшее усвоение способов применения определениямоста при анализе путей передачи прав доступа, целесообразно рассмотреть графыРис. 3. Пример передачи прав доступа по мостуРис. 4. Виды путей длины 2 (* - или t, или д)доступов, представленные на рис. 5, с использованием которых следует показать,что мостами могут являться tg-пути, неоднократно проходящие через один и тот жеобъект.Рис. 5. «Т-образный» мостТакже представляет интерес решение задачи на непосредственную проверку условийтеоремы 4 (рис. 6).Рис. 6. Проверка условий теоремы 4В расширенной модели Take-Grant кроме де-юре правил рассматриваются четыреде-факто правила преобразования графов доступов spy(x,y, z), f in d ( x , y , z ),post(x,y, z), pass(x,y, z) и используется следующее определение.Определение 10. Пусть x , y Е O0, x = y - различные объекты графа доступови информационных потоков G0 = (S0, O0, E0 U F0). Определим предикатcan_write(x,y, G0), который будет истинным тогда и только тогда, когда существуютграфы Gi = (Si , Oi , E i U Fi), ... , Gn = (SN, ON, EN U FN) и де-юре или де-фактоправила opi , ... , opN, где N ^ 0, такие, что G0 bopi Gi bop2 ... bopN GN и (x, y, w) Е FN.Алгоритмически проверяемые необходимые и достаточные условия истинностипредиката can_wr i te(x,y,G0) обосновываются в следующей теореме.Теорема 5. Пусть G0 = (So, O0, E0 U F0)-граф доступов и информационныхпотоков, x , y Е O0, x = y. Тогда предикат can_wr i te(x,y,G0) истинен тогда и толькотогда, когда существуют объекты oi, ... , om Е O0, где o1 = x, om = у, такие, что илиm = 2 и (x, у, w) Е F0, или для i = 1, ... , m - 1 выполняется одно из условий:- oi Е S0 и или истинен предикат can_share({w},oi ,oi+1 ,G0), или (oi,oi+1,w) ЕЕ E0 U F0;- oi+1 Е S0 и или истинен предикат can_share({r},oi+1,oi ,G0), или (oi+1,oi ,r) ЕЕ E0 U F0;- oi ,oi+1 Е S0 и или истинен предикат can_share(a,oi ,oi+1,G0), или истинен предикатcan_share(a,oi+1,oi ,G0), где а Е {t,g}, или существует объект oi Е O0, такой,что либо истинны предикаты can_share({t}, oi , oi, G0), can_share({g}, oi+1, oi, G0),либо истинны предикаты can_share({g}, oi , oi, G0), can_share({t}, oi+1, oi, G0).Наиболее интересным при доказательстве теоремы 5 является обоснование возможностиреализации информационного потока между двумя субъектами в случае, когдавыполнено третье условие теоремы. На рис. 7 приведен пример обоснования возможностиреализации информационного потока между двумя субъектами для одного изслучаев.о\ /х у х ___ v y , уРис. 7. Реализация информационного потока на записьДля лучшего усвоения положений расширенной модели Take-Grant целесообразнорешить задачи на применение теоремы 5 с целью проверки условий истинностипредиката can_wr i te(x,y,G0) (рис. 8).Кроме анализа условий реализации информационных потоков, в рамках расширенноймодели Take-Grant рассматривается алгоритм построения замыкания графадоступов и информационных потоков. При этом используются следующие определения.Определение 11. Пусть G = (S ,O,E U F ) - граф доступов и информационныхпотоков, такой, что для каждого субъекта s Е S существует объект o Е O,такой, что выполняется условие (s,o, { t ,g,r ,w} ) С E . Тогда замыканием (или де-факто-замыканием) графа G называется граф доступов и информационных потоковG* = (S, O, E * U F *), полученный из G применением последовательности правил take,grant и де-факто правил. При этом применение к графу G* указанных правил неприводит к появлению в нем новых ребер.Определение 12. Пусть G = (S ,O,E U F ) -граф доступов и информационныхпотоков, такой, что для каждого субъекта s Е S существует объект o Е O, такой,Рис. 8. Проверка выполнения условий теоремы 5что выполняется условие (s,o, {t, g,r,w}) С E. Тогда tg-замыканием графа G называетсяграф доступов и информационных потоков Gtg = (S ,O,E tg U F ), полученныйиз G применением последовательности правил take или grant. При этом каждое ребро(oi, o2,a) Е E tg \ E имеет вид (oi , o2 ,t) или (oi , o2,g), и применение к графу Gtg правилtake или grant не приводит к появлению в нем новых ребер указанного вида.Определение 13. Пусть G = (S ,O,E U F ) -граф доступов и информационныхпотоков, такой, что для каждого субъекта s Е S существует объект o Е O, для котороговыполняется условие (s, o, {t, g, r, w}) С E . Тогда де-юре-замыканием графа Gназывается граф доступов и информационных потоков Gdejure = ( S ,O,E dejure u F ),полученный из G применением последовательности правил take или grant. При этомприменение к графу Gdejure правил take или grant не приводит к появлению в немновых ребер.Таким образом, схематично алгоритм построения замыкания графа доступов и информационныхпотоков состоит из следующих трех шагов:1. Построение tg-замыкания.2. Построение де-юре-замыкания.3. Построение замыкания (де-факто-замыкания).При этом наиболее интересным является алгоритм построения tg-замыкания графадоступов и информационных потоков G = (S, O, E UF ), состоящий из следующих пятишагов:1. Для каждого s Е S выполнить правило create({t, g, r, w}, s, o); при этом создаваемыеобъекты занести в множество O, создаваемые ребра занести в множество E .2. Инициализировать: L = { (x ,y ,a) Е E : а Е {t,g}} - список ребер графа доступови информационных потоков и N = 0 - множество вершин.3. Выбрать из списка L первое ребро (x, y, а). Занести x и y в множество N . Удалитьребро (x, y, a) из списка L .4. Для всех вершин z Е N проверить возможность применения правил take илиgrant на тройке вершин x , y , z с использованием ребра (x, y, а), выбранного на шаге 3.Если в результате применения правил take или grant появляются новые ребра вида(a, b, в), где {a, b} С {x, y , z } и а Е {t, g}, занести их в конец списка L и множество E .5. Если список L не пуст, перейти на шаг 3.Пример применения алгоритма построения tg-замыкания приведен на рис. 9.Рис. 9. Пример применения алгоритма построения tg-замыканияПри завершении изучения положений моделей КС с дискреционным управлениемдоступом целесообразно решить практическую задачу построения для системы Take-Grant двух эквивалентных ей систем ХРУ и ТМД. При этом следует особо рассмотретьотличия полученных систем ХРУ и ТМД. В том числе следует обратить внимание нато, что для обозначения субъектов модели Take-Grant в модели ХРУ потребуетсяиспользование специального права доступа, а в модели ТМД для этого достаточноиспользовать специальные типы. Также целесообразно дать ответ на вопрос, какимограничениям должна соответствовать система, построенная в соответствии с положениямимодели Take-Grant , чтобы эквивалентная ей система ТМД была монотонной иациклической.В основанной на дискреционном управлении доступом субъектно-ориентированноймодели ИПС рассматриваются вопросы определения порядка безопасного взаимодействиясубъектов системы, описания и обоснования необходимых условий реализацииИПС, которая обеспечивает выполнение в КС требований априорно заданной политикибезопасности. При этом используются следующие определения и обозначения.Определение 14. Объект о в момент времени t функционально ассоциированс субъектом s, когда состояние объекта о повлияло на вид преобразования данных,реализуемого субъектом s в следующий момент времени t + 1.Определение 15. Монитор обращений (МО) -субъект, активизирующийся привозникновении любого информационного потока между объектами КС. Монитор безопасностиобъектов (МБО) -МО, который разрешает только потоки, не принадлежащиемножеству запрещенных информационных потоков.Введём следующие обозначения:[s]t - множество объектов, ассоциированных с субъектом s в момент времени t;o[t] - состояние объекта о в момент времени t;Stream(s, о) ^ о' - поток информации от объекта о к объекту о1;Create(s, о) ^ s' - операция порождения субъектов (из объекта о порожден субъектs' при активизирующем воздействии субъекта s).МБО фактически является механизмом реализации политики безопасности в КС.При изменении функционально ассоциированных с субъектами или с МБО объектовмогут измениться и свойства субъектов или самого МБО, и, как следствие, могут возникнутьпотоки, принадлежащие множеству запрещенных информационных потоков(рис. 10).Рис. 10. Возможные пути обхода политики безопасности нарушителемs': а - изменение функциональности субъектаs; б - изменение функциональности МБО; в -реализацияинформационного потока в обход МБОДля противодействия возможности реализации рассмотренных запрещенных информационныхпотоков в рамках модели предлагается обеспечить корректность субъектовсистемы друг относительно друга и замкнутость программной среды. При этомиспользуются следующие определения.Определение 16. Субъекты s и s' называются корректными относительно другдруга, когда в любой момент времени отсутствует поток (изменяющий состояние объекта) между любыми объектами o и o', ассоциированными соответственно с субъектамиs и s'. Таким образом, выполняется следующее условие:o Е [s]t, o' Е [s']t, где t ^ 0, не существует субъекта s'', такого, что илиStream(s", o) ^ o', или Stream(s'', o') ^ o.Определение 17. Корректные относительно друг друга субъекты s и s' называютсяабсолютно корректными, когда множества ассоциированных объектов указанныхсубъектов не имеют пересечения. Таким образом, выполняется условие[s]t П [s']t = 0, где t ^ 0.Определение 18. Монитор порождения субъектов (МПС) - субъект, активизирующийсяпри любом порождении субъектов. Монитор безопасности субъектов(МБС)-МПС, который разрешает порождение субъектов только для фиксированногомножества пар активизирующих субъектов и объектов-источников.Определение 19. КС называется замкнутой по порождению субъектов (обладаетзамкнутой программной средой), когда в ней действует МБС.Определение 20. Программная среда называется изолированной (абсолютноизолированной), когда она является замкнутой по порождению субъектов (в ней действуетМБС) и субъекты из порождаемого множества корректны (абсолютно корректны)относительно друг друга, МБС и МБО.Определение 21. Операция порождения субъекта Create(s,o) ^ s' называетсяпорождением с контролем неизменности объекта-источника, когда для любого моментавремени t > t0, в который активизирована операция порождения объекта Create ,порождение субъекта s' возможно только при тождественности объектов o[t0] и o[t].В субъектно-ориентированной модели ИПС обосновывается следующая лемма.Лемма 1 (базовая теорема ИПС). Если с момента времени t0 в абсолютной ИПСдействует только порождение субъектов с контролем неизменности объекта-источникаи все порождаемые субъекты абсолютно корректны относительно друг друга и существующихсубъектов (в том числе МБО и МБС), то в любой момент времени t > t0программная среда также остается абсолютной ИПС.Для учета влияния субъектов в КС на систему защиты целесообразно рассматриватьрасширенную схему взаимодействия элементов системы. При этом должна бытьособо подчеркнута роль МБС при порождении субъектов из объектов (рис. 11). Взаимодействиесубъектов и объектов при порождении потоков уточняетсявведениемассоциированных с субъектами объектов. Объект управления МБО (ОУо) содержитинформацию о разрешенных значениях отображения Stream (о разрешенных и запрещенныхинформационных потоках) и функционально ассоциирован с МБО, и объектуправления МБС (ОУ^) содержит информацию о значениях отображения Create (обэлементах множества разрешенных объектов-источников) и функционально ассоциированс МБС. Таким образом, рассмотренная концепция ИПС является расширениемклассического подхода к реализации ядра безопасности КС.Рис. 11. Ядро безопасности с учетом контроля порождения субъектов2. Модели мандатного или ролевого управления доступоми безопасности информационных потоковМандатное управление доступом чаще всего описывают в терминах, понятиях иопределениях свойств классической модели Белла - ЛаПадулы и ее основных интерпретаций.Классическая модель Белла - ЛаПадулы является автоматной моделью, в котороймоделируемая КС представляется абстрактной системой, каждое состояние которойописывается с использованием:- множества текущих доступов субъектов к объектам системы;- функций, задающих для каждого субъекта уровень доступа и текущий уровеньдоступа, для каждого объекта его уровень конфиденциальности;- матрицы доступов, позволяющей в дополнение к мандатному управлению доступомиспользовать дискреционное управление доступом.Описывается множество действий системы, задающих правила перехода системыиз состояния в состояние.С использованием уровней доступа субъекта и уровня конфиденциальности объекта,видов доступа и матрицы доступов в модели Белла - ЛаПадулы задаются трибазовых свойства безопасности: ss-свойство, ^-свойство и ds-свойство, которыми долженобладать каждый безопасный доступ субъекта к объекту.Определение 22. Доступ (s, о, г) обладает ss-свойством относительно f = (fs,fo, fc), где f s - функция уровней доступа субъектов, f o - функция уровней конфиденциальностиобъектов, fc - функция текущих уровней доступа субъектов, когда выполняетсяодно из условий:- г Е {execute, append};- г Е {read, write} и f s(s) ^ fo(o).Состояние системы (b, m, f ), где b - множество текущих доступов, m - матрицадоступов, обладает ss-свойством, когда в нём все доступы обладают ss-свойством относительноf .Определение 23. Доступ (s, о, г) обладает ^-свойством относительно f = (fs,fo, fc), когда выполняется одно из условий:- r = execute;- r = append и fo(o) ^ f c(s);- r = read и fc(s) ^ f0(o);- r = write и fc(s) = fo(o).Состояние системы (b, m, f ) обладает ^-свойством, когда в нём все доступы обладают^-свойством относительно f .Определение 24. Состояние системы (b, m, f ) обладает ds-свойством, когда внём для каждого доступа (s, o, r) выполняется условие r Е m[s, o].В безопасном состоянии все доступы должны быть безопасными. Система являетсябезопасной, когда все состояния на всех возможных траекториях ее функционированияявляются безопасными.Таким образом, на безопасных траекториях функционирования система, построеннаяв соответствии со свойствами классической модели Белла - ЛаПадулы, должнаразрешать получение субъектами только безопасных доступов к объектам.С использованием требования соответствия ss-свойству всех доступов состояниясистемы уровнем доступа субъекта ограничивается максимальный уровень конфиденциальностиобъектов, к которым субъект потенциально может получить доступна чтение. Основным свойством безопасности является ^-свойство. С использованиемтребования соответствия ^-свойству всех доступов состояния системы предотвращаетсявозможность реализации субъектом информационного потока от объекта с высокимуровнем конфиденциальности к объекту с низким уровнем конфиденциальности,при этом используется проверка текущего уровня доступа субъекта. Свойство дискреционнойбезопасности (ds-свойство), в котором используется матрица доступов, какправило, подробно не рассматривается.Алгоритмически проверяемые условия выполнения в системе свойств безопасностиформулируются и обосновываются в имеющих схожие формулировки теоремах A1, A2и A3. В качестве примера приведена формулировка теоремы A1.Теорема 6 (теорема A1). Система обладает ss-свойством для любого начальногосостояния z0, обладающего ss-свойством, тогда и только тогда, когда для каждогодействия (q, d, (b*, m*, f *), (b, m, f )), где q - запрос системе, d - ответ системы, (b, m,f )-исходное состояние, (b*, m*, f *)-последующее состояние, выполняются следующиеусловия:1. Каждый доступ (s, o, r) Е b* \ b обладает ss-свойством относительно f *.2. Если доступ (s, o, r) Е b и не обладает ss-свойством относительно f *, то (s, o,r) Е b*.При изучении классической модели Белла - ЛаПадулы целесообразно учесть,что она разрабатывалась для обеспечения безопасности конкретной защищеннойКС Multics. Поэтому некоторые элементы (например, права доступа append, execute,иерархия объектов, функция текущего уровня доступа субъектов) реализованы в моделитолько для обеспечения соответствия условиям функционирования КС Multics ине являются необходимыми для моделирования произвольной КС с мандатным управлениемдоступом. Поэтому рассмотрение интерпретаций модели Белла - ЛаПадулы(например, интерпретации «read-write» или интерпретации «безопасность переходов»)и особенно описанных в них свойств безопасности позволит лучше изучить наиболеесущественные и важные для теории элементы модели Белла - ЛаПадулы. Для тогочтобы лучше исследовать свойства классической модели Белла - ЛаПадулы и оценитьсложность практической разработки формальной модели управления доступомдля реальной КС, уместно решить задачу: построить пример системы Белла - ЛаПа-дулы с двумя субъектами и двумя объектами (большее число элементов системы неповлияет, по сути, на ход построения, но сделает его существенно более трудоемким).Самым интересным при изучении модели Белла - ЛаПадулы является анализ еенедостатков, в том числе:- отсутствие логической увязки условий выполнения системой свойств безопасности,данных в определениях, с заложенными в модель условиями их проверки, необходимостьи достаточность которых доказывается в базовой теореме безопасности(теореме БТБ);- модель «статична», то есть в ней отсутствует описание правил перехода системы изсостояния в состояние, а также «статично» анализируются условия возникновенияинформационных потоков;- реализация в КС только свойств безопасности, описанных в модели, не позволяетобеспечить защиту от возможности возникновения запрещенных информационныхпотоков (особенно информационных потоков по времени).Первый недостаток легко иллюстрируется на примере некорректной интерпретациимодели Белла - ЛаПадулы и имеет в основном теоретическое значение.Второй недостаток можно рассмотреть на следующих примерах.Пример 1. В классической модели Белла - ЛаПадулы для безопасности системытребуется безопасность каждого состояния на любой реализации (траектории) системы.Рассмотрим систему, в которой при переходе из любого состояния в последующееуровень доступа каждого субъекта устанавливается максимальным, а уровень конфиденциальностикаждого объекта - минимальным. Такая система будет безопаснав смысле определений свойств безопасности классической модели Белла - ЛаПаду-лы (любой доступ любого субъекта к любому объекту будет, очевидно, удовлетворятьss-свойству и ^-свойству). В то же время реализация такой системы вряд ли имееткакой-либо практический смысл.Пример 2. Используем интерпретацию low-watermark классической модели Белла- ЛаПадулы, в которой строится пример системыс мандатным управлением доступом.В ней описываются три правила перехода системы из состояния в состояние: Read,Write, Reset, и доказывается безопасность системы в смысле определений свойств безопасностиклассической модели Белла - ЛаПадулы. Наиболее важным в примере (начто следует обратить внимание) является то, что наличие или отсутствие в определениирезультатов применения правила Write требования стирания информации в объектев случае реального понижения его уровня конфиденциальности не влияет на логикудоказательства безопасности системы. Таким образом, отсутствие в классической моделиБелла - ЛаПадулы описаний правил перехода системы из состояния в состояниеможет привести к тому, что в формально безопасной КС будет возможна реализациязапрещенных информационных потоков.Пример 3. В интерпретации «безопасность переходов» делается попытка устранитьвторой недостаток модели Белла - ЛаПадулы путем введения в модель функциипереходов, с использованием которой на моделируемую КС накладывается существенноеограничение: за один шаг работы системы (переход из состояния в состояние) вноситсятолько одно изменение в один из параметров, используемый при определениисвойств безопасности. То есть либо изменяется на один элемент множество текущихдоступов, либо одно из значений одной из функций, при этом остальные параметрыостаются неизменными. С использованием интерпретации «безопасность переходов»можно разработать новые ограничения на функцию переходов, учитывающие особенностиреализации механизмов защиты в современных КС (например, механизмов администрированияпараметров безопасности).Условия реализации информационных потоков анализируются в модели Белла -ЛаПадулы с использованием определения ^-свойства. При этом предполагается, чтоинформационный поток возникает в случае, когда в состоянии КС найдется субъект,который имеет доступ на чтение к одному объекту и доступ на запись к другомуобъекту. В то же время функциональность субъекта может быть реализована такимобразом, что наличие описанных двух доступов не приводит к реализации информационногопотока.Третий недостаток модели Белла - ЛаПадулы имеет наибольшее практическое итеоретическое значение. Примеры запрещенных информационных потоков по времени,возникающих в результате реализации субъектами доступов к объектам, впервые былиописаны самими авторами модели. В то же время в связи с постоянным усложнениемсовременных КС, появлением в них новых функциональных возможностей, которыемогут быть эффективно использованы нарушителем для создания запрещенных информационныхпотоков по памяти и по времени, условия реализации информационныхпотоков продолжают исследоваться в теории компьютерной безопасности.При изучении модели Белла - ЛаПадулы условия реализации в КС запрещенныхинформационных потоков целесообразно рассмотреть на примерах.Пример 4. Классический пример реализации запрещенного информационногопотока по времени от объекта с высоким уровнем конфиденциальности к объектус низким уровнем конфиденциальности.Используем обозначения:fi - объект-файл с уровнем конфиденциальности High, который может содержатьзапись «А» или запись «В»;f 2 -объект-файл с уровнем конфиденциальности Low < High;s i - субъект с высоким уровнем доступа High, работающий по программе:Process s i ( f i : file)Open f i for read;While f i = «A» Do End;Close f i ;End.s2 - субъект-нарушитель с низким уровнем доступа Low, работающий по программе:Process s2(fi : file, f 2 : file)Open f 2 for write;Start si(fi);I f (Stop si) ThenWrite «B» to f 2;ElseWrite «A» to f 2;End IfClose f 2;End.Схема реализации информационного потока по времени приведена на рис. 12.Рис. 12. Пример реализации информационного потока по времениc использованием «зависания» субъектаСубъект-нарушитель s2 действует одновременно с субъектом si, проверяя егосостояние. При этом в зависимости от результата работы с конфиденциальнымобъектом-файлом f 1 субъекта s1, который либо сразу завершит работу, либо «зависнет», субъект s2 записывает данные в объект-файл f 2 с низким уровнем конфиденциальности.Пример 5. Пример реализации информационного потока по времени с использованиемсовместного доступа кооперирующих субъектов к файловой директории. Используемследующие обозначения:f 1 - объект-файл с уровнем конфиденциальности High, который может содержатьзапись « A » или запись « B »;f 2 -объект-файл с уровнем конфиденциальности Low < High;s 1 - субъект с высоким уровнем доступа High;s2 - субъект с низким уровнем доступа Low;dir - объект-директория с уровнем конфиденциальности Low;file - объект-файл в директории dir с уровнем конфиденциальности Low.Субъекты s1 и s2 кооперируют друг с другом. В согласованный момент временисубъект s1 считывает из f 1 его содержимое. Если оно «A», то он ничего не делает, если«B », то он открывает объект file на чтение (не нарушая свойств безопасности моделиБелла - ЛаПадулы). В тот же момент времени субъект s2 пытается удалить директориюdir. Если ему это удается, то он записывает в файл f 2 запись «A», если нет, тозапись «B» (большинство современных КС не разрешат субъекту удалить дирек

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