Метод верификации и анализа защищенности баз данных на основе формализации требований целостности

• Автор: Глухарев, Михаил Леонидович
• Шифр специальности: 05.13.19
• Научная степень: Кандидатская
• Год защиты: 2011
• Место защиты: Санкт-Петербург
• Количество страниц: 132 с. : ил.

ВВЕДЕНИЕ
1 АНАЛИЗ СОВРЕМЕННЫХ МЕТОДОВ И СРЕДСТВ ВЕРИФИКАЦИИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ И БАЗ ДАННЫХ

1.1 Архитектура современных реляционных баз данных.

1.2 Формирование концепции целостности реляционных баз данных

1.2.1 Понятие целостности реляционных баз данных.

1.2.2 Определение места целостности в системе характеристик качества баз данных

1.2.3 Анализ механизмов реализации требований целостности в реляционных базах данных

1.3 Общая характеристика методов и инструментов верификации программного обеспечения и баз данных.

1.3.1 Понятие, цели и задачи верификации.

1.3.2 Классификация методов верификации программного обеспечения

1.3.3 Современные методы и инструменты верификации реляционных баз данных

1.4 Анализ эффективности динамического тестирования целостности реляционных баз данных
1.5 Постановка задач исследования
2 РАЗРАБОТКА МЕТАМОДЕЛИ ТРЕБОВАНИЙ И ФУНКЦИЙ ЦЕЛОСТНОСТИ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ.
2.1 Целостность как корректность состояний и переходов.
2.2 Разработка метамодели требований целостности на основе совершенствования метамодели ГарсиаМолина, Ульмана и Уидом.
2.3 Применение формальных описателей в качестве спецификаций объектов
ограничений.
2.3.1 Типовые требования целостности и их формальные описатели.
2.3.2 Использование формальных описателей в качестве спецификаций
триггеров и триггерных связок.
2.4 Выводы
3 РАЗРАБОТКА МЕТОДА ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ И ВЫЯВЛЕНИЯ НЕДЕКЛАРИРОВАННЫХ ВОЗМОЖНОСТЕЙ ОБЪЕКТОВОГРАНИЧЕНИЙ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ.
3.1 Анализ методов логикоалгебраической верификации программных процедур
3.1.1 Связь между формальным описателем требования целостности и тройкой Хоара.
3.1.2 Взаимосвязь функциональной корректности программы с выбором наиболее сильного постусловия.
3.1.3 Анализ возможности применения метода индуктивных утверждений для верификации триггеров.
3.1.4 Требования к разрабатываемому методу формальной верификации
объектовограничений
3.2 Разработка процедур и алгоритмов, используемых в рамках метода формальной верификации объектовограничений.
3.2.1 Этапы проведения верификации
3.2.2 Восстановление описателей по ограничениям целостности.
3.2.3 Восстановление описателей по триггерам
3.2.4 Получение собственных постусловий простых операторов
3.2.5 Усиление собственного постусловия простого оператора
3.2.6 Правило последовательного усиления постусловий операторов маршрута
3.2.7 Получение постусловия маршрута, содержащего оператор отката транзакции
3.2.8 Алгоритм синтеза постусловия маршрута.
3.2.9 Синтез постусловия триггера.
3.2. Восстановление описателей по триггерным связкам
3.2. Сравнение описателей.
3.3 Выводы
4 РАЗРАБОТКА РЕКОМЕНДАЦИЙ ПО ПРАКТИЧЕСКОМУ ПРИМЕНЕНИЮ МЕТОДА ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ОБЪЕКТОВОГРАНИЧЕНИЙ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ
4.1 Границы применимости разработанного метода формальной верификации объектовограничений.
4.2 Основные принципы построения и функционирования программной системы проведения верификации объектовограничений
4.2.1 Описание функций системы проведения верификации
4.2.2 Структура системы проведения верификации объектовограничений.
4.3 Описание программной реализации системы проведения верификации объектовограничений.
4.3.1 Описание реализации подсистемыкоординатора
4.3.2 Описание реализации подсистемы анализа Ькодов.
4.3.3 Описание реализации подсистемы анализа спецификаций
4.3.4 Описание реализации подсистемы восстановления описателей
4.3.5 Описание реализации подсистемы сравнения описателей
4.4 Оценка оперативности и полноты выявления недекларированных возможностей в объектахограничениях с использованием разработанного метода.
4.5 Выводы.
ЗАКЛЮЧЕНИЕ.
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ


Таким образом, задачи формализации требований и функций целостности реляционных БД, а также повышения оперативности и полноты выявления НДВ в БД являются актуальными в области верификации БД. Объектом диссертационного исследования являются реляционные БД на стадиях разработки и тестирования. Предметом диссертационного исследования является формальная верификация и выявление НДВ ОЦ и триггеров реляционных БД. Цель исследования повышение оперативности и полноты выявления НДВ в ОЦ и триггерах реляционных БД. Научная задача исследования состоит в обосновании и разработке научнометодического аппарата формализации требований и функций целостности реляционных БД и выявления НДВ в ОЦ и триггерах на основе формальных моделей требований целостности. БД. Для решения поставленных задач применялись такие методы, как системный анализ, теория верификации программного обеспечения, логика Хоара, формальная логика. Теоретическую и методологическую базу исследования составляют труды отечественных и зарубежных ученых в области верификации различных компонентов АИС, стандарты в области информационных технологий и информационной безопасности. БД. БД, использующий новые алгоритмы синтеза постусловия маршрута в теле триггера и постусловия триггера, процедуры восстановления описателей по ОЦ, триггерам и триггерным связкам, процедуру сравнения описателей и позволяющий получать формальные модели НДВ, непосредственно влияющих на содержимое БД. Достоверность полученных научных результатов определяется корректным применением методов исследования, доказанностью ряда утверждений, лежащих в основе метамодели требований и функций целостности и метода верификации ОЦ и триггеров, апробацией результатов диссертационных исследований на научнопрактических конференциях и их внедрением в организациях. Практическая значимость результатов исследования состоит в возможности повышения оперативности и полноты выявления НДВ в ОЦ и триггерах реляционных БД, а также уменьшения объема и сложности последующих динамических испытаний за счет использования разработанного метода и программной системы проведения формальной верификации. Практическая ценность и новизна работы подтверждаются двумя актами внедрения от СПбФ ОАО НИИАС результаты использованы в рамках комплексного научнотехнического проекта Внедрение системы вертикальных динамических нагрузок Аш1а и от кафедры Информатика и информационная безопасность ФГБОУ ВПО ПГУПС результаты применены в учебном процессе и научноисследовательских работах. России СанктПетербург, СПИИРАН, г. Методы и технические средства обеспечения информационной безопасности СанктПетербург, СПбГПУ, г. Инфотранс, СанктПетербург, ПГУПС, первой международной научнопрактической конференции Интеллектуальные системы на транспорте СанктПетербург, ПГУПС, . По результатам исследования опубликовано 9 статей, 3 из которых в журналах, рекомендуемых ВАК, 5 в материалах общероссийских, межрегиональных и международных конференций. Диссертация включает введение, четыре главы, заключение, список использованных источников. В первой главе рассматривается объект исследования реляционные БД. Приводится модель логической архитектуры современных реляционных БД. Раскрывается значимость свойства целостности для БД, проводится анализ методов и механизмов реализации требований целостности, предъявляемых к БД заказчиками. Также в этой главе проводится анализ методов верификации программного обеспечения, методов и инструментов тестирования целостности БД. Обосновывается необходимость разработки метамодели, описывающей принципы моделирования требований целостности, и нового метода формальной верификации для повышения качества выявления НДВ в ОЦ и триггерах БД. Вторая глава посвящена разработке метамодели, задающей принципы моделирования требований целостности двух классов требования к состоянию и требования к переходу. Вводится понятие формального описателя требования целостности и задается его структура. Также в рамках метамодели определяются специфические действия над формальными описателями, которые используются при проведении формальной верификации ОЦ и триггеров БД.