Содержание к диссертации
Введение
Глава 1. Дискреционная политика безопасности и ее моделирование 7
1. 1 Формальные политики безопасности 7
1.2 Формальные субъекты и объекты 8
1.3 Дискреционные модели 10
1.4 Применение дискреционных моделей 12
1.5 Модели дискреционного доступа 16
1.6 Дальнейшее развитие моделей HRU и Take-Grant 36
Глава 2. Базисный подход в модели HRU 40
2.1 Матрица доступов 40
2.2 Базисный подход в модели HRU 42
2.3. Монооперационные системы в базисе 47
2.4 Применение базисного подхода в операционных системах Windows 49
Глава 3. Алгоритмы проверки безопасности состояний компьютерной системы в модели Take-Grant 61
3.1 Исследование безопасности Take-Grant 61
3.2 Поиск tg-путей 61
3.3 Пример поиска tg-путей 62
3.4 Поиск островов 66
3.5 Пример поиска островов 67
3.6 Образование стяжек-островов 70
3.7 Распознаватели мостов 70
3.8 Примеры распознавания мостов 87
3.9 Алгоритмы поиска мостов 90
3.10 Примеры поиска мостов 102
3.11 Оценка общей трудоемкости 106
3.12 Применение модели Take-Grant для анализа безопасности Windows 107
Заключение 109
- Применение дискреционных моделей
- Базисный подход в модели HRU
- Применение базисного подхода в операционных системах Windows
- Пример поиска tg-путей
Введение к работе
Актуальность проблемы. Модели безопасности компьютерных систем позволяют формализовать процесс выявления возможных каналов утечки информации. С их помощью может быть проведено строгое доказательство устойчивости компьютерных систем к атакам злоумышленников [11-13, 38-41].
На сегодняшний день разработано несколько типов моделей безопасности, однако исторически первыми были дискреционные модели [15,19,20,34,47,56], основанные на принципе явного присвоения наборов разрешенных действий для каждой пары субъект - объект информационных отношений. Все модели безопасности компьютерных систем основываются на принципах впервые сформулированных в стандарте «Department of Defense Trusted Computer System Evaluation Criteria» [61], также известному как «Оранжевая книга», регламентирующему уровни безопасности информационных систем, минимальным требованием защищенности системы является наличие в ней разделения доступа. То есть, необходимо организовать работу системы так, чтобы каждый пользователь имел доступ лишь к тем частям информационной системы, которые необходимы ему для выполнения своих обязанностей. Разделение доступа в информационных системах реализуется через политику безопасности, представляющую собой нормы и правила эксплуатации системы [1-9, 11-13, 15-17].
Модель Харрисона-Руззо-Ульмана (Harrison-Ruzzo-Ulman, HRU) [15, 19, 20, 47, 68] была одной из первых моделей, ориентированных на анализ дискреционного доступа, и большинство более поздних моделей основаны на ее базовых положениях. Одним из основных результатов модели HRU является алгоритмическая неразрешимость задачи проверки произвольной системы на наличие каналов утечки информации. В связи с этим в работах [67, 77] предложен ряд ограничений модели, позволяющих выявить системы, для которых можно гарантировать защищенность. При этом существенно ограничивается функциональность компьютерной системы.
Модель Take-Grant [15, 20, 47, 71] более предсказуема, чем модель HRU. Для модели Take-Grant сформулированы условия, при которых в системе, работающей согласно этой модели, гарантированно не произойдет утечек информации. Однако способы проверки выполнимости данных условий не определены.
Целью диссертационной работы является развитие моделей дискреционного разграничения доступа HRU и Take-Grant, выявление новых классов безопасных компьютерных систем, построение алгоритмов проверки безопасности состояния компьютерной системы.
Методы исследования. При решении поставленных задач использовались математические модели, теория графов, теория алгоритмов, элементы булевой алгебры.
Научная новизна результатов исследований.
1. Впервые применен базисный подход для анализа безопасности модели HRU, что позволило расширить класс систем гарантированно защищенных от несанкционированного доступа.
2. Проведен анализ подсистемы безопасности операционных систем семейства Windows на возможность возникновения несанкционированных доступов с использованием дискреционных моделей безопасности.
3. Построены полиномиальные алгоритмы проверки возможности несанкционированного доступа заданного субъекта к заданному объекту.
Достоверность результатов работы. Научные результаты диссертационной работы получены с использованием методов хорошо зарекомендовавших себя при моделировании политик безопасности компьютерных систем. Проведено сравнение результатов моделирования с современными программными средствами защиты информации.
Практическая ценность заключается в разработке алгоритмов проверки безопасности компьютерных систем и выявлении безопасных состояний, которые могут найти применение в программных реализациях средств аудита безопасности вычислительных комплексов.
Основные положения, выносимые на защиту:
Возможно расширение дискреционной модели безопасности HRU за счет введения различных операций преобразования матриц доступа.
На множестве операций преобразования матрицы доступа возможно выделение базисного набора операций, через который линейно выражаются все остальные операции.
Рассмотрение компьютерных систем в различных базисах позволяет расширить класс систем, для которых допустимо доказательство гарантированной защищенности от несанкционированных доступов.
Алгоритмы проверки отсутствия несанкционированных доступов могут быть построены на основе алгоритмов на графах, поиска в ширину и поиска в глубину.
5. Проверка отсутствия каналов несанкционированного доступа между заданными субъектом и объектом может быть осуществлена за полиномиальное время.
Апробация работы. Основные результаты диссертации докладывались и обсуждались на следующих конференциях: Межвузовская научно-практическая конференция «Информационные технологии автоматизации и управления» (Омск, 2009); XIII международная научно-практическая конференция «Решетневские чтения» (Красноярск, 2009); Вторая международная научно-практическая конференция «Современные проблемы гуманитарных и естественных наук» (Москва, 2010), «Научное творчество XXI века» (Красноярск 2010), Вторая международная научно-практическая конференция «Наука в современном мире» (Москва, 2010), Сибирская научная школа-семинар с международным участием «Компьютерная безопасность и криптография» - SIBECRYPT'10 (Тюмень, 2010), а также обсуждались на научных семинарах Омского государственного университета.
Публикации. По теме диссертации опубликованы 14 научных работ, в том числе три статьи в коллективной монографии «Проблемы обработки и защиты информации книга 1 — Модели политик безопасности компьютерных систем» и две статьи в журнале, из списка рекомендованного ВАК.
Структура и объем работы. Диссертационная работа состоит из введения, трех глав, заключения и списка литературы. Работа содержит 116 страницы основного текста, 33 рисунка и 5 таблиц. Список литературы включает 80 наименований.
Применение дискреционных моделей
Согласно [5-9, 61, 66, 65] наличие дискреционного разделения доступов является минимальным требованием защищенности информационных систем. Потому при построении любой информационной системы, где требуется обеспечить защиту информации необходимо предусмотреть дискреционный контроль доступа. Наиболее очевидными примерами таких систем могут являться операционные системы и базы данных. И в тех и в других системах применяются дискреционные политики как в чистом виде, так и их расширения - групповые политики. В общих словах можно сказать, что групповые политики применяются в том случае, когда количество субъектов становится слишком велико чтобы отслеживать каждый из них. Тогда субъекты со схожими типами доступов группируются в роли (например, роль администратора, роль пользователя и т.п.) и права доступов устанавливаются для всей роли в целом. Подробнее ролевые политики описаны в [68-70].
Для баз данных объектами является любая сущность, содержащая конечную информацию: таблицы, представления, строки, столбцы и т.д. субъектами могут быть отдельные пользователи, группы пользователей, роли и хранимые процедуры (процедура может выступать как субъектом, так и объектом) [30, 45, 59, 79].
Все субъекты хранятся в специальных структурах системы управления базами данных (СУБД) и могут разделяться на несколько категорий. Набор категорий определяется производителем СУБД. Права доступов задаются чаще всего администратором СУБД (суперпользователем) явно или неявно (например, через роль). Однако отдельные объекты, такие как таблицы или представления, могут находиться во владении отдельных субъектов, и тогда владелец может самостоятельно распределять права доступов на эти объекты [30]. В зависимости от конкретной СУБД механизмы обеспечения безопасности данных могут отличаться, но описанные выше элементы дискреционных политик присутствуют всегда.
В операционных системах в качестве объектов выступают файлы, каталоги, устройства и т.п. Объектом может быть любой ресурс. Номинальными субъектами в операционных системах являются пользователи и группы, однако роль реально действующего субъекта выполняет процесс [14, 21, 29, 42, 46].
В UNIX-подобных операционных системах каждый пользователь имеет уникальный идентификатор (UID). Пользователь может входить в некоторые группы, каждая из которых также имеет свой идентификатор (GID). Таким образом, каждый пользователь может иметь несколько идентификаторов групп и один идентификатор пользователя. Когда пользователь запускает процесс -этот процесс наследует идентификатор пользователя. Более того, все процессы, запущенные некоторым родительским процессом с определенным идентификатором пользователя, наследуют этот идентификатор.
Объекты в UNIX-подобных системах также имеют идентификатор пользователя, определяющий владельца объекта. Кроме того, объект имеет единственный идентификатор группы, определяющий группу, которой он принадлежит.
С каждым объектом связан набор прав доступов, состоящий из трех операций: г — чтение, w — запись и х — исполнение. Набор операций может задаваться для пользователя, группы и всех прочих. Так, например, если некоторый субъект запрашивает какую-либо операцию над объектом, то происходит сравнение UID субъекта и объекта, и проверяется наличие разрешения на осуществление данной операции. Если UID не совпадают, то та же процедура осуществляется для GID. И наконец, если ни UID, ни GID не совпали, проверяется наличие разрешения на данную операцию для всех прочих, и если разрешение есть - операция осуществляется, если нет — отклоняется [21, 60].
В операционных системах Windows NT [29, 42, 46, 60, 73, 74] существует три класса операций, отличающихся типом субъектов и объектов: 1) разрешения - определяются для всех субъектов на объект любого типа (данные операции аналогичны операциям г, w, х в UNIX-подобных системах); 2) права пользователей — определяются для групп пользователей на осуществление некоторых системных операций (то есть объектом в данном случае выступает операционная система); 3) возможности пользователей — определяются для отдельных пользователей на выполнение действий, формирующих пользовательскую среду (например, изменение состава главного меню). При входе субъекта в систему, ему присваивается так называемый маркер доступа, который содержит идентификатор пользователя и групп, в которые пользователь входит. Права доступа к конкретному объекту хранятся в структурах называемых списками контроля доступа ACL (Access Control List). Ссылки на ACL объекта хранятся в дескрипторе безопасности объекта DS. Для каждого объекта существуют системный ACL (SACL, System ACL) и избирательный ACL (DACL, Discretionary ACL). DACL администрируется владельцем объекта и предназначен для разделения доступа к объету. SACL объекта администрируется системным администратором и предназначен для аудита действий с объектом. Списки контроля доступов состоят из записей АСЕ (Access Control Entry), каждая из которых отвечает за разрешение или запрет одного права доступа.
Базисный подход в модели HRU
Рассмотрим модель HR.U и ее представление в терминах операций над множеством матриц доступа. В данной модели ключевую роль играют примитивные операторы, из которых строятся команды преобразования матрицы доступов. В результате выполнения примитивного оператора осуществляется переход системы из состояния Q = (S, О, in) в новое состояние Q- (S , О , т1). Примитивные операторы модели HRU можно рассматривать как операции над множеством матриц доступа, следовательно, по теореме 1, они могут быть выражены через операции базиса Въ Проведем соответствующие построения: 1. Enter йк into m[s, о] — ввести право ак в ячейку m[s, о]: Enter ak into mfs, oJ= Inv(m[s, o], к). 2. Delete ak from mfs, oj— удалить право ak из ячейки mfs, oj: Delete ak from mfs, oJ= Inv(m[s, о], k). 3. Create subject s — создать субъект s (т. е. новую строку матрицы т): Create subject s=AddS(s, т). 4. Create object о — создать объект о (т. е. новый столбец матрицы т): Create object о= AddO(o, т). 5. Destroy subject s — уничтожить субъект s: Destroy subject s= DelS(s, m). 6. Destroy object о - уничтожить объект о: Destroy object о= DelO(о, m). Первый и второй примитивный оператор HRU представляются одинаково через операцию Inv(m[s, ], к), однако условие выполнения у них разное. В первом случае право ак первоначально отсутствует в ячейке матрицы доступов, а во втором случае наоборот присутствует. Как видим, примитивных операторов HRU на один больше чем базисных операций, следовательно, они не являются базисом. Построим базис на основе примитивных операторов HRU. Из примитивных операторов могут быть построены команды, состоящие из двух частей: 1. условие, при котором выполняется команда; 2. последовательность примитивных операторов. Общий вид команды: Command с(хи х2, ...,Xf) составноеусловие выполнения команды Последовательность примитивных операторов end command; Каждое состояние системы Qt является результатом выполнения некоторой команды с к предыдущему состоянию Qi-i. Набор операций {Enter ак into m[s,o], Create subject s, Create object o, Destroy subjects, Destroy object о} обозначим BH. Теорема 2.2. Набор операций Вн является базисом модели HRU. Доказательство. Так как работа команд HRU направлена исключительно на изменение матрицы доступа, покажем, что при помощи системы примитивных операторов можно построить любую матрицу доступа, то есть построить любую команду. Рассмотрим матрицы т и т принадлежащие множеству всех матриц доступаМ. Преобразуем твт при помощи системы примитивных операторов. Алгоритм преобразования можно записать с помощью следующей последовательности шагов: 1. Многократно применим оператор Destroy object о к матрице т до тех пор, пока количество объектов в матрице т не станет равным нулю. 2. Многократно применим оператор Destroy subject s к матрице т до тех пор, пока количество субъектов в матрице т не станет равным нулю. 3. Многократно применим оператор Create subject s к матрице т до тех пор, пока количество субъектов в матрице т не станет равным количеству субъектов в матрице т . 4. Многократно применим Create object о к матрице т до тех пор, пока количество объектов в матрице т не станет равным количеству объектов в матрице т . 5. Для каждого права ак применим оператор Enter ак into m[s,o], если право ак содержится в соответствующей ячейке m [s,o]. Таким образом, при помощи примитивных операторов, произвольно выбранная матрица тЄМ , может быть преобразована в произвольно выбранную матрицу т ЄМ , что доказывает полноту системы.
Докажем минимальность набора -бн. Согласно определению, набор операторов не будет минимальным, если какой-либо оператор из набора можно представить в виде набора других операторов принадлежащих данному набору. Допустим, что рассматриваемый набор не минимален. Тогда для преобразования произвольно выбранной матрицы /иЄМ в произвольно выбранную матрицу JH GM МОЖНО будет обойтись без какого-либо оператора.
Предположим, что излишним будет оператор Destroy object о. Преобразуем матрицу тЄМ в матрицу т Е.М , при этом число столбцов матрицы т больше числа столбцов матрицы т . Очевидно, что для преобразования матрицы т в т необходимо сократить число столбцов (т. е. субъектов) матрицы т. Однако, без оператора Destroy object о это сделать не возможно. Таким образом, при помощи набора операторов {Enter ак into m[s,o], Create subject s, Create object o, Destroy subject s} не возможно преобразовать произвольную матрицу доступов тЄМ в произвольную матрицу т єМ , что не удовлетворяет условию полноты. Следовательно, оператор Destroy object о нельзя исключить из базисного набора.
Предположим, что излишним является оператор Destroy subject s. Аналогично предыдущему случаю, рассмотрим преобразование матрицы mGM в матрицу т єМ , при этом число строк (т. е.. число субъектов) матрицы т больше числа строк т матрицы. Очевидно, что для сокращения числа субъектов не возможно обойтись без оператора Destroy subject s, т.е. набор операторов {Enter ак into m[s,o], Create subject s, Create object o, Destroy object о} не будет удовлетворять условию полноты. Следовательно, оператор Destroy subject s нельзя исключить из базисного набора.
Применение базисного подхода в операционных системах Windows
Пусть излишний — оператор Create object о. Аналогично, при преобразовании матрицы в матрицу такой, что количество столбцов (объектов) матрицы m меньше количества строк матрицы ш , необходимо будет увеличить количество столбцов матрицы т, однако без оператора Create object о сделать это не представляется возможным. Следовательно, оператор Create object о не возможно исключить из базисного набора.
Наконец, предположим, что излишним будет оператор Enter ак into m[s,o]. Рассмотрим случай преобразования матрицы mGM к матрице т ЄМ такой, что в некоторой ячейке m[s,o] матрицы т присутствует право ак, а в соответствующей ей ячейке m [s ,o ] матрицы т право ак отсутствует. Очевидно, что для преобразования матрицы необходимо выполнить добавление права. При помощи операторов {Create subject s, Create object о, Destroy subject s, Destroy object о} можно выполнять удаление и добавление столбцов и строк матрицы, при этом, если удаляется какой-либо субъект или объект, все права, связанные с ним, также удаляются. Но при помощи данного набора операторов не возможно выполнить добавление права в ячейку матрицы. Таким образом, без оператора Enter ак into m[s,o] не возможно преобразовать произвольную матрицу тЄМ к произвольной матрице т ЄМ , а это значит, что оператор Enter ак into m[s,o] не возможно удалить из базисного набора. Таким образом показано, что для преобразования матриц необходимы все операторы из набора Вн. Следовательно, рассматриваемый набор операторов будет минимальным.
Как видно из доказательства теоремы, для построения полной системы используется только пять из шести примитивных операторов. Следствие 2.1. Примитивный оператор Delete ак from m[s,o] может быть представлен в виде суперпозиции других примитивных операторов модели HRU. Доказательство. Рассмотрим матрицы шит такие, что количество строк и количество столбцов в этих матрицах равны. В какой-либо ячейке матрицы т отсутствует право ak, которое присутствует в соответствующей ячейке матрицы т. Все остальные ячейки матриц ттлт полностью совпадают. Преобразуем матрицу mum способом, описанным в доказательстве теоремы 2. С другой стороны то же преобразование выполняет оператор Delete ak from m[s,o]. Следовательно, для удаления права из матрицы т можно обойтись без оператора Delete ак from m[s,o]. Это доказывает, что оператор Delete ак from m[s,o] является избыточным и представляется в виде последовательности операторов из набора Вн. Безопасность системы определяется некоторыми условиями на начальное состояние системы Q0, а также особенностями системы команд. Как было показано в теореме 1.1, задача проверки безопасности произвольной системы алгоритмически неразрешима. Однако можно выделить отдельные классы систем, для которых возможно построение алгоритма, проверяющего безопасность системы. Важным случаем являются монооперационные системы (определение 1.1). Доказательство безопасности монооперационных систем приведено в [78, 80]. Расширим понятие монооперационной системы, с учетом существования базисного набора операций. Определение 2.2 Монооперационная система в базисе В - это такая система, каждая команда которой содержит ровно один оператор из базиса В. Теорема 2.3 Существует алгоритм, проверяющий: является ли исходное состояние монооперационной системы в базисе Б/ безопасным по отношению к праву ак. Доказательство. Необходимо показать, что число последовательностей команд монооперационной системы в базисе, которые необходимо проверить, ограничено и сами команды имеют конечную длину. В этом случае алгоритмом проверки безопасности будет являться алгоритм перебора всех последовательностей команд и проверки их конечного состояния на отсутствие утечки права ак. Нет необходимости рассматривать команды, содержащие операции DelO(o,m) и DelS(s,m), так как необходимо проверить наличие права после выполнения команды, а не его отсутствие. Также нет необходимости рассматривать последовательности, содержащие более одной операции AddS(o.m) и команды, содержащие операции AddO(o,m), так как все последовательности, которые проверяют или вносят права в новые элементы матрицы, могут быть заменой параметров в командах, представленных последовательностями, действующими с существующими субъектами и объектами. Одна операция AddS(o,m) необходима, если в начальном состоянии системы субъекты отсутствуют. Таким образом, необходимо рассмотреть только последовательности команд, которые содержат операции Inv(m[s,o],k) и одну операцию AddS(o,m). Число различных операций Inv(m[s,o],k) можно вычислить следующим образом: w= j(5,0+l)((9o+l), где А - множество всех типов доступов в компьютерной системе. Все команды, содержащие одну и ту же операцию, но разные условия, объединяются в одну команду с составным условием. Таким образом, число последовательностей команд, которые необходимо проверить равняется п!, при этом длина каждой команды равна п. Непредсказуемость сложных систем, является одним из главных недостатков модели HRU. Наложение условия монооперационности значительно сужает класс безопасных систем. При введении понятия базиса монооперационной системы, появляется возможноть рассматривать более широкий класс систем, которые также будут являться безопасными. Для того, чтобы проверить является ли компьютерная система безопасной, достаточно найти такой базис, в котором она будет монооперационной.
Пример поиска tg-путей
Рассмотрим поиск моста типа t . Для начала опишем алгоритм неформально. В начале работы алгоритм разбивает все множество вершин-объектов исходного графа на два подмножества О и О.. В множество О попадают те вершины, до которых существует мост заданного вида, все остальные вершины заносятся в множество Оґ В самом начале работы алгоритма в множестве Оу находится только одна вершина (начальная вершина). Далее алгоритм просматривает все дуги графа, инцидентные вершинам из множества Ог и если обнаруживается дуга вида 1, соединяющая вершину еу из Ог с вершиной ei из Ot, то в удаляется из Oi и заносится в О. После просмотра всех дуг графа в Ог может быть занесено сразу несколько вершин, то есть мощность Ог увеличится на некоторое число, а мощность О. уменьшится на это же число. Если вершина / попадет в множество Of то это значит, что в графе существует путь заданного вида и алгоритм заканчивает работу. Иначе, процедура повторяется для измененных Ог и О.. Однако возможна ситуация, когда после просмотра всех дуг в Ог не будет добавлено ни одной вершины. Это возможно, когда между вершинами из О и вершинами из не существует дуг вида 1 . Чтобы отловить данную ситуацию, нужно проверить мощности множеств, которыми мы оперируем: если мощности множеств не изменились, значит необходимо закончить работу алгоритма с выдачей сообщения о том, что моста заданного между рассматриваемыми островами не существует. Формально алгоритм будет состоять из трех основных этапов. Перед началом работы алгоритма разобьем множество О на два подмножества Ог и 0{, причем 0=ОгиО; . Этап 1. Вершина s заносится в множество О, все остальные вершины заносятся в Оґ Этап 2. Просматриваются все дуги графа, началом которых являются вершины из 0}, если существует ft е) ei заносится в множество О и удаляется из 0{. Здесь егєОг , е,єО. . Когда все дуги инцидентные вершинам из Ог множества будут просмотрены - переходим на третий этап. Этап 3. Если после выполнения этапа 2 вершина / оказалась во множестве Of то алгоритм заканчивает свою работу: мост заданного вида в графе существует. Если после выполнения этапа 2 мощности множеств О. и О. не изменились, алгоритм также заканчивает работу: моста заданного вида в графе не существует. В противном случае — возвращаемся на этап 2. Замечание. В зависимости от задачи можно предусмотреть разные реализации алгоритма. Например, если требуется лишь показать наличие или отсутствие моста между указанными вершинами, то приведенного выше описания будет достаточно - алгоритм выдает сообщение о результатах своей работы. Если же требуется найти сам мост, то необходимо дополнительно каким-либо образом поддерживать множество отмеченных вершин и дуг, например, после каждого шага второго этапа строить граф путей (который не обязательно будет деревом) или определенным образом окрашивать выбранные вершины и дуги. Проведем оценку работы предложенного алгоритма. Пусть исходный граф содержит TV вершин. Так как граф ориентирован, то в случае его полно связности количество дуг в нем будет равно N(N-1). Количество повторений этапа 2 можно ограничить количеством вершин графа, так как в случае если после каждого выполнения этапа в множество О будет заноситься по одной вершине, то мост в графе будет найден за N шагов. В общем случае во множество Ог за каждое выполнение этапа 2 будет заноситься более одной вершины, то есть мост будет найден меньше чем за N шагов. Если же моста не существует, то на каком-то шаге i N не найдется дуги нужного вида и алгоритм ничего не занесет в множество Oj,, то есть мощность множества останется неизменной, тогда алгоритм прервется с выдачей соответствующего сообщения. Таким образом, сложность работы алгоритма можно оценить как О {N-N-{N—l)) или 0($г). Теорема 3.1 Приведенный выше алгоритм корректно находит мост типа — t Доказательство. Во-первых нужно доказать, что алгоритм вообще закончит свою работу (сходимость алгоритма), во-вторых - что алгоритм найдет мост нужного вида (корректность алгоритма). Сходимость можно показать исходя из того, что множество вершин-объектов исходного графа конечно. Алгоритм разбивает множество О на Oi и 0}1 причем 0=OrUOi . На каждом шаге второго этапа алгоритма либо какая-то вершина удаляется из О. и заносится в О при этом мощности обоих множеств соответственно изменяются, либо перемещения вершин не происходит — мощности множеств не меняются и алгоритм заканчивает работу. Пусть 0=М . Возможно три варианта развития событий. 1. Все вершины из Oi будут перенесены в Of тогда на следующем шаге алгоритм закончит свою работу, так как мощности множеств менять будет уже не возможно. Всего алгоритм совершит М+1 шагов. 2. На шаге к М алгоритм обнаружит мост. Алгоритм закончит работу, при этом совершит к шагов. 3. На шаге к М алгоритм обнаружит, что мощности множеств О и О не изменились. Алгоритм закончит работу, при этом совершит к шагов. Таким образом, алгоритм в любом случае закончит работу не зависимо от того, присутствуют в графе мосты или нет. Корректность алгоритма покажем индукцией по длине моста (и). В качестве базы индукции мы не можем выбрать п=1, так как это бы означало, что начальная и конечная вершина моста соединены дугой t ,и, следовательно, принадлежат одному острову. Поэтому в качестве базы выберем п-2 и покажем, что алгоритм найдет такой мост. Ситуация, когда в графе присутствует мост длины, 2 изображена на рисунке 3.15. С вершиной s связана как минимум одна дуга вида f , соединяющая вершины s я х. С вершиной х, в свою очередь, связана как минимум одна дуга вида t , соединяющая д: и/.
