Объектно-функциональная верификация информационной безопасности распределенных автоматизированных информационных систем таможенных органов

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

Автореферат диссертации на соискание ученой степени
доктора технических наук

Объектно-функциональная верификация информационной безопасности распределенных автоматизированных информационных систем таможенных органов

Специальность: 05.13.19 - «Методы и системы защиты информации, информационная безопасность»

Скиба В.Ю.

Работа выполнена в Государственном образовательном учреждении высшего профессионального образования «Санкт-Петербургский государственный политехнический университет».

Официальные оппоненты:

Доктор технических наук, профессор Присяжнюк Сергей Прокофьевич

Доктор технических наук, профессор Гаценко Олег Юрьевич

Доктор технических наук, профессор Жуков Игорь Юрьевич

Ведущая организация - Всероссийский научно-исследовательский институт проблем вычислительной техники и информатизации.

Общая характеристика работы

Актуальность работы. В Концепции национальной безопасности Российской Федерации угрозы национальным интересам России в информационной сфере поставлены в один ряд с угрозами в экономической, внутриполитической, социальной, международной, военной, пограничной, экологической сферах. В соответствии со Стратегией развития информационного общества в Российской Федерации информационное общество характеризуется высоким уровнем развития информационных и телекоммуникационных технологий и их интенсивным использованием гражданами, бизнесом и органами государственной власти. Одной из основных задач определено противодействие использованию потенциала информационных и телекоммуникационных технологий в целях угрозы национальным интересам России. Для решения поставленных задач сформулированы направления реализации стратегии, среди которых обеспечение безопасности функционирования информационных и телекоммуникационных систем ключевых объектов инфраструктуры России. В Доктрине информационной безопасности Российской Федерации выделяются четыре вида угроз информационной безопасности, одним из которых являются угрозы безопасности информационных и телекоммуникационных систем.

Распределенные автоматизированные информационные системы (РАИС) таможенных органов включены в Перечень критически важных информационных систем Российской Федерации. Следовательно, научные исследования в области обеспечения информационной безопасности РАИС таможенных органов являются актуальными и своевременными.

Крупный вклад в развитие теории и практики информационной безопасности внесли И.И. Быстров, В.А. Герасименко, О.Ю. Гаценко, А.А. Грушо, В.С. Заборовский, П.Д. Зегжда, Д.П. Зегжда, В.А. Конявский, А.А. Малюк, А.А. Молдовян, Л.Г. Осовецкий, М.П. Сычев, С.П. Присяжнюк, С.П. Расторгуев, А.Г. Ростовцев, В.А. Садовничий, А.А. Стрельцов, А.А. Тарасов, Л.М. Ухлинов, В.П. Шерстюк, А.Ю. Щербаков и др. В их работах разработана концепция защиты информации, обоснованы принципы реализации управляемых процессов обеспечения безопасности информации и принципы построения систем защиты информации объектов информатизации и электронных документов на основе построения изолированной программной среды с использованием программно-аппаратных средств защиты информации, рассмотрены теоретические аспекты и методология организации криптографической защиты информации, развита технология создания информационно-безопасного программного обеспечения в условиях наличия непреднамеренных и намеренных несанкционированных включений - закладок, а также сформулированы основные модели угроз и нарушителей технологической и эксплуатационной безопасности информации. В тоже время, данные работы либо предполагали замкнутый или детерминированный цикл разработки АИС, либо были ограничены только одним направлением обеспечения безопасности информации, например, предусматривающего применение встраиваемых аппаратно-программных средств защиты информации, криптографических методов или средств обеспечения сетевой безопасности.

В настоящее время все большее распространение получают ведомственные или корпоративные РАИС, которые объединяют в единый контур большое число разнородных территориально распределенных объектов и включают в себя разнообразные средства вычислительной техники, различное телекоммуникационное оборудование, многообразное общесистемное и прикладное программное обеспечение. При этом необходимо учитывать, что РАИС (в том числе, таможенных органов) постоянно находятся одновременно в стадиях модернизации и эксплуатации. В этих условиях повысить эффективность обеспечения безопасности информации возможно за счет применения методов формализации спецификации системы обеспечения безопасности информации (СОБИ) и ее последующей верификации на этапах проектирования (модернизации) и эксплуатации РАИС.

Необходимость в более точном формировании требований неизбежно ведет к разработке формальных методов формализации спецификаций. Традиционный подход к формализации спецификаций систем предполагает, что детальное проектирование и разработка систем начинается после завершения разработки спецификации. Предлагаемый подход предполагает быстрое развитие по эволюционной спирали, в процессе которого спецификация РАИС подвергается постоянному уточнению. Целью является создание комбинации компонентов (функциональных и объектовых подсистем) РАИС, а не монолитной системы. Таким образом, разработка спецификаций одновременно является и формированием требований и проектированием системы. Наличие спецификаций значительно упрощает модернизацию СОБИ РАИС и позволяет вводить в эксплуатацию отдельные подсистемы, не дожидаясь завершения разработки системы в целом.

Под верификацией СОБИ РАИС понимается подтверждение соответствия системы заданным требованиям. При этом применение методов верификации на этапе проектирования СОБИ РАИС позволяет обеспечивать технологическую безопасность, т.е. обнаруживать и предотвращать нарушения безопасности информации на этапе проектирования РАИС. Применение методов верификации на этапе функционирования СОБИ РАИС позволяет обеспечивать эксплуатационную безопасность, т.е. обнаруживать и предотвращать нарушения безопасности информации на этапе эксплуатации РАИС. Все выше перечисленное определяет актуальность темы диссертационного исследования.

Целью диссертации является разработка формальных методов и моделей верификации СОБИ РАИС таможенных органов, позволяющих эксплуатировать системы в условиях постоянного изменения объектов и функций объектов защиты.

Объект и предмет исследования. Объектом являются РАИС таможенных органов, а предметом - модели и методы управления безопасностью информации и оценивания эффективности систем обеспечения информационной безопасности, а также средства обеспечения внутреннего аудита и мониторинга состояния объекта, находящегося под воздействием угроз нарушения его информационной безопасности.

Задачи исследования:

Структурно-функциональный анализ РАИС таможенных органов и обоснование модели их жизненного цикла.

Формализация проблемы обеспечения безопасности информации в РАИС с мультикаскадной спиралевидной моделью жизненного цикла.

Разработка математического аппарата формального описания (спецификации) РАИС на основе временных алгебраических сетей Петри.

Формализованное описание РАИС с учетом временных и функциональных требований к характеристикам обеспечения безопасности информации.

Разработка методов верификации формальной спецификации СОБИ РАИС на этапе разработки (модернизации) системы.

Разработка модели адаптивного управления процессами обеспечения безопасности информации с использованием методов верификации спецификации СОБИ РАИС.

Обоснование системы показателей и оценки эффективности обеспечения безопасности информации в РАИС.

Практическое применение разработанных методов, моделей и методик к обоснованию структуры типовой РАИС в защищенном исполнении и при создании конкретных РАИС таможенных органов.

Методы исследования. Для решения поставленных задач использовались методы теории сложности систем, теории множеств, прикладной теории алгоритмов, теории исследования операций, теории конечных автоматов, теории вероятности, а также аппарат сетей Петри и методы структурно-функционального анализа и проектирования.

Основные научные результаты, выносимые на защиту и их новизна

1. Комплекс методов и методик верификации СОБИ РАИС на основе поиска достижимых состояний временных алгебраических сетей Петри (ВАСП) в глубину и ширину, а также верификации расчетных программ в составе РАИС на основе функций самосводимости.

2. Модель адаптивного управления процессами обеспечения безопасности информации на основе динамической верификации сетевой модели спецификации (СМС) СОБИ РАИС, используемой в качестве эталонной модели объекта управления.

3. Комплекс моделей, методов и методик разработки спецификации СОБИ РАИС, включая СМС СОБИ РАИС как иерархическое множество ВАСП, методы объектной и функциональной декомпозиции ВАСП и методику структурно-функционального формирования СМС СОБИ РАИС.

4. Временные алгебраические сети Петри как новое расширение аппарата сетей Петри, учитывающее ограничения на время выполнения операций в РАИС и на состояние ее элементов.

5. Структура типовой РАИС в защищенном исполнении с практическими реализациями совокупности РАИС таможенных органов.

Научная новизна полученных результатов заключается в том, что:

- предложена мультикаскадная спиралевидная модель жизненного цикла РАИС;

- модифицирован аппарат алгебраических сетей Петри за счет введения временных параметров;

- предложено комплексное совместное применение методов двухэтапной оптимизации структуры и характеристик РАИС, формального описания систем с использованием ВАСП и функциональной и объектовой декомпозиции данных сетей для формирования СМС СОБИ РАИС;

- модифицированы методы поиска достижимых маркировок ВАСП в глубину и ширину для проведения верификации СМС СОБИ РАИС на этапе проектирования РАИС для обеспечения ее технологической безопасности;

- предложена модель адаптивного управления безопасностью информации в РАИС, использующая методы верификации СМС СОБИ РАИС для получения эталонного состояния системы с учетом времени прогноза, для обеспечения эксплуатационной безопасности РАИС.

Научная значимость диссертации состоит в развитии теории обеспечения безопасности информации в части разработки моделей, методов и методик формализации спецификации СОБИ РАИС, характеризуемых мультикаскадной спиралевидной моделью жизненного цикла, и последующей ее верификации как на этапе проектирования (разработки, модернизации) РАИС, так и на этапе ее эксплуатации.

Практическая ценность работы. Практическая ценность полученных результатов заключается в том, что в диссертации решена важная народнохозяйственная проблема разработки моделей, методов и методик верификации СОБИ РАИС, позволяющих эксплуатировать системы в условиях постоянного изменения объектов и функций объектов защиты.

Результаты диссертационных исследований использовались при непосредственном участии и под руководством автора для разработки целого ряда РАИС таможенных органов, основными из которых являются Система ведомственных удостоверяющих центров таможенных органов (СВУЦТО); Автоматизированная система внешнего доступа таможенных органов (АСВД ТО); Система обеспечения безопасности информации Единой автоматизированной информационной системы таможенных органов (СОБИ ЕАИС ТО).

Внедрена информационная технология представления участниками внешнеэкономической деятельности (ВЭД) сведений таможенным органам в электронной форме. Реализация технологии в 2007 году отмечена 2 наградами Национальной отраслевой премии «За укрепление безопасности России», а в 2009 году - «Серебряным кинжалом».

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

- при проведении НИОКР в Институте проблем информационной безопасности МГУ М.В. Ломоносова, в Научном центре Российской таможенной академии, 50 ЦНИИ ВКС, 4 ЦНИИ МО;

- при разработке различных РАИС таможенных органов;

- при разработке нормативно-правового обеспечения информационной безопасности таможенных органов;

- при разработке средств обеспечения сетевой безопасности в Научно-производственном объединении робототехники и кибернетики;

- в учебном процессе МГТУ им. Н.Э. Баумана.

Апробация и публикация основных результатов работы. Основные результаты диссертации опубликованы в 2 монографиях, 1 учебном пособии, 17 статьях (в том числе в 8 изданиях, рекомендованных ВАК для опубликования результатов диссертаций на соискание ученой степени доктора наук), 57 отчетах по НИОКР, использовались при разработке 2 учебных программ в МГТУ им. Н.Э. Баумана и 47 правовых нормативных актов ФТС России. Основные результаты работы более 40 раз докладывались на международных и отечественных конференциях и семинарах.

Структура и объем работы. Диссертация состоит из введения, шести глав, заключения и списка литературы. Общий объем работы составляет 321стр. машинописного текста, 27 рисунков и 7 таблиц. Список литературы содержит 470 наименований, включая труды автора.

Содержание работы

Введение. Обоснована актуальность темы диссертации, дана краткая ее характеристика, сформулированы цель и основные задачи исследования, приведены положения, выносимые на защиту, кратко изложено содержание разделов диссертации.

Глава 1. Анализ современного состояния в области обеспечения безопасности информации в РАИС таможенных органов и постановка научной проблемы. Проведен структурно-функциональный анализ РАИС таможенных органов (рис. 1) и, в первую очередь, ЕАИС ТО. Структура ЕАИС ТО является иерархической и соответствует структуре таможенных органов, при этом подразделения таможенных органов размещаются более чем в десяти тысячах территориально-разнесенных административных зданиях. Элементами ЕАИС ТО являются технически, информационно и программно совместимые комплексы средств автоматизации (локальные вычислительные сети с телекоммуникационным оборудованием, общим и специальным программным и информационным обеспечением), объединенные ведомственной интегрированной телекоммуникационной сетью. Всего эксплуатируется более 10 тыс. ЛВС и более 300 комплексов специальных программных средств, объединенных логически в более чем 50 функциональных (основных, вспомогательных и обеспечивающих) подсистем. Техническая архитектура и функционально-программная инфраструктура ЕАИС ТО постоянно подвержена изменениям, связанным с разработкой и вводом в эксплуатацию новых компонент и непрерывной доработкой эксплуатируемых компонент (в связи с изменениями нормативно-правовой базы или совершенствованием процессов таможенного оформления и контроля). Ежегодно осуществляется дооснащение средствами вычислительной техники, телекоммуникационным оборудованием, общесистемным программным обеспечением и сертифицированными средствами защиты информации.

Рис. 1. Обобщенная структура РАИС таможенных органов

Приведено обобщенное описание модели угроз безопасности информации, характеризуемой наличием внешних и внутренних источников угроз, а также объективными и субъективными факторами их проявления. При этом выделены технологические и эксплуатационные угрозы. Модель нарушителя включает в себя как внутренних и внешних санкционированных пользователей ЕАИС ТО, так и злоумышленников.

На основании проведенного структурно-функционального анализа обоснована мультикаскадная спиралевидная модель жизненного цикла РАИС, в которой для каждой функциональной или объектовой подсистемы циклически повторяется классическая каскадная модель, причем период цикла для каждой подсистемы различен и не совпадает по времени начала и окончания. Приведена формальная постановка научной проблемы, обоснована методическая схема диссертационного исследования.

Глава 2. Математический аппарат формализации спецификаций и их верификации. Анализ известных методов формализации спецификации и верификации протоколов и систем (сети Петри, язык АДА, язык SPECIAL для системы HDM, конечные автоматы, исчисление взаимодействующих процессов и т.д.) позволил выделить аппарат алгебраических сетей Петри как наиболее мощное средство для формализации спецификаций СОБИ РАИС. Необходимость адекватного представления сложного характера процессов обеспечения безопасности информации в РАИС обусловила целесообразность расширения аппарата алгебраических сетей Петри за счет введения временных параметров. В результате были предложены ВАСП.

Временной алгебраической сетью Петри называется кортеж S=<PF,T,A,V,D,Q,H,,M,M₀>, где Р={p₁,…,p_n} и F={f₁,…,f_m} - конечное множество позиций типа «р» (LIFO, «last in, first out») и типа «f» (FIFO, «first in, first out») соответственно; T={t₁,…,t_r} - конечное множество переходов; А={a,b,…} - конечный алфавит; - отображение, помечающее дуги, соединяющие позиции с переходами и переходы с позициями; D - вектор с временными параметрами сети, определяющий длительности (задержки) срабатывания переходов; Q - вектор, определяющий активизированные в переходы сети, элементы вектора принимают значения 0 или 1 (переход не выполняется или выполняется); Н - вектор, определяющий время инициализации (активизации) выполнения переходов; ф - время функционирования сети; M: PF A^* и M₀: PF A^* - текущая и начальная маркировка позиций.

Для каждого элемента x PFT сформулированы понятия множеств выходов и входов .

Динамика функционирования ВАСП описывается:

- условием возбуждения перехода:

-

(1)

- условием завершения выполнения перехода:

(2)

- рекуррентными уравнениями динамики изменения состояния сети:

_k = _k + _k

Q_k = Q_k-1 + U_k - U_k

H_k = H_k-1 + _kU_k - (_kU_k - D) U_k

(3)

где _k - интервал между тактами срабатывания переходов сети.

Последовательность переходов t^k T^* (kN, t^k = t₁…t_k, {t_i}T, T^* - множество конечных слов на алфавите T) называется разрешенной для маркировки М и дает маркировку M (обозначается ), если выполнены следующие условия:

а) t^k = M = M;

б) .

Маркировка M называется достижимой из маркировки М, если существует конечная последовательность t^k T^*, такая, что . Множеством достижимых маркировок ВАСП начиная с маркировки М называется множество . Множество достижимых маркировок ВАСП S начиная с начальной маркировки позиции М₀ обозначается R(S) = [M₀). Множество достижимых маркировок позволяет определить три языка:

1. Множество переходов t ВАСП S, разрешенных при начальной маркировке M₀: .

2. Множество последовательностей переходов t^k ВАСП S, разрешенных из маркировки M₀ за i тактов: .

3. Множество последовательностей переходов t^k ВАСП S, при которых достигается маркировка M, начиная с маркировки M₀: .

С использованием языков L(S), L^*(S) и L(S, M) рассмотрены свойства ВАСП. Позиция x называется ограниченной, если n N - такое, что при M R(S) имеет место |M(x)| n, где |a| обозначает длину слова a. Сеть S называется ограниченной, если ограниченна каждая ее позиция. Сеть S называется сетью без блокировки, если для любого x L^*(S) существует переход t T, такой, что x t L^*(S).

Теорема 1. ВАСП S ограничена тогда и только тогда, когда множество R(S) конечно.

Теорема 2. Множество X A^* является кодексом, если и только если пересечение любых двух свободных моноидов, заданных образующими X_i и X_j (X_i X, X_j X) не содержит слов a X^*, таких, что

{x_i | x_i X_i, x_i a} \ {x_j | x_j X_j, x_j a} V, V {x_j | x_j X_j, x_j a} \ {x_i | x_i X_i, x_i a} .

Теорема 3. ВАСП является корректной, если она является ограниченной, активной и без блокировок, а множество всех слов образует кодекс.

В главе также определены основные операции с ВАСП: объединение, исключение, дополнение.

Глава 3. Комплекс моделей, методов и методики формирования спецификации СОБИ РАИС. Под спецификацией СОБИ РАИС понимается описание структуры и функций РАИС с использованием ВАСП. Разработка спецификации СОБИ РАИС основывается на следующих принципах (правилах) формализации:

Правило 1. Каждому элементу СОБИ и РАИС (включая ресурсы) ставится в соответствие позиция ВАСП. При этом маркировка позиции отражает состояние специфицируемого элемента.

Правило 2. Каждому процессу (операции) по обработке информации сопоставляется один или несколько переходов ВАСП. При этом инцидентные дуги перехода определяют элементы РАИС, задействованные при выполнении операции. Маркировка входящих и выходных дуг перехода определяет необходимое состояние задействованных элементов до начала выполнения операции (предусловия) и после окончания операции (постусловия). Каждому переходу назначается временной параметр задержки срабатывания перехода, характеризующий длительность выполнения операции.

Правило 3. Каждому элементарному состоянию моделируемых элементов СОБИ и РАИС сопоставляется конкретное слово на алфавите А. Каждое слово специфицирует только одно состояние. Множество всех слов, специфицирующих состояния, образует кодекс на алфавите А.

Правило 4. Каждому постусловию и предусловию выполнения специфицируемого процесса (операции) обработки информации или по обеспечению ее безопасности сопоставляется конкретное слово на алфавите А. Множество слов постусловий и предусловий образует кодекс на алфавите А.

При этом необходимо обеспечить выполнение следующих принципов (условий) корректности спецификации СОБИ РАИС:

1. Полнота и адекватность, т.е. отображение всех существенно значимых элементов и атрибутов, а также их взаимосвязи и характеристик процессов функционирования РАИС.

2. Стандартность и унифицированность внутренней структуры элементов РАИС и взаимодействия между ними.

3. Модульность, т.е. автономной организации элементов РАИС, позволяющей стандартными способами объединять элементы в сложные структуры и заменять любой элемент и их совокупности.

4. Гибкость, т.е. практически неограниченной возможности расширения и реорганизации структуры одних компонент РАИС без изменения (или без существенного изменения) других компонент.

5. Прозрачность, т.е. простоты изучения структурных элементов РАИС, любой их совокупности и взаимосвязей между элементами.

6. Безопасность. Спецификация учитывает требования безопасности, если в ней четко определено функционирование СОБИ РАИС для всех нештатных ситуаций.

7. Непротиворечивость. Спецификация непротиворечива, если ее положения не противоречат друг другу или другим спецификациям.

8. Верифицированность. Спецификация проверяема, если разработанная система может быть подвергнута проверке на соответствие положениям этой спецификации.

9. Правильность означает, что РАИС строго соответствует всем функциональным и интерфейсным спецификациям, а также удовлетворяет в пределах допусков всем спецификациям технических характеристик.

10. Адаптируемость означает, что РАИС или ее подсистемы можно легко использовать или приспособить для выполнения новых функций.

В то же время, ВАСП для всей РАИС в целом может получиться достаточной большой, что существенно увеличит время ее верификации. В связи с этим предложено описывать спецификацию СОБИ РАИС в виде СМС СОБИ РАИС, которая представляет собой совокупность: SMS = <SS, {SSO_i |i[1,N]},{SSF_j |j[1,F]},{SSP_k |k[1,Z]},{SSK_P |p[1,]}>, где SS - внешняя спецификация РАИС; SSO и SSF - множество спецификаций объектовых и функциональных подсистем РАИС (N и F соответственно количество объектовых и функциональных подсистем РАИС); SSP - множество спецификаций элементов РАИС, находящихся под контролем СОБИ; SSK - множество спецификаций специализированных компонент, разрабатываемых только для данной РАИС. Каждая спецификация представляет из себя ВАСП.

Для построения СМС СОБИ РАИС предложены методы структурной и функциональной декомпозиции. Функциональная декомпозиция заключается в разложении некоторой функции (процесса) на подфункции. Выделяется:

1. Функциональная декомпозиция внешней спецификации (обозначение: , условие полноты: ).

2. Функциональная декомпозиция спецификации объектовой подсистемы (обозначение: , условие полноты: и ).

Теорема 4. Для перехода t исходной ВАСП S в результате функциональной декомпозиции получена ВАСП SF. ВАСП SF является корректной функциональной декомпозицией перехода t исходной ВАСП S тогда и только тогда, когда выполняются условия:

- для ВАСП SF существует конечное не пустое множество последовательностей переходов L(S, M)={t^k T^*} такое, что .

- время функционирования ВАСП SF для выполнения последовательности переходов t^k равно длительности срабатывания перехода t исходной ВАСП S: .

Объектовая декомпозиция заключается в разложении некоторой системы (подсистемы, объекта) на подсистемы, компоненты. Выделяется:

1. Объектовая декомпозиция внешней спецификации (обозначение: , условие полноты ).

2. Объектовая декомпозиция спецификации функциональной подсистемы (обозначение: , условие полноты: и ).

Методы декомпозиции СМС СОБИ РАИС необходимы для детализации либо элементов, задействованных при обеспечении безопасности информации (метод структурной декомпозиции), либо самих процессов обеспечения безопасности информации или модели нарушителя (метод функциональной декомпозиции). Пример фрагмента СМС для информационной технологии представления участниками ВЭД сведений таможенным органам в электронной форме приведен на рис. 2.

Разработана методика структурно-функционального формирования СМС (СФС) СОБИ РАИС (рис. 3), которая основывается на принципах многоступенчатой оптимизации при соблюдении ряда условий, наиболее существенным из которых является вариантность разработки. При СФС СОБИ рассматривается трехуровневое дерево критериев и ограничений, формируемых при выборе конкретного варианта структуры СОБИ. Это дерево связывает первый уровень (СОБИ в целом) - со 2-м (промежуточным) уровнем, на котором располагаются различные подсистемы СОБИ.



а) исходная сеть

б) объектовая декомпозиция позиции p₃

в) функциональная декомпозиция перехода t₁

Рис. 2. Пример объектной и функциональной декомпозиции СМС



Рис. 3. Схема методики СФС СОБИ РАИС

В свою очередь, 2-й уровень связан с 3-м (нижним), охватывающим отдельные элементы - программно-аппаратные средства, входящие в различные подсистемы СОБИ.

На первом этапе методики СФС СОБИ РАИС формируется множество вариантов структур и осуществляется локальная оптимизация, в рамках которой выбираются состав и структура подсистем (локально оптимальные или близкие к оптимальным варианты). Для конкретного задания функции оценки на этом этапе используются методы теории нечетких многокритериальных задач оптимизации. Пусть A - множество допустимых структур СОБИ, z₁, z₂, ..., z_n - целевые функции, - множество мер неопределенности, адекватно отражающих неполноту информации об условиях функционирования СОБИ. На высоких уровнях абстракции множеством охватываются структурные, параметрические, режимные и эксплуатационные меры неопределенности. Множество допустимых исходов при сочетании элементов множества действий с элементами множества мер неопределенности, может быть описано декартовым произведением A. Целевые функции при этом получают смысл отображений: . Рациональный принцип принятия решений S в этом случае определяется следующими условиями:

1. S (A, , Z) A, т.е. решениями могут быть лишь допустимые структуры СОБИ;

2. a S (A, , Z) и b A при Z (a, ) = Z (b, ); b S (A, , Z), т.е. две структуры, имеющие одинаковые векторные оценки, либо обе являются, либо обе не являются решениями;

3. S (A, , Z) eff (A, , Z), где множество eff (A, , Z) - эффективная граница образа множества A, полученного с помощью отображения Z, и является множеством всех допустимых векторных оценок. Определение вариантов структур СОБИ, оптимальных по Парето, представляет собой классическую задачу векторной оптимизации, состоящей в определении множества: ;

4. S (A, , Z) , т.е. существует, по крайней мере, одно решение;

5. если (A, , Z) и (B, , Z) - две ситуации принятия решений, то , т.е. лучшие структуры для множества A остаются лучшими структурами для сокращенного множества B, если эти структуры нельзя исключить из рассмотрения.

Существенным моментом при оптимизации структур СОБИ РАИС является построение иерархического дерева критериев. При обосновании структуры подсистем СОБИ в качестве критериев (целевых функций) используются только наиболее значимые критерии эффективности обеспечения безопасности информации. При обосновании состава элементов подсистем СОБИ обязательным условием является использование полного множества обоснованных критериев эффективности СОБИ.

На втором этапе осуществляется спецификация рациональной структуры СОБИ в виде СМС СОБИ РАИС.

Глава 4. Комплекс методов и методик верификации СОБИ распределенной АИС. При верификации СОБИ РАИС особое значение имеет исследование и анализ структурных и динамических характеристик СМС СОБИ. Обобщенная методика верификации СМС СОБИ РАИС (рис. 4) предполагает для каждой ВАСП, входящей в СМС, решение следующих задач. безопасность информация верификация мультикаскадный

Задача 1. Задача достижимости маркировки. Достижима ли заданная маркировка ВАСП из ее начальной маркировки. Решение данной задачи заключается в построении множества достижимых маркировок.

Рис. 4. Схема обобщенной методики верификации СМС СОБИ РАИС

Задача 2. Задача определения принадлежности ограничений на маркировку позиций и множества маркировки дуг ВАСП к множеству кодексов.

Задача 3. Задача ограниченности позиций (сети в целом). Задача связана с проверкой выполнения ограничений на маркировку позиций и условий теоремы 1.

Задача 4. Задача устойчивости, активности и блокирования переходов.

Разработаны алгоритмы построения множеств достижимых маркировок ВАСП на основе методов исчерпывающего поиска в ширину и исчерпывающего поиска в глубину. В рамках данных алгоритмов под маркировкой ВАСП будем понимать кортеж: = <, Q, H, M>, где - время функционирования, Q - вектор активных переходов, H - вектор времени активизации переходов; M -маркировка позиций.

Особенность метода исчерпывающего поиска в ширину заключается в том, что достижимые маркировки просматриваются последовательно в порядке их формирования с целью определения для каждой анализируемой маркировки множества непосредственно достижимых из нее маркировок без возвращения к анализу уже просмотренных.

Через R(₀,k) обозначим множество достижимых маркировок ВАСП, полученное на k-й итерации алгоритма. Пусть R₁(₀,k) и R₂(₀,k) подмножества маркировок, просмотренных и не просмотренных на предыдущих итерациях. По определению R₁(₀,k)R₂(₀,k)=R(₀,k) и R₁(₀,k)R₂(₀,k)={}. Данные множества наделяются отношением порядка, которое определяется порядком формирования непосредственно достижимых маркировок. Каждая итерация алгоритма состоит в просмотре одной из еще не просмотренной маркировки _a R₂(₀, k) с наименьшим порядковым номером. Для маркировки _a на основе условия возбуждения перехода (1) строится множество возбужденных переходов T(_a):

(4)

Просмотр маркировки _a на k-й итерации заключается в ее преобразовании в маркировку _a (образ маркировки после завершения выполнения активизированных переходов) с учетом сформированного в соответствии с (2) вектора U_k завершения выполнения переходов:

 (5)

Компоненты маркировки _a вычисляются по следующим уравнениям:

_a = _a + 1

Q_a = Q_a - U_k

H_a = H_a - (_aU_k - D) U_k

(6)

Для полученной маркировки _a формируется на основе (4) и (1) множество возбужденных переходов. Для каждого из не просмотренных переходов t_a T₂(_a) формируется непосредственно достижимая маркировка _s:

(7)

Компоненты маркировки _s вычисляются по следующим уравнениям:

t_j T: U_k[t_j] = 0

U_k[t_a] = 1

_s = _a

Q_s = Q_a + U_k

H_s = H_a + _aU_k

(8)

Далее выполняется анализ полученной маркировки с целью включения ее в подмножества R₂(₀,k) или R₁(₀,k). При этом, если _sR₁(₀,k), то просматривать ее на последующих итерациях нет необходимости. В противном случае полученная маркировка _s, включается в подмножество R₂(₀,k) для следующей итерации: R₂(₀,k+1)=R₂(₀,k+1){_s}. Итерация заканчивается после анализа последней из непосредственно достижимых маркировок для _a. Алгоритм заканчивает работу, когда R₂(₀,q)={} для некоторой q-итерации. Алгоритм построения множества достижимых маркировок методом исчерпывающего поиска в ширину представляет собой следующую последовательность шагов.

0. Инициализация: R₁(₀,0)=R₂(₀,1)={}; R₂(₀,0)={₀}; =k=0.

1. Для очередной по порядку маркировки _aR₂(₀,k) сформировать управляющий вектор U_k на основе(2) и маркировку _a на основе (5) и (6).

2. Для полученной маркировки _a сформировать множество возбужденных переходов T(_a) на основе (1) и (4). Положить T₁(_a)={}, T₂(_a)=T(_a).

3. Если T₂(_a)={}, то переход на шаг 7.

4. Для очередного по порядку перехода t_aT₂(_a) сформировать непосредственно достижимую маркировку _s на основе (7) и (8). Положить T₁(_a)=T₁(_a){t_a} и T₂(_a)=T₂(_a) \ {t_a}.

5. Если полученная маркировка _sR₁(₀,k), то переход на шаг 3.

6. Положить R₂(₀,k+1) = R₂(₀,k+1) {_s}, причем маркировка _s получает очередной по счету номер. Переход на шаг 3.

7. Положить R₁(₀,k) = R₁(₀,k) {_a} и R₂(₀, k) = R₂(₀, k) \ {_a}.

8. Если R₂(₀, k) {}, то переход на шаг 1.

9. Если R₂(₀,k+1){}, то положить R₁(₀,k+1)=R₁(₀,k) и k=k+1 и переход на шаг 1.

10. Положить R(₀)=R₁(₀,k) и закончить выполнение алгоритма.

Идея метода исчерпывающего поиска в глубину состоит в том, что достижимые маркировки просматриваются в двух направлениях: прямом и обратном. Просмотр маркировки в прямом направлении осуществляется с целью формирования только одной непосредственно достижимой из нее маркировки, после чего осуществляется переход к просмотру этой сформированной маркировки. Просмотр маркировки в обратном направлении заключается в анализе множества непосредственно достижимых маркировок и возвращении к просмотру непосредственно предшествующей маркировки в случае просмотра в прямом направлении всех маркировок указанного множества. Алгоритм, реализующий метод, заканчивает работу, когда завершен поиск в прямом направлении всех маркировок, непосредственно достижимых из начальной маркировки.

Множества T(_a), T₁(_a), T₂(_a) обозначают множества возбужденных, просмотренных и не просмотренных переходов для маркировки _a. Множества упорядочены естественным отношением порядка, индуцируемым отношением порядка исходного множества переходов ВАСП и для них выполняются условия: T₁(_a)T₂(_a)=T(_a) и T₁(_a)T₂(_a)={}. Здесь _a - достижимая маркировка, которая подлежит просмотру в прямом направлении на текущем шаге алгоритма. Алгоритм построения множества достижимых маркировок для ВАСП методом исчерпывающего поиска в глубину представляет собой выполнение следующих шагов.

0. Инициализация алгоритма: R₁(₀)={}; R₂(₀)={₀}; _a=₀; =k=0.

1. Для маркировки _aR₂(₀,k) сформировать на основе (2) управляющий вектор U_k и получить маркировку _a на основе (5) и (6).

2. Для полученной маркировки _a сформировать множество возбужденных переходов T(_a) на основе (1) и (4). Положить T₁(_a)={}, T₂(_a)=T(_a).

3. Если T₂(_a)={}, то перейти на шаг 7.

4. Для очередного по порядку t_aT₂(_a) сформировать непосредственно достижимую маркировку _s на основе (7) и (8). Положить T₁(_a)=T₁(_a){t_a} и T₂(_a)=T₂(_a)\{t_a}.

5. Если маркировка _sR₁(₀)R₂(₀), то переход на шаг 3.

6. Положить R₂(₀)=R₂(₀){_s}; м_a=м_s; k=k+1. Запомнить предыдущие значения T₁(_a) и T₂(_a) переход на шаг 1.

7. Положить R₁(₀)=R₁(₀){_a} и R₂(₀)=R₂(₀)\{_s}.

8. Если k0, то положить k=k-1 и определить маркировку м_д, из которой достигается маркировка м_a. Положить м_a=м_д и перейти на шаг 3.

9. Положить R(₀)=R₁(₀) и закончить выполнение алгоритма.

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

Для доказательства отсутствия преднамеренных и (или) непреднамеренных программных дефектов предложен метод верификации расчетных программ на основе ST-пары функций. В качестве расчетной программы рассматривается любая программа, решающая задачу получения значения некоторой вычислимой функции. Метод верификации расчетных программ использует идею самотестирующихся программ, не требует вычисления эталонных значений и является независимым от используемого при написании программы языка программирования, что существенно повышает оперативность исследования программы и точность оценки вероятности отсутствия в ней программных дефектов. Необходимо отметить, что предлагаемый метод можно использовать для программ, вычисляющих функции особого вида, а именно функции, обладающие свойством случайной самосводимости.

Пусть Р - программа, которая предположительно вычисляет функцию Y= f(X), I - объединение подмножеств I_n (n принадлежит множеству натуральных чисел N), D^P={D_n | n N} - множество распределений вероятностей D_n над I_n, err (P, f, D_n) - вероятность того, что Р(x)f(x), где х выбрано случайно в соответствии с распределением D_n из подмножества I_n, - есть некоторый параметр безопасности. Тогда (₁,₂)-самотестирующейся программой для функции f в отношении D^P с параметрами 0<₁<₂<1 называется вероятностная оракульная программа T_f, которая для параметра безопасности и любой программы P на входе n имеет следующие свойства:

- если err (Р, f, D_n) е₁, тогда программа выдаст на выходе ответ «норма» с вероятностью не менее 1 - ;

- если err (P, f, D_n) е₂, тогда программа выдаст на выходе «сбой» с вероятностью не менее 1 - .

Пусть xI_n и с>1 -целое число. Свойство случайной самосводимости заключается в том, что f(x) может быть выражена через легко вычислимую функцию F от х, а₁,...,а_c, и f(a₁),...,f(а_c), где а₁,...,а_c являются легко вычислимыми по данному x и каждое a_i является случайно распределенным над I_n в соответствии с D^P. Пусть для функции Y=f(Х) существует пара функций (g_c,h_c) таких, что Y=g_c(f(a₁),…,f(a_c)) и Х=h_c(a₁,…,a_c). Пара функций (g_c,h_c)^Y обеспечивает выполнение для функции Y=f(Х) свойства случайной самосводимости и называется ST-парой функций для функции Y=f(Х). В этом случае, пусть длина кода программ, реализующих функции g_c и h_c и время их выполнения составляет константный мультипликативный фактор от длины кода и времени выполнения программы Р.

Метод верификации расчетной программы Р на основе ST-пары функций для некоторого входного значения вектора X^* заключается в выполнении следующего алгоритма.

1. Определить множество такое, что , где выбраны случайно из входного подмножества I_n.

2. Вызвать программу Р для вычисления значения и для вычисления множества значений .

3. Определить значения .

4. Если то программа Р корректна на множестве значений входных параметров , в противном случае - некорректна.

Относительный выигрыш по оперативности предложенного метода верификации (по отношению к методу тестирования программ на основе ее эталонных значений) определяется следующим образом:

.

Так как, коэффициент K_gh < 1, а с 2, то получаем относительный выигрыш по оперативности испытания расчетных программ указанного типа (обладающих свойством случайной самосводимости) более чем в 1.5 раза.

В качестве примера работоспособности предложенного метода рассмотрена верификация программы вычисления функции дискретного возведения в степень y = f_AM (x) = A^x modulo М. Для экспериментальных исследований была выбрана программа ЕХР из библиотеки базовых криптографических функций CRYPTOOLS, за реализацию которой автором в составе группы разработчиков получено авторское свидетельство.

Глава 5. Методы верификации при управлении процессами обеспечения безопасности информации. Управление процессами обеспечения безопасности информации в РАИС представляет собой целенаправленное воздействие на элементы СОБИ с целью достижения требуемых показателей защищенности информации при наличии внешних и внутренних дестабилизирующих факторов. Рассмотрены функции (управляющая, информационная и вспомогательная) и задачи (оперативные и нормативные) управления. Анализ функций и задач управления позволил разработать соответствующую модель управления.

Модель адаптивного управления процессами обеспечения безопасности информации является основой организации процесса управления элементами СОБИ РАИС. Функционирование СОБИ РАИС происходит в среде, описываемой кортежем: Q(t)=<Y(t),H(t)>, где Y(t) - управляемые характеристики среды (потоки данных, полномочия абонентов, параметры криптографических протоколов и т.д.); H(t) - неуправляемые характеристики среды (отказы элементов СОБИ, попытки НСД и т.д.). Состояние СОБИ X(t) в процессе функционирования зависит от состояния среды Q(t) а также от реализации управления U(t): U(t)=<U_н(t),U_о(t)>, где U_н(t) и U_о(t)- нормативное и оперативное управление элементами СОБИ.

Декомпозиция факторов управления на оперативные и нормативные позволяет более эффективно решать задачи управления элементами СОБИ в условиях неопределенности места и времени попыток НСД, а также в РАИС с переменной структурой, для которых нормативное управление процессами обеспечения безопасности информации малоэффективно.

Пусть R=R^t{X(t)} - критерий эффективности обеспечения безопасности информации, определенный на контролируемых состояниях РАИС и ее СОБИ. Индекс t обозначает то, что в процессе функционирования возможно изменение целей управления, а, следовательно, и критерия эффективности.

Математическая формулировка цели управления в этом случае заключается в решении задачи: , где - упреждение прогноза состояния безопасности информации; U^* - стратегия управления с учетом упреждения прогноза; R^t - критерий эффективности в момент времени t с учетом упреждения прогноза; S - прогнозируемое состояние с учетом упреждения прогноза; - ограничения на выбор стратегии управления. В качестве эталонной модели СОБИ используется СМС СОБИ.

В условиях неопределенности ряда характеристик распределенной обработки информации в модели используются элементы программного управления (планирования нормативного _н и оперативного управления _о).

В общем случае в n+1-й момент времени управление определяется как U_n+1=W(U_n,_n,,_n), где W - оператор рекуррентного управления, а U_n, _n, , _n - значения соответствующих параметров в n-й момент времени. Сущность модели заключается в иерархическом представлении функций управления (рис. 5) с элементами адаптации к условиям применения: W=W<W_по,W_пн,W_о,W_н>, где W_по и W_пн - подоператоры планирования оперативного и нормативного управления элементами СОБИ: _о=W_по(X,S) и _н=W_пн(X,S,U_о); W_о и W_н - подоператоры оперативного и нормативного управления СОБИ: U_о=W_о(X,S,_о) и U_н=W_н(X,S,_н).

Задача определения периодичности функционального контроля СОБИ РАИС решается на основе статистики и характеристик обеспечения безопасности информации, к которым относятся периодичность попыток НСД и отказов элементов, стоимость зондирования, направления и объемы потоков информации, а также характеристик надежности элементов СОБИ.

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

Необходимость решения данной задачи обусловлена целесообразностью организации контроля периодически через интервалы времени _k с целью минимизации суммарной стоимости функционирования и управления СОБИ. Пусть Т - время функционирования РАИС, C(s) - стоимость функционального контроля, (t) - состояние в момент времени t, (s) - потенциальный ущерб (стоимость) пребывания РАИС в конкретном состоянии (для безопасных состояний, примем равным 0), Тогда ожидаемая стоимость функционирования СОБИ на интервале [0, T] (с учетом только ущерба из-за неоперативности обнаружения нарушения безопасности и стоимости функционального контроля):

,

где и .

Заметим, что S_b подмножество состояний системы, при которых выполняются требования по обеспечению безопасности информации. Таким образом, задача состоит в определении n, t₁,…t_n, при которых функция принимает минимальное значение. Зависимость функций C_k-1(t_k-1,t_k) и r_k-1(t_k-1,t_k) от времени предыдущего контроля означает, что, в общем случае, после очередного контроля или восстановления безопасного состояния информации, РАИС может функционировать с новыми вероятностными характеристиками. Если данные функции зависят только от временного интервала между осуществлением функционального контроля, то считается, что данные функции описывают однородную РАИС, то есть r_k-1(t_k-1,t_k)=r_k-1(?_k) и C_k-1(t_k-1,t_k)=C_k-1(?_k). Тогда функции потерь приобретает следующий вид:

Зафиксировав число проверок на интервале [0, T], найдем оптимальные значения интервалов между итерациями функционального контроля СОБИ из условия минимума функции потерь. Продифференцировав функции C_k-1 (t), получим следующую систему уравнений:



Определив оптимальные значения {_k} и подставив их в функцию потерь, получим функцию , зависящую только от n и Т. Оптимальные значения n определяются из условия минимума полученной функции.

Показано, что для оценки эффективности СОБИ РАИС необходимо использовать счетное множество показателей: R = {R_i|i[1,n]}. Процесс формирования дерева показателей эффективности СОБИ сводится к следующему:

...