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

Значительная часть современных автоматизированных информационных систем (АИС) основана на использовании реляционных баз данных (БД). Качество БД оказывает значительное влияние на качество АИС в целом.

Одной из важнейших характеристик качества БД является информационная безопасность, которая, в свою очередь, включает в себя целостность информации. В теории реляционных БД целостность понимается как логическая согласованность и семантическая корректность данных. До начала разработки БД заказчик формулирует требования целостности, значимые в данной предметной области. Задача разработчика БД состоит в том, чтобы обеспечить программную реализацию этих требований в виде специальных программных объектов БД — ограничений целостности (ОЦ) и триггеров. Поддержка целостности в БД выполняется на требуемом уровне, если обеспечены:

• пригодность ОЦ и триггеров, т. е. ОЦ и триггеры реализуют все специфицированные требования целостности;

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

ВДВ).

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

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

Вопросам общей теории верификации компонентов АИС, особенно программного обеспечения, посвящены работы ряда отечественных и зарубежных специалистов: В. В. Липаева, В. В. Кулямина, А. А. Корниенко, М. А. Еремеева, М. М. Безкоровайного, Б. Боэма, Г. Майерса и др. Конкретные методы верификации описаны в работах Н. А. Абрамовой, A.B. Аграновского, В. А. Непомнящего, В. Е. Котова, Ч. Хоара, Р. Флойда, Э. Дейкстры, Р. Андерсона, Э. Кларка и др. авторов. Вопросы верификации БД, в том числе верификации целостности, рассматривают в своих работах П. Тонграк, Т. Саваннасарт, С. А. Халек, К. Бинниг, Н. Бруно, X. Кеннет, Р. Дж. Жанг, X. Ибрагим, М. Наката, А. Альвэн и др. авторы. Верификация целостности БД, в основном с использованием тестовых сценариев, проводится с использованием специализированного программного обеспечения, разрабатываемого компаниями Computer Associates, Rational Software, Logic Wokrs, Quest Software, Oracle, IBM и др.

Существующие методы верификации целостности реляционных БД обладают следующими недостатками:

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

• разработка тестовых сценариев для выявления НДВ в БД требует значительных затрат человеческого труда и отрицательно сказывается на оперативности выявления НДВ;

• отсутствует способ формального описания свойств имеющихся НДВ в ОЦ и триггерах;

• на практике имеет место неполнота выявления НДВ в ОЦ и триггерах, особенно это касается умышленных НДВ (программных закладок), что отчасти связано с отсутствием формального описания НДВ.

Таким образом, задачи формализации требований и функций целостности реляционных БД, а также повышения оперативности и полноты выявления НДВ в БД являются актуальными в области верификации БД.

Объектом диссертационного исследования являются реляционные БД на стадиях разработки и тестирования.

Предметом диссертационного исследования является формальная верификация и выявление НДВ ОЦ и триггеров реляционных БД.

Цель исследования — повышение оперативности и полноты выявления НДВ в ОЦ и триггерах реляционных БД.

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

Достижение поставленной цели и решение научной задачи требует решения следующих частных задач:

• анализ существующих методов и средств верификации программного обеспечения и реляционных БД;

• разработка метамодели требований и функций целостности реляционных БД;

• разработка метода формальной верификации и анализа защищенности реляционных БД;

• разработка практических рекомендаций по применению и программной реализации метода формальной верификации и анализа защищенности реляционных БД.

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

На защиту выносятся следующие научные результаты:

• метамодель требований и функций целостности, описывающая принципы моделирования требований целостности различных классов и пригодная к использованию при проведении формальной верификации ОЦ и триггеров реляционных БД;

• метод формальной верификации и анализа защищенности реляционных БД, основанный на метамодели требований и функций целостности и использующий семантический анализ программных кодов ОЦ и триггеров;

• принципы построения и функционирования программной системы проведения верификации и анализа защищенности реляционных БД.

Научная новизна диссертационной работы состоит в следующем:

• разработана метамодель, включающая структуру формальных описателей требований целостности и используемые при проведении формальной верификации ОЦ и триггеров реляционных БД действия над описателями;

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

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

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

Практическая ценность и новизна работы подтверждаются двумя актами внедрения: от СПбФ ОАО «НИИАС» (результаты использованы в рамках комплексного научно-технического проекта «Внедрение системы вертикальных динамических нагрузок Aguila») и от кафедры «Информатика и информационная безопасность» ФГБОУ ВПО ПГУПС (результаты применены в учебном процессе и научно-исследовательских работах).

Основные результаты исследований излагались и обсуждались на научных семинарах кафедры «Информатика и информационная безопасность» ПГУПС, кафедры «Информационная безопасность» ПГУПС при Санкт-Петербургском институте информатики и автоматизации РАН, а также на четвертой Санкт-Петербургской межрегиональной конференции «Информационная безопасность регионов России» (Санкт-Петербург, СПИИРАН, 2005 г.), четырнадцатой общероссийской научно-технической конференции «Методы и технические средства обеспечения информационной безопасности» (Санкт-Петербург, СПбГПУ, 2007 г.), международной научно-практической конференции «Инфотранс-2005, 2009» (Санкт-Петербург, ПГУПС), первой международной научно-практической конференции «Интеллектуальные системы на транспорте» (Санкт-Петербург, ПГУПС, 2011).

По результатам исследования опубликовано 9 статей, 3 из которых — в журналах, рекомендуемых ВАК, 5 — в материалах общероссийских, межрегиональных и международных конференций.

Диссертация включает введение, четыре главы, заключение, список использованных источников.

4.5 Выводы.

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

1. Разработана концептуальная модель СПВ, согласно которой основными функциями СПВ являются: обработка файлов спецификаций, извлечение БСД,-кодов объектов-ограничений из файлов скриптов, извлечение объектов-ограничений из системного каталога СУБД или системных таблиц БД, выбор объектов-ограничений для анализа и собственно проведение верификации объектов-ограничений. Вспомогательными функциями системы являются: лексический и синтаксический анализ 8С) Ь-кодов, редактирование словаря собственных постусловий, редактирование БД сравнения описателей.

2. Разработана структурная схема СПВ, согласно которой СПВ включает следующие подсистемы: координатор, подсистему анализа 8С) Ь-кодов, подсистему анализа спецификаций, подсистему восстановления описателей, подсистему сравнения описателей, словарь собственных постусловий и БД подсистемы сравнения описателей.

3. Выполнена программная реализация прототипа СПВ.

4. Выполнено оценивание оперативности выявления НДВ с помощью разработанного метода. Полученные результаты позволяют обоснованно утверждать о более высокой оперативности формальной верификации по сравнению с динамическим тестированием целостности.

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

ЗАКЛЮЧЕНИЕ

.

В результате проведенного исследования был разработан метод формальной верификации ОЦ и триггеров реляционных БД на основе метамодели требований целостности. Применение разработанного метода позволяет повысить оперативность и полноту выявления НДВ в ОЦ и триггерах.

При решении частных задач были получены следующие результаты.

1. Выполнен анализ объекта исследования и современных методов верификации ПО и БД. Установлено, что для выявления НДВ в ОЦ и триггерах в настоящее время используется динамическое тестирование, позволяющее выявлять в среднем 72,82% ошибок и 19,21% программных закладок, при этом средние затраты времени на тестирование одного требования целостности составляют 8 минут 32 секунды. Низкий процент выявления программных закладок имеет объективную причину: инженер по тестированию заранее не знает о наличии закладок и не может целенаправленно подготовить сценарии для их активизации. Также установлено, что недостатком динамического тестирования БД на современном этапе является отсутствие формального моделирования требований целостности и НДВ, что затрудняет идентификацию НДВ.

2. Разработана метамодель требований и функций целостности. Описаны основные математические характеристики требований целостности: множество таблиц и псевдотаблиц, столбцов и операций, активизирующих переход данных из одного состояния в другое. Введено понятие формального описателя требования целостности и задана его общая структура. С помощью формальных описателей можно моделировать требования целостности двух классов: требования к состоянию и требования к переходу. Доказано, что некоторые описатели обладают свойством соединимости, и в связи с этим определены специфические действия над формальными описателями: соединение и разбиение. Они используются при проведении формальной верификации ОЦ и триггеров. Введены понятия избыточности и безызбыточности требования целостности, критичности и некритичности активизирующих БМЬ-операций описателя. Показано, что описатели, будучи логико-алгебраическими моделями требований целостности, одновременно могут служить в качестве спецификаций ОЦ, триггеров и триггерных связок. Установлено, что реальные функции целостности БД, как и требования целостности, могут быть смоделированы с помощью формальных описателей. Достоверность результата подтверждается практикой использования механизмов поддержки целостности в реляционных БД.

3. Разработан метод формальной верификации и анализа защищенности реляционных БД на основе созданной метамодели требований и функций целостности. Метод использует семантический анализ программных кодов ОЦ и триггеров и включает оригинальные алгоритмы синтеза постусловия маршрута в теле триггера, синтеза постусловия триггера, восстановления описателей по ОЦ, триггерам и триггерным связкам и процедуру сравнения описателей. Метод позволяет выявлять нереализованные функции целостности и получать формальные описания НДВ в объектах-ограничениях при условии, что НДВ оказывают непосредственное влияние на содержимое БД.

У ' 1 ^ -А.

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

4. Даны рекомендации по практическому применению разработанного метода. Описаны принципы построения и функционирования СПВ, создан прототип СПВ, благодаря чему метод формальной верификации может использоваться в автоматизированном режиме.

5. Проведено исследование оперативности и полноты выявления НДВ при формальной верификации и динамическом тестировании. Установлено, что затраты времени на динамическое тестирование в среднем в 2,18 раз превышают время, требуемое для формальной верификации. Среднее время проверки одного требования целостности при динамическом тестировании составляет 8 минут 32 секундыпри формальной верификации — 3 минуты 52 секунды. Полнота обнаружения ошибок и программных закладок при формальной верификации достигает 100%, в среднем обнаруживается 94,44% ошибок и 94,73% программных закладок.

Таким образом, в ходе проведенного исследования были решены частные задачи и главная научная задача исследования и достигнута цель, состоящая в повышении оперативности и полноты выявления НДВ в ОЦ и триггерах реляционных БД.