Введение к работе
Актуальность темы исследования
Значительная часть современных автоматизированных
информационных систем (АИС) основана на использовании реляционных баз данных (БД). Качество БД оказывает значительное влияние на качество АИС в целом.
Одной из важнейших характеристик качества БД является информационная безопасность, которая, в свою очередь, включает в себя целостность информации. В теории реляционных БД целостность понимается как логическая согласованность и семантическая корректность данных. До начала разработки БД заказчик формулирует требования целостности, значимые в данной предметной области. Задача разработчика БД состоит в том, чтобы обеспечить программную реализацию этих требований в виде специальных программных объектов БД - ограничений целостности (ОЦ) и триггеров. Поддержка целостности в БД выполняется на требуемом уровне, если обеспечены:
пригодность ОЦ и триггеров, т. е. ОЦ и триггеры реализуют все специфицированные требования целостности;
корректность ОЦ и триггеров, т. е. работа ОЦ и триггеров приводит к ожидаемым результатам, в частности, ОЦ и триггеры не содержат случайных или умышленных недекларированных возможностей (НДВ).
Недостаточная пригодность и корректность ОЦ и триггеров может стать причиной нарушения целостности информации, что, в свою очередь, может привести к сбоям в работе АИС и связанным с ними проблемам в производственной деятельности организации, снижению качества продукции и услуг, экономическому ущербу, человеческим жертвам.
Верификацией называется процесс проверки соответствия различных компонентов АИС заданным требованиям, в том числе требованиям пригодности и корректности. Верификация позволяет обнаруживать в компонентах АИС ошибки и программные закладки, являющиеся разновидностями НДВ. Часть НДВ относится к уязвимостям компонентов АИС, так как при использовании НДВ возможно нарушение информационной безопасности. Таким образом, цели верификации пересекаются с целями анализа защищенности, направленного на выявление уязвимостей АИС, но не сводимого исключительно к выявлению НДВ. Диссертационное исследование посвящено разработке метода верификации и анализа защищенности реляционных БД, позволяющего выявлять НДВ в ОЦ и триггерах реляционных БД.
Вопросам общей теории верификации компонентов АИС, особенно
программного обеспечения, посвящены работы ряда отечественных и
зарубежных специалистов: В. В. Липаева, В. В. Кулямина,
А. А. Корниенко, M. А. Еремеева, M. М. Безкоровайного, Б. Боэма, Г. Майерса и др. Конкретные методы верификации описаны в работах Н. А. Абрамовой, А.В. Аграновского, В. А. Непомнящего, В. Е. Котова, Ч. Хоара, Р. Флойда, Э. Дейкстры, Р. Андерсона, Э. Кларка и др. авторов. Вопросы верификации БД, в том числе верификации целостности, рассматривают в своих работах П. Тонграк, Т. Саваннасарт, С. А. Халек, К. Бинниг, Н. Бруно, 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 таблиц.
