автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.19, диссертация на тему:Метод верификации и анализа защищенности баз данных на основе формализации требований целостности

На правах рукописи

005001268

ГЛУХАРЕВ МИХАИЛ ЛЕОНИДОВИЧ

МЕТОД ВЕРИФИКАЦИИ И АНАЛИЗА ЗАЩИЩЕННОСТИ БАЗ ДАННЫХ НА ОСНОВЕ ФОРМАЛИЗАЦИИ ТРЕБОВАНИЙ ЦЕЛОСТНОСТИ

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

Автореферат

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

1 О НОЯ 2011

Санкт-Петербург 2011

д

005001268

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

Научный руководитель: Официальные оппоненты:

Ведущая организация:

доктор технических наук, профессор Корниенко Анатолий Адамович

доктор технических наук, профессор Молдовян Александр Андреевич

кандидат технических наук, доцент Зима Владимир Михайлович

Санкт-Петербургский филиал ФГУП «ЗащитаИнфоТранс»

Защита диссертации состоится 17 ноября 2011 г. в 15 часов 00 минут на заседании диссертационного совета Д 218.008.06 при Петербургском государственном университете путей сообщения по адресу: 190031, Санкт-Петербург, Московский пр., д. 9 (ауд. 1-217).

С диссертацией можно ознакомиться в библиотеке Петербургского государственного университета путей сообщения.

Автореферат разослан ж 2011 г.

Ученый секретарь диссертационного совета кандидат технических наук, профессор ^ Кудряшов В.А.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы исследования

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

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

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

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

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

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

Вопросам общей теории верификации компонентов АИС, особенно программного обеспечения, посвящены работы ряда отечественных и зарубежных специалистов: В. В. Липаева, В. В. Кулямина,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Методы исследования: системный анализ, теория верификации программного обеспечения, логика Хоара, формальная логика.

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

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

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

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

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

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

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

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

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

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

Реализация результатов работы. Основные результаты диссертационных исследований внедрены в следующих организациях:

• Санкт-Петербургский филиал ОАО «Научно-исследовательский и проектно-конструкторский институт информатизации, автоматизации и связи на железнодорожном транспорте» (НИИАС) в рамках комплексного научно-технического проекта «Внедрение системы вертикальных динамических нагрузок Aguila»;

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

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

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

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

диссертации - 132 е., из которых основного текста - 127 с. Библиографический список содержит 88 наименований. Основной текст диссертации включает 18 рисунков и 6 таблиц.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

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

В работе экспериментально установлено, что динамическое тестирование позволяет определить все не реализованные в БД требования целостности, выявить в среднем 73 % случайных ошибок в объектах-ограничениях и 19 % программных закладок. Среднее время на тестирование одного требования целостности составило приблизительно 9 минут.

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

Вторая глава посвящена разработке метамодели, задающей принципы моделирования требований целостности двух классов:

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

В разработанной метамодели любое требование целостности характеризуется следующими множествами:

• Т- множество таблиц, связанных данным требованием;

• С - множество конкретных столбцов, связанных данным требованием.

Требование к состоянию характеризуется множеством Т, которое включает только основные («физические») таблицы БД t\, t„. Требование к переходу характеризуется множеством Т, которое, помимо

основных таблиц, может включать псевдотаблицы t'"s ntfel, соответствующие таблице (/е[1,и]) и содержащие информацию о

модифицированных строках таблицы t, до ( tfel ) или после ( t™ ) выполнения DML-операции, активизирующей переход данных из одного состояния в другое.

Множество С = {c,,...,cm} содержит столбцы таблиц и (или) псевдотаблиц, связанных требованием целостности.

Требование к переходу имеет дополнительную характеристику -множество DML-операций, активизирующих переход. Множество операций обозначается за Л и включает элементы вида:

• ins(t) - операция вставки строк в таблицу t;

• upd(t) - операция обновления строк таблицы t;

• délit) - операция удаления строк из таблицы t. Логико-алгебраическая модель требования целостности представляет

собой формальный описатель (далее - описатель) — выражение вида:

Q(tv...,tn,cv...cm)\A, (1)

если Г не содержит псевдотаблиц, или

a^...,tl,...,in,tr,tfel,cl,...cm)\A, (2)

если Г содержит псевдотаблицы. Условие Q связывает все элементы множеств Та С. Элементы множества А определяются в зависимости от содержания требования, но всегда справедливо следующее соотношение: А с {ms(i: ), upd(t{ ), délit, )} u... u {ins(t„ ), upd(tn ), délitn )}. (3)

Если множество Т включает псевдотаблицы, их может быть не более

Jns del

двух - и г,- , - соответствующих одной и только одной таблице При этом множество А удовлетворяет соотношению:

А с {ins(tj ), upd{ti ), déliti )}. (4>

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

Также в рамках созданной метамодели определены два специфических действия над описателями: соединение и разбиение.

В ходе разработки метамодели было доказано, что если существует q требований целостности с описателями Q\Ai,...,Q\Aqt то существует

требование целостности с описателем SI A ^ — который

называется соединением исходных q описателей. Соединение может трактоваться, как действие над описателями, т. е. получение описателя

вида на основе исходных описателей Q\ Ai, ...,Q\ А .

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

Также в главе 2 водится понятие критичности и некритичности DML-операций, с которыми связаны понятия избыточности и безызбыточности требования целостности.

Критичной для требования операцией (или просто критичной операцией) называется такая операция из множества А, по выполнении которой условие Q может оказаться ложным при отсутствии в БД контролирующего объекта-ограничения. Операция, не являющаяся критичной, называется некритичной операцией. Множество критичных операций требования обозначается за А'; А'с. А. Таблицы, обрабатываемые критичными операциями, являются элементами

множества I"; T'çi Т. На практике во многих случаях 7"совпадает с Т.

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

Требование целостности является безызбыточным, если все операции, входящие в множество А его описателя, являются критичными.

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

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

Любой описатель может специфицировать процедурную реализацию требования целостности. В ходе исследования было показано, что описатель может быть спецификацией триггера для связанной таблицы t, если и только если А с {ins(t), upd{t), del{t)}.

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

вида Q(t\, —,tn, с{, ...ст)| А, где Г не содержит псевдотаблиц, является спецификацией триггерной связки, минимальный размер которой равен |7"|. Вследствие совпадения множества Т' с Г на практике, минимальный размер триггерной связки во многих случаях может определяться, как ¡7].

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

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

Исходными данными для проведения формальной верификации ОЦ и триггеров являются:

• формальные описатели требований целостности;

• SQL-коды ОЦ и триггеров проверяемой БД.

Верификация проводится в два этапа.

Первый этап - восстановление описателей - представляет собой построение модели реализации ОЦ и триггеров. На этом этапе эксперт (инженер по тестированию) проводит семантический анализ SQL-кодов ОЦ и триггеров. Результатом этих действий является набор описателей реализованных функций целостности - восстановленных описателей.

Описатель, восстановленный по объекту-ограничению R, обозначается следующим образом: Desc{R). Описатель, восстановленный по связке триггеров 7УЬ ..., Trq (где q - размер связки), обозначается за Desc{Tr\, ...; Тгд). При прохождении первого этапа необходимо получить перечень описателей, восстановленных по всем проверяемым ОЦ, триггерам и триггерным связкам.

Восстановление описателей по кодам ОЦ не представляет трудности. Каждому типовому ОЦ, поддерживаемому реляционными СУБД, можно поставить в соответствие типовой описатель, руководствуясь информацией о разновидности ОЦ и о количестве связанных столбцов.

Процедура восстановления описателей по ОЦ сводится к следующей последовательности действий.

1. Информация обо всех ОЦ извлекается из системного каталога СУБД (системных таблиц БД) или файлов SQL-скриптов.

2. Тип каждого ОЦ определяется по ключевым словам PRIMARY KEY, FOREIGN KEY, UNIQUE, NOT NULL, CHECK.

3. По разновидности ОЦ определяется соответствующий типовой описатель, который и принимается в качестве описателя, восстановленного по ОЦ.

В результате каждому ОЦ БД ставится в соответствие один и только один восстановленный описатель.

Более сложным является семантический анализ триггера, т. к. триггер представляет собой программную процедуру.

В процессе семантического анализа триггера в его теле выделяются возможные маршруты выполнения М\, ...,Mi, после чего каждый маршрут анализируется в отдельности.

Текущий маршрут М представляется в виде последовательности F\, S\, ...; Fn, Sn, где ..., "Sjv-простые SQL-операторы, aFh ..., FN-условия передачи управления операторам S\, ..., S¡у соответственно. Под простыми операторами в данном случае понимаются DML-операторы, непосредственно влияющие на состояние данных в таблицах и (или) псевдотаблицах (INSERT, UPDATE, DELETE, ROLLBACK TRAN), a также пустой оператор. Оператор SELECT не изменяет состояния данных, но SQL-конструкции на его основе могут использоваться в условиях F\,...,Fff. Если передача управления оператору S/ производится безусловно, то F, принимается тождественно равным 1. Если 5,- - пустой

оператор, это означает передачу управления оператору Si+i по условию

Каждому оператору S, текущего маршрута ставится в соответствие собственное постусловие Qt - постусловие, определяемое непосредственно на основе семантики оператора 5,- при рассмотрении данного оператора изолированно от прочих операторов маршрута.

На основе ряда вспомогательных утверждений и правил разработан алгоритм синтеза постусловия QM маршрута М(рис. 1).

Алгоритм использует множество предикатов U, в которое последовательно включаются предусловие маршрута (блок 1), условия Ft (блок 4) и собственные постусловия операторов Qj (блок 12). До включения Qi в множество U выполняется инверсия тех текущих элементов этого множества, ложность которых следует из условия Q-, (блоки 8- 11).

Постусловие QM формулируется по окончании прохождения маршрута, в тот момент, когда множество U является окончательно сформированным. Если маршрут завершается оператором ROLLBACK TRAN,

то Qm определяется, как отрицание конъюнкции всех элементов множества U; в остальных случаях - как конъюнкция элементов без отрицания.

После синтеза постусловий всех маршрутов выполняется синтез постусловия триггера. В диссертационном исследовании показано, что дизъюнкция постусловий маршрутов является постусловием триггера:

Qtv=Qm, v...vQMi. (8)

Множество DML-операций АТг описателя, восстановленного по триггеру Тг, формируется на основе перечня активизирующих операторов, указанного при создании или замене триггера.

Результатом восстановления описателей по триггерам является множество описателей реализуемых ими функций целостности БД. Если в этом множестве существует группа описателей с эквивалентными условиями Q, то существует соединение этих описателей, являющееся формальной моделью более общей функции целостности; с другой стороны, это говорит о наличии в БД триггерной связки. Если триггеры Тг\, ...; Тгд образуют триггерную связку, то соединение восстановленных по ним описателей допустимо считать описателем, восстановленным по триггерной связке.

Процедура восстановления описателей по триггерным связкам

выполняется в следующем порядке.

1. Восстанавливаются описатели по триггерам целевой БД.

2. В полученной модели реализации функций целостности выделяются группы описателей, имеющих эквивалентные условия Q.

3. Соединяются описатели с эквивалентными условиями ().

Соединения описателей заменяют группы описателей по триггерам,

на основе которых они получены. На этом процесс восстановления описателей завершается, и его результатом является перечень описателей, восстановленных по ОЦ, триггерам и триггерным связкам.

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

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

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

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

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

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

Функциями программной системы являются обработка файлов спецификаций, содержащих описатели исходных требований целостности, извлечение 5С)Ь-кодов объектов-ограничений из файлов скриптов, получение информации об объектах-ограничениях из системного каталога СУБД или системных таблиц БД и собственно проведение верификации объектов-ограничений.

Кроме того, в процессе анализа спецификаций, скриптов и проведения верификации система выполняет некоторые вспомогательные функции, а именно: лексический и синтаксический анализ 8С>Ь-кодов, редактирование словаря собственных постусловий и редактирование БД подсистемы сравнения описателей.

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

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

Таблица 1 - Данные о количестве таблиц БД, требований целостности и объектов-ограничений в каждом испытании_

Номер испытания Количество таблиц Количество требований целостности Количество объектов-ограничений

1 24 48 42

2 30 64 62

3 47 89 89

4 52 96 96

5 52 104 104

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

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

динамическое тестирование в среднем в 2,18 раз превышают время, требуемое для формальной верификации. Среднее время проверки одного требования целостности при динамическом тестировании составляет 8 минут 32 секунды; при формальной верификации - 3 минуты 52 секунды.

Динамическое тсстироввание

-Формальна« верификация

1 2 3 А 5 Номер испытания

Рисунок 2 - Сравнение временных затрат на динамическое тестирование и формальную верификацию объектов-ограничений

Сравнение динамического тестирования и формальной верификации в части обнаружения случайных ошибок в объектах-ограничениях показывает, что при формальной верификации полнота обнаружения приближается к 100 %, в среднем обнаруживается примерно 94,44 % ошибок. Процент обнаруженных ошибок при динамическом тестировании оказался не более 88,89, в среднем обнаруживается 72,82 % ошибок.

Сравнение динамического тестирования и формальной верификации в части обнаружения программных закладок показывает, что при формальной верификации полнота обнаружения также приближается к 100 %, в среднем обнаруживается примерно 94,73 % закладок. Эти показатели значительно выше, чем при динамическом тестировании (максимум 35,71 % при проведении испытаний, в среднем - 19,21 %).

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

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

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

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

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

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

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ РАБОТЫ

(публикации в изданиях, рекомендованных ВАК Минобрнауки России, выделены курсивом)

/. Глухарев М. Л. Применение формальных описателей для логико-алгебраического моделирования требований целостности информации в реляционных базах данных // Известия Петербургского университета путей сообщения. - СПб: ПГУПС, 2010. -Вып. 4 (25). - С. 78-88.

2. Глухарев М. Л. Метод формальной верификации ограничений целостности и триггеров реляционных баз данных // Известия Петербургского университета путей сообщения. - СПб: ПГУПС. 2011. - Вып. 2 (27). - С. 79-87.

3. Глухаревы. Л., Косаренко А. П., Хомоненко А. Д. Программа для автоматизированной верификации ограничений целостности баз данных // Программные продукты и системы. - Тверь, 2011. 1 (93). - С. 91-95.

4. Глухарев М. Л, Разработка показателей и методов оценивания корректности реляционных баз данных // Известия Петербургского университета путей сообщения. -Вып.1. - СПб.: ПГУПС , 2008. - С. 135-148.

5. Еремеев М. А., Глухарев М. Л., Корниенко А. А. Анализ методов проверки корректности программ // Информационные технологии на железнодорожном транспорте: Сборник докладов десятой международной научно-практической конференции «Инфотранс-2005». - СПб.: ПГУПС, 2005. - С. 276-280.

6. Корниенко А. А., Глухарев М. Л. Анализ методов верификации программных средств в защищенных информационных системах // Информационная безопасность регионов России: Тезисы докладов четвертой Санкт-Петербургской Межрегиональной конференции "ИБРР-2005". - СПб.: СПОИСУ, 2005.

7. Корниенко А. А., Глухарев М. Л. Понятие и виды корректности реляционных баз данных//Методы и технические средства обеспечения безопасности информации: Материалы XVI общероссийской научно-технической конференции. - СПб.: СПбГПУ, 2007.-С. 10-11.

8. Глухарев М. Л. Современные методы и программные средства тестирования и верификации реляционных баз данных И Инновации на железнодорожном транспорте -2009: Сборник докладов юбилейной научно-технической конференции. - СПб.: ПГУПС, 2009. - С. 68-73.

9. Корниенко А. А., Глухарев М. Л. Анализ современных инструментальных средств тестирования реляционных баз данных //Информационные технологии на железнодорожном транспорте: Аннотации докладов четырнадцатой международной научно-практической конференции «Инфотранс-2009», Санкт-Петербург, 2009. - СПб.: ПГУПС, 2009. - С. 79-82.

Подписано к печати 10.10.2011 Печ. л. 1,0

Печать - ризография Бумага для множит, апп. Формат 60x84 1/16

Тираж 100 экз. Заказ № Ш.

ПГУПС 190031, г. С-Петербург, Московский пр., 9

ОБОЗНАЧЕНИЯ И СОКРАЩЕНИЯ.

ВВЕДЕНИЕ.

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.10 Восстановление описателей по триггерным связкам.

3.2.11 Сравнение описателей.

3.3 Выводы.

4 РАЗРАБОТКА РЕКОМЕНДАЦИЙ ПО ПРАКТИЧЕСКОМУ ПРИМЕНЕНИЮ МЕТОДА ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ОБЪЕКТОВ-ОГРАНИЧЕНИЙ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ.

4.1 Границы применимости разработанного метода формальной верификации объектов-ограничений.

4.2 Основные принципы построения и функционирования программной системы проведения верификации объектов-ограничений.

4.2.1 Описание функций системы проведения верификации.

4.2.2 Структура системы проведения верификации объектов-ограничений.

4.3 Описание программной реализации системы проведения верификации объектов-ограничений.

4.3.1 Описание реализации подсистемы-координатора.

4.3.2 Описание реализации подсистемы анализа SQL-кодов.

4.3.3 Описание реализации подсистемы анализа спецификаций.

4.3.4 Описание реализации подсистемы восстановления описателей.

4.3.5 Описание реализации подсистемы сравнения описателей.

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

4.5 Выводы.

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

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

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

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

ВДВ).

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

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

Вопросам общей теории верификации компонентов АИС, особенно программного обеспечения, посвящены работы ряда отечественных и зарубежных специалистов: В. В. Липаева, В. В. Кулямина, А. А. Корниенко, М. А. Еремеева, М. М. Безкоровайного, Б. Боэма, Г. Майерса и др. Конкретные методы верификации описаны в работах Н. А. Абрамовой, 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 % программных закладок.

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

1. Липаев В.В. Обеспечение качества программных средств. Методы и стандарты. Серия «Информационные технологии». М.: СИНТЕГ, 2001. -380 с.

2. В.В. Липаев. Оценка качества программных средств // Сетевой журнал. http://www.setevoi.rU/cgi-bin/text.pl/magazines/2002/3/52. №3, 2002.

3. В.В. Липаев. Анализ качества баз данных // Открытые системы. http://www.osp.ru/os/2002/03/181272. №3, 2002.

4. Безкоровайный М.М., Костогрызов А.И., Львов В.М. Инструментально-моделирующий комплекс для оценки качества функционирования информационных систем «КОК». М.: «Синтег», 2000.

5. Боэм Б.У. Инженерное проектирование программного обеспечения: пер с англ. М.: Радио и связь, 1985.

6. Майерс Г. Надежность программного обеспечения. М.: Мир, 1980. -360с.

7. Майерс Г. Искусство тестирования программ. М.: Фин. И Статистика, 1982. - 178с.

8. Ю.Абрамова Н. А., Баталина Т. С., Гегамов Н. А., Коврига С. В. Новый математический аппарат для анализа внешнего поведения и верификации программ. М.: Институт проблем управления, 1998. 109 с.

9. П.Аграновский А., Зайцев В., Телеснин Б., Хади Р. Верификация программ с помощью моделей // Открытые системы №12, 2003.

10. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М. Радио и связь, 1988. 256 с.

11. В. Е. Котов. Сети Петри. М.: Наука, 1984. 158 с.

12. С. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10), October 1969, pp. 576 585.

13. Hoare C.A.R. Proof of correctness of data representation. Acta Informatica, 1, 1972.-pp. 271-287.

14. R. W. Floyd. Assigning meaning to programs. Proc. of Symposium in Applied Mathematics. J. T. Schwartz, ed. Mathematical Aspects of Computer Science, 19:19-32,1967.

15. Дейкстра Э. Дисциплина программирования. M.: Мир, 1978. 275 с.

16. Андерсон Р. Доказательство правильности программ. М.: Мир, 1982. -165 с. , ,

17. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: МЦНМО, 2002.

18. Tongrak P., Suwannasart Т. A Tool for Generating Test Case from Relational Database Constraints Testing / Computer Science and Information Technology (ICCSIT 2009). 2nd IEEE International Conference on Date: Aug. 8-11. Beijing, China, 2009, pp. 435^39.

19. Khalek S.A., Elkarablieh В., Laleye Y.O., Khurshid S. Query-Aware Test Generation Using a Relational Constraint Solver. Automated Software Engineering, 2008. 23rd IEEE/ACM International Conference. L'Aquila, 2008, pp. 238-247.

20. Binnig С., Kossmann D., Lo E., and Ozsu M.T. QAGen: Generating Query-Aware Test Databases. ETH Zurich Technical Report, 2007.

21. Binnig C., Kossmann D., and Lo E. Towards Automatic Test Database Generation. IEEE Data Eng. Bull. 31(1): 28-35, 2008.

22. Bruno N., and Chaudhuri S. Flexible database generators. In VLDB '05: Proceedings of the 31st international conference on Very large data bases. VLDB Endowment, 2005, pp. 1097-1107.

23. Kenneth H., Kristian Т., and Rico W. Simple and realistic data generation. In VLDB '06: Proceedings of the 32nd international conference on Very large data bases. VLDB Endowment, 2006, pp. 1243-1246.

24. Nakata, M.; Murai, T. Updating under integrity constraints in fuzzy databases. Fuzzy Systems, 1997., Proceedings of the Sixth IEEE International Conference on Volume 2, Date: 1-5 Jul 1997, pp. 713-719.

25. Alwan A.A., Ibrahim H., Udzir N.I. A Framework for Checking Integrity Constraints in a Distributed Database. 2008. ICCIT '08. Third International Conference on Convergence and Hybrid Information Technology. Vol. 1. Busan, Korea, Nov. 11-13, 2008.

26. ГОСТ P ИСО МЭК TO 10032-2007: Эталонная модель управления данными. -M.: Стандартинформ, 2009.

27. Когаловский М. Р. Энциклопедия технологий баз данных.— М.: Финансы и статистика, 2002. 798 с.

28. Хомоненко А.Д., Цыганков В.М., Мальцев М.Г. Базы данных: Учебник для высших учебных заведений / Под ред. проф. А.Д. Хомоненко. — СПб.: Корона принт, 2004. 736 с.

29. Дейт К. Дж. Введение в системы баз данных, 8-е издание: Пер. с англ. -М.: Издательский дом «Вильяме», 2008. 1328 с.

30. Коннолли Т., Бегг К. Базы данных. Проектирование, реализация и сопровождение. Теория и практика. — 3-е издание.: Пер. с англ. — М.: Издательский дом «Вильяме», 2003. 1439 с.

31. Гарсиа-Молина Г., Ульман Дж., Уидом Дж. Системы баз данных. Полный курс; пер. с англ. М.: Издательский дом «Вильяме», 2004. - 1088 с.

32. Пушников А.Ю. Введение в системы управления базами данных. Часть 1. Реляционная модель данных: Учебное пособие/Изд-е Башкирского ун-та. -Уфа, 1999.- 108 с.

33. Урман С., Хардман Р., МакЛафлин М. Oracle Database 10g. Программирование на языке PL/SQL; пер. с англ. СПб.: Питер, 2010. -792 с.

34. Мамаев Е. В. Microsoft ® SQL Server 2000. СПб.: БХВ-Петербург, 2004. -1280 с.

35. Михеев P. Н. MS SQL Server 2005 для администраторов. СПб.: БХВ-Петербург, 2006. - 544 с.40.3икопулос П. К., Бакларц Дж., деРус Д., Мельник Р. Б. DB2 версии 8: официальное руководство. М.: КУДИЦ-ОБРАЗ, 2004. - 373 с.

36. Глухарев М. Л. Разработка показателей и методов оценивания корректности реляционных баз данных // Известия Петербургского университета путей сообщения. Вып.1. - СПб.: ПГУПС , 2008. - С. 135148.

37. ГОСТ Р ИСО / МЭК 9126-93. Оценка качества программной продукции. Характеристики качества и руководства по их применению. М.: Госстандарт России, 2004. - 12 с.

38. ГОСТ Р 50922-2006. Защита информации. Основные термины и определения. -М.: Стандартинформ, 2006.

39. Ключевский Б. Программные закладки // Системы безопасности, связи и телекоммуникаций, №22, 1998. с. 60-66.

40. Герасименко В.А. Защита информации в автоматизированных системах обработки данных. М.: «Энергоатомиздат», 1994.

41. Руководящий документ Гостехкомиссии России «Защита от несанкционированного доступа к информации. Термины и определения» -М.: Военное издательство, 1992.

42. ISO/IEC 12207 Systems and Software Engineering Software Life Cycle

43. Processes. Geneva, Switzerland: ISO, 2008. 50.IEEE 1012-2004 IEEE Standard for Software Verification and Validation. IEEE, 2005.

44. ISO/IEC 15504-1 Information technology — Process assessment, Part 1:

45. Concepts and vocabulary. Geneva, Switzerland: ISO, 2004. 52. IEEE 829-1998. Standard for Software Test Documentation. New York: IEEE,1998.

46. IEEE 1008-1987. Standard for Software Unit Testing. In IEEE Standards: Software Engineering, Volume Two: Process Standards. New York: IEEE,1999.

47. ISO/IEC 14598-1 Information technology — Software product evaluation —

48. Part 1: General overview. Geneva, Switzerland: ISO, 1999. 55.ISO/IEC 14598-2 Information technology — Software product evaluation — Part 2: Planning and management. Geneva, Switzerland: ISO, 2000.

49. ISO/IEC 14598-3 Information technology — Software product evaluation — Part 3: Process for developers. Geneva, Switzerland: ISO, 2000.

50. ISO/IEC 14598-4 Information technology — Software product evaluation — Part 4: Process for acquirers. Geneva, Switzerland: ISO, 1999.

51. ISOAEC 14598-5 Information technology — Software product evaluation — Part 5: Process for evaluators. Geneva, Switzerland: ISO, 1998.

52. IEEE 1028 Standard for Software Reviews. New York: IEEE, 1998.

53. ГОСТ P ИСО/МЭК 13335-1-2006. Информационная технология. Методы и средства обеспечения безопасности. Часть 1. Концепция и модели менеджмента безопасности информационных и телекоммуникационных технологий. М.: Стандартинформ, 2007.

54. Федеральный закон РФ «О техническом регулировании» №184-ФЗ, 2002.

55. IEEE 1044 Standard Classification for Software Anomalies. New York: IEEE,1993.

56. IEEE 1044.1 Guide to Classification for Software Anomalies. New York: IEEE, 1995.

57. Бахтизин B.B., Глухова JI.A. Применение метрик сложности при разработке программных средств//Информатизация образования, №1, 2005. с.81-88.

58. Дейкстра. Э. Заметки по структурному программированию // У. Дал, Э. Дейкстра, К. Хоор. Структурное программирование. — М.: Мир, 1975. — с. 7-97.

59. IEEE 829-1998. Standard for Software Test Documentation. New York: IEEE, 1998.

60. Кулямин В.В. Перспективы интеграции методов верификации программного обеспечения // Труды ИСП РАН. Том 16. М.: ИСП РАН, 2009.-с. 73-88.

61. Глухарев М. JI. Современные методы и программные средства тестирования и верификации реляционных баз данных // Инновации на железнодорожном транспорте 2009: Сборник докладов юбилейной научно-технической конференции. - СПб.: ПГУПС, 2009. - с. 68-73.

62. Лукацкий А.В. Базы данных тоже уязвимы//Компьютер-пресс №8, М., 1999.

63. Codd E.F. A relational model for large shared data banks, Comm. ACM, 13:6 (1970), pp. 377-387.

64. Gupta A., Harinarayan V., Quass D. Aggregate-query processing in data warehousing environments, Proc. Intl. Conf. on Very Large Databases (1995), pp. 358 369.

65. Nicolas J.-M. Logic for improving integrity checking in relational databases, Acta Informica, 18:3 (1982), pp. 227 253.

66. Грэхем P., Кнут Д., Паташник О. Конкретная математика: Основание информатики. М.: МИР, 1998. - 703 с. J ;

67. Глухарев М. Л. Применение формальных описателей для логико-алгебраического моделирования требований целостности информации в реляционных базах данных // Известия Петербургского университета путей сообщения. СПб: ПГУПС, 2010. - Вып. 4 (25). - С. 78-88.

68. Francez N. Verification of programs, Addison-Wesley Publishers Ltd., 1992.

69. Дудаков С. M. Математическое введение в информатику: Учебное пособие. Тверь: Твер. гос. ун-т, 2003. 221 с.

70. Требования и спецификации в разработке программ. Сборник статей. М. Мир, 1984.

71. Баженова И. Ю. SQL и процедурно-ориентированные языки. http://www.intuit.ru/department/database/cdba/

72. Рамбо Дж. UML 2.0. Объектно-ориентированное моделирование и разработка. СПб.: Питер, 2007. - 540 с.

73. Буч Г., Рамбо Дж., Джекобсон А. Язык UML. Руководство пользователя = The Unified Modeling Language user guide. — 2-е изд. — M., СПб.: ДМК Пресс, Питер, 2004. — 432 с.

74. ISO/IEC 19501:2005. Information technology Open Distributed Processing -Unified Modeling Language (UML) Version 1.4.2. Geneva, Switzerland: ISO, 2005.

75. Рамбо Дж. UML 2.0. Объектно-ориентированное моделирование и разработка. СПб.: Питер, 2007. - 540 с.

76. Фридл Дж. Регулярные выражения, 3-е издание. Пер. с англ. -СПб.: Символ-Плюс, 2008. - 608 с.

77. Шилдт Г. Полный справочник по Java: Java SE 6 Edition. 7-е изд. - М.: Вильяме, 2007. - 1035 с.

78. Монахов В. В. Язык программирования Java и среда NetBeans. СПб: БХВ-Петербург, 2008. - 627 с.

79. Хопкрофт Дж., Мотвани Р., Ульман Дж. Введение в теорию автоматов, языков и вычислений. М.: Издательский дом «Вильяме», 2002. - 528 с.