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

кандидата технических наук
Диасамидзе, Светлана Владимировна
город
Санкт-Петербург
год
2012
специальность ВАК РФ
05.13.19
Диссертация по информатике, вычислительной технике и управлению на тему «Метод выявления недекларированных возможностей программ с использованием структурированных метрик сложности»

Автореферат диссертации по теме "Метод выявления недекларированных возможностей программ с использованием структурированных метрик сложности"

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

ДИАСАМИДЗЕ СВЕТЛАНА ВЛАДИМИРОВНА

МЕТОД ВЫЯВЛЕНИЯ НЕД ЕКЛАР И Р ОВ А ИНЫХ ВОЗМОЖНОСТЕЙ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ СТРУКТУРИРОВАННЫХ МЕТРИК СЛОЖНОСТИ

05.13.19 - МЕТОДЫ И СИСТЕМЫ ЗАЩИТЫ ИНФОРМАЦИИ, ИНФОРМАЦИОННАЯ БЕЗОПАСНОСТЬ

Автореферат

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

1 3 ДЕН 2012

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

005057258

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

Ведущая организация: Федеральное государственное унитарное предприятие «ЗащитаИнфоТранс».

Защита диссертации состоится «25» декабря 2012 г. в 13.30 часов на заседании диссертационного совета Д 218.008.06 на базе Петербургского государственного университета путей сообщения по адресу: 190031, Санкт-Петербург, Московский пр., д. 9, ауд. 1-217.

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

Автореферат разослан «23» ноября 2012 г.

Ученый секретарь диссертационного совета кандидат технических наук,

профессор Кудряшов Владимир Александрович

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

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

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

доктор технических наук, профессор Кустов Владимир Николаевич, генеральный директор ООО «Удостоверяющий центр Газинформсервис»

кандидат технических наук, доцент Платонов Владимир Владимирович, профессор кафедры информационной безопасности компьютерных систем ФГБОУ ВПО «СПбГПУ»

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

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

Угрозы информационной безопасности, как указано в Стратегии национальной безопасности Российской Федерации до 2020 года, предотвращаются за счет совершенствования безопасности функционирования информационных и телекоммуникационных систем критически важных объектов инфраструктуры и объектов повышенной опасности в Российской Федерации, повышения уровня защищенности корпоративных и индивидуальных информационных систем. Также, на основании документа ФСТЭК России от 18.05.2007 г. «Общие требования по обеспечению безопасности информации в ключевых системах информационной инфраструктуры» система управления железнодорожным транспортом определяется как ключевая система, информационной инфраструктуры. Это, в свою очередь, определяет информационно-управляющие и автоматизированные системы, программные и программно-технические комплексы инфраструктуры железнодорожного транспорта и железнодорожного подвижного состава, в том числе и высокоскоростного, как системы управления критически важными объектами или технологическими процессами. Таким образом, для данных систем на железнодорожном транспорте выдвигаются усиленные требования к обеспечению информационной безопасности и защите информации.

Важную роль при обеспечении функциональной и информационной без опасности информационно-управляющих и автоматизированных систем играют верификация и подтверждение соответствия (сертификация и декларирование) программных средств (ПС) и' программно-технических комплексов. Вопросам общей теории верификации, оценки подтверждения соответствия, выбору и оцениванию характеристик качества и безопасности ПС посвящены работы ряда отечественных и зарубежных специалистов: В. В. Липаева, А. А. Корниенко, М. А. Еремеева, А. Г. Ломако, И. Б. Шубинского, В. В. Кулямина, Д. В. Богданова, В. В. Фильчакова, Г. Майерса, Б. Боэма, Ч. Хоара, Э. Дейкстры и др. Вопросы построения и применения метрической теории программ к проблеме верификации ПС рассматривают в своих работах М. Холстед, У. Хансен, Дж. Майерс, Т. Мак-Кейб, 3. Чен и другие авторы. Оценивание трудоемкости проектирования и качества разработки программ с использованием метрик сложности проводится с помощью специализированных ПС, разрабатываемых компаниями Abraxas Software, IBM, М Squared Technologies, MathWorks, McCabe Software, Microsoft, NDepend, ООО "PVS", Parasoft, Programming Research (PRQA), Rational Software, Scientifíc Toolworks, SonarSource и др.

Существующие процедуры и методы подтверждения соответствия ПС по требованиям безопасности информации обладают следующими недостатками:

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

функционально сложных информационных систем, и, как следствие большая трудоемкость работы эксперта;

• недостаточность предписанных нормативными документами проверок, непосредственно связанных с безопасностью ПС;

• неопределенность действий экспертов и достоверности получаемых результатов при отсутствии точно декларированных способов проведения некоторых предписанных проверок;

• сложность проведения испытаний в отсутствие исходных текстов программ.

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

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

Предмет диссертационного исследования - контроль наличия/отсутствия НДВ программных средств с использованием метрического анализа.

Цель диссертационного исследования — повышение полноты и сокращение временных затрат на проведение испытаний при контроле наличия/отсутствия НДВ программных средств.

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

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

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

• обоснование структурированных формальных моделей представления программных средств и оценивающих их метрик сложности;

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

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

2

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

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

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

• метод выявления дефектов, подобных НДВ, в программных средствах с использованием модели программы в виде схемы Янова и совокупности структурированных метрик сложности;

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

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

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

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

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

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

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

Практическая значимость результатов исследования состоит в возможности повышения полноты выявления НДВ и сокращении временных затрат при проведении испытаний при контроле отсутствия НДВ ПС за счет

3

использования разработанных метода и методики выявления НДВ программ в дизассемблированном коде с использованием структурированных метрик топологической и информационной сложности. В результате применения результатов исследования затраты времени на проведение статического анализа программного средства экспертом сократились в 1,5-2 раза.

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

• ФГБОУ ВПО ПГУПС;

• ООО «ЦБИ»;

• ФГУП «ЗащитаИнфоТранс».

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

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

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

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

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

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

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

В частности, отмечено, что в настоящее время в связи с комплексным характером требований к качеству и информационной безопасности информационно-управляющих и автоматизированных систем, подтверждение соответствия (сертификация и декларирование) ПС на железнодорожном транспорте осуществляется на добровольной основе в двух основных системах сертификации:

• по требованиям качества - в Системе сертификации на железнодорожном транспорте. В качестве основы для проведения испытаний используется одна из двух систем показателей качества ПС, базирующихся, соответственно, на критериальном аппарате ГОСТ 28195-89 «Оценка качества программных средств. Общие положения» и ГОСТ Р ИСО/МЭК 9126-93 «Информационная технология. Оценка программной продукции. Характеристика качества и руководства по их применению».

• по требованиям безопасности информации — в Системе сертификации средств защиты информации по требованиям безопасности информации. Для ПС железнодорожного транспорта преимущественно применяется сертификация по контролю отсутствия НДВ в соответствии с руководящим документом Гостехкомиссии (ФСТЭК) России «Защита от несанкционированного доступа к информации. Часть 1. Программное обеспечение средств защиты информации. Классификация по уровню контроля отсутствия недекларированных возможностей».

Процесс контроля наличия/отсутствия НДВ в исследуемом ПС включает в себя два основных этапа испытаний: статический анализ исходных текстов и динамический анализ ПС. Полный процесс статического анализа ПС включает в себя три основных вида исследования исходных текстов программы:

1. Лексический анализ, заключающийся в поиске лексем.

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

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

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

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

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

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

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

Таким образом, для выявления дефектов и НДВ были определены две базовые модели представления программ в соответствии с рассмотренными трактовками семантики программ:

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

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

Рисунок 1 - Структурированные формальные модели представления

программы

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

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

7

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

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

Третья глава посвящена разработке метода выявления дефектов, подобных НДВ, с использованием структурированных метрик сложности. Сущность метода состоит в формировании метрического базиса как совокупности структурированных метрик топологической и информационной сложности, соотнесенных с конструкциями языка ассемблер; последующем их ранжировании путем экспертного оценивания; приведении логической модели программы к продуктивной структуре, построенной на основе канонического представления схем Янова; экспериментальном определении «чувствительности» и корреляции выбранных компонент метрического базиса к изменениям программного кода, и, на этой базе, разработке системы критериев оценивания безопасности функциональных объектов (участков программного кода).

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

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

Таблица 1. Метрический базис

Метрический базис структуры программы

Показатель Конструкции языка ассемблер Метрика

т, Последовательность Последовательностей Метрика Джилба где Цоор - число операторов цикла; число операторов условного перехода; ¿я/4- число связей между подпрограммами.

т2 Последовательность Разветвлений Метрика Чена M(G) = (n(G),N,Q0) где n(G) - цикломатическое число; N- число операторов; Q0 - число пересечений

т3 Последовательность Циклов Метрика Вудворда Узловая мера (число узлов передач управления) YPO

т4 Разветвление Последовательностей Метрика Пивоварского где V*(G) - модифицированная цикломатическая сложность; P¡ - глубина вложенности í-ой предикатной вершины

т5 Разветвление Разветвлений Метрика точек пересечения Точка пересечения дуг появляется, если min(a,b) < min(p,q) < max(a,b) & max(p,q) > max(a,b) | min(a,b) < max(p,q) < max(a,b) & min(p,q) < min(a,b) где a,b — вершины графа.

т6 Разветвление Циклов Функциональная метрика Харрисона-Мейджела /* = Nc¡ If- сумма приведенных сложностей всех вершин управляющего графа; fx = ^ c¡ - отношение числа вершин графа к функциональному числу

т7 Цикл Последовательностей Метрика регулярных выражений P(G) = N+L+^k где N- число операндов; L - число операторов; 2 к - число скобок в регулярном выражении управляющего графа программы

те Цикл Разветвлений Метрика Пратта Мера сложности, удовлетворяющая следующим условиям: 1. Мера сложности простого оператора = 1. 2. = 3. M(IF_P_THEN F,"ELSE F¡)=2 MAX(M(F¡)M^2)) 4. M(WHILE P DO F)=2M(F)

т9 Цикл Циклов Метрика Мак-Клура M(P) = fp*X(P)+gp*Y(P) гдtfp и gp - соответственно число модулей, непосредственно предшествующих и следующих за модулем Р; Х(Р) - сложность обращения к модулю Р; Y(P) - сложность управления вызовом из модуля Р других модулей

Метрический базис информационной сложности программ

Показатель Свойства программы Метрика

т10 Эквивалентность Частичная эквивалентность Метрики размера программы п =П]+ пг-словарь программы, n¡, n¡ - количество уникальных операторов и операндов программы; N= N¡+N2 - длина программы, N¡, N2 - общее число операторов и операндов в программе; N*= nilog2n¡ +n2log2n2-теоретическая длина программы.

m,i Информационная энтропия Я (х)=-У (г) lo g 2 р (г) где п ' число состояний<ёистемы; p(i) - вероятность перехода системы в i-e состояние.

m¡2 Интеллектуальное содержание / = VxL где V - объем программы; L 2"и2 _ уровень реализации программы Щ-Ыг

m¡i Метрика Чепина Q = Р + 2М + ЗС + 0,5Т где Р - вводимые переменные; М- модифицируемые или создаваемые внутри программы переменные; С - управляющие переменные; Г- не используемые переменные.

m¡4 Метрика спена 1 " SP - среднее от числа утверждении, " м содержащих каждый конкретный идентификатор

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

{тх,т„т1й,тхг}>- {тг,т„т„т6,тд}у {т7,т8,тм,т13,т14} (1)

Наиболее предпочтительными являются метрические характеристики длины текста по Холстеду, метрики Джилба и точек пересечения, а также

метрика интеллектуального содержания.

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

признаков дефектов программ, подобных НДВ, и подготовки рекомендаций по их устранению.

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

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

ьи----—-1 Построение управляющего графа программы Г (В, Д> как начального отображения схемы Янова без предикатных условий

Р7

Нахождение минимш путей графа Г (Б,/ маршруты, минима соответствующую ьного покрытия всех '), определяющего тъно покрывающие ему схему С? (А, Р)

гШ-:--

Определение предикатных условий схемы С? (А, Р) путем символического выполнения программы по найденным маршрутам

гШ-—--

Приведение построенной схемы О (А, Р/ к

каноническому виду и построение продуктивной структуры путем применения аксиом и правил вывода эквивалентных преобразований

Рисунок 2 - Алгоритм приведения программы к продуктивной структуре на основе канонического представления схем Янова

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

1) характер относительных изменений между отдельными функциональными объектами (ФО) и ПС в целом метрик информационной

11

сложности: теоретической и реальной длины программы, метрики интеллектуального содержания и ее составляющих, в частности, уровня

реализации программы;

2) превышение для метрик Джилба и точек пересечения усредненного по ФО значения отношений среднеквадратического отклонения к математическому ожиданию, рассчитанных для всех ФО, некоторых граничных значений,

установленных экспериментально.

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

Словарь программы

Иосодное состояние программы Внедрение типовой программной закладки Т) Внедрение унихальной профаммной закладки

\

\

Интеллектуально« содержание

Уровень реализации программы

Рисунок 3 - Изменения значений метрик информационной сложности при наличии программных закладок

Экспериментально были определены граничные значения в соответствии со вторым критерием. Для этого для всех ФО было рассчитано отношение среднеквадратического отклонения к математическому ожиданию метрик Джилба и точек пересечения на двух этапах исследования программы: сразу после дизассемблирования исполняемого файла и после «очистки» программы путем приведения управляющего графа к продуктивной структуре на базе канонического вида схемы Янова. Тогда условие классификации выявленных дефектов как подобных НДВ и программных закладок определяется по формуле:

3(7. , т,

, где 1 = 1,5

(2)

Граничные значения кгр1 для метрик Джилба и точек пересечения зависят от сечений, в которых они рассчитываются. Для «очищенных» или свободных от

дефектов программ экспериментально были получены следующие «жесткие» граничные значения: кгр1 = 0,07; кгр5 — 0,005. С ростом количества исследованных программ и объема статистических данных эти граничные значения могут уточняться.

Дополнительным критерием может служить следующее отношение:

{С1 ! т^проЦукпиа* ^ j ^^

(сг, / т,)>1аассем5я

На практике это соотношение больше единицы и показывает степень «очищения» программы от простейших дефектов.

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

Рисунок 4 - Основные этапы методики выявления НДВ в исполняемом коде программы с использованием метрического анализа

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

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

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

Таблица 2. Среднее время проведения испытаний экспертом.

Среднее время проведения испытаний Объем исполняемого ПС

До 100 Кб 100 Кб-10 Мб 10 Мб-100 Мб

Стандартными инструментальными средствами 120 час 280 час 480 час

Инструментальными средствами с применением метрического анализа 80 час 160 час 200 час

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

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

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

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

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

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

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

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

6. Проведено исследование оперативности и полноты выявления НДВ на этапе статического анализа с использованием подсистемы метрического анализа. Показано, что оперативность и полнота выявления НДВ повышается в 1,5 —2 раза.

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

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

1. Диасамидзе C.B. Метод и методика выявления недекларированных возможностей программ с использованием структурированных метрик сложности // Известия Петербургского университета путей сообщения - СПб-ПГУПС, 2012. - Вып. 3 (32). - С. 29 - 36.

2. Диасамидзе C.B. Принцип сертификационных испытаний программных средств // Автоматика, связь, информатика. - 2009, № 7. - С. 29 - 30.

3. Диасамидзе C.B. Проблемы сертификационных испытаний программных средств связи. // Автоматика, связь, информатика. - 2009, № 2. -С. 31-32.

Публикации, не входящие в перечень, рекомендованный ВАК Мттнобрнауки России

4 Диасамидзе C.B., Новиков В.А., Платонов A.A. Использование метрик сложности для оценивания качества программ // Информационные технологии на железнодорожном транспорте: Доклады двенадцатой международной научно-практической конференции «Инфотранс-2007». - СПб.: ПГУПС, 2008. - С. 70 -72.

5 Корниенко A.A., Диасамидзе C.B. Использование метрик сложности для распознавания недекларированных возможностей и оценивания качества программного обеспечения // Телекоммуникационные, информационные и логистические технологии на транспорте России: Сборник докладов четвертой международной научно-практической конференции «ТелекомТранс-2008». -

Ростов н/Д.: РГУПС, 2008. - С. 74 - 78.

6. Корниенко A.A., Диасамидзе C.B. Оценка недекларированных возможностей и качества программного обеспечения II «Ведомственные и корпоративные сети и системы». - 2008, № 3. - С. 157 -160.

7. Диасамидзе C.B. Комплексные сертификационные испытания программных средств по требованиям качества и безопасности информации // Информационные технологии на железнодорожном транспорте: Доклады тринадцатой международной научно-практической конференции «Инфотранс-2008». - СПб.: ПГУПС, 2008. - С. 127 - 131.

8. Schäbe Hendrik, Tsyper Alexander, Корниенко A.A., Диасамидзе C.B. Сертификация программного обеспечения согласно европейским и российским стандартам безопасности для железнодорожных систем - сравнение // Интеллектуальные системы на транспорте: материалы I международной научно-практической конференции «ИнтеллектТранс-2011». - СПб.: ПГУПС, 2011. - С. 42 - 56.

9. Диасамидзе C.B. Использование метрик сложности для логической оценки качества разработки программных средств // Интеллектуальные системы на транспорте: материалы I международной научно-практической конференции «ИнтеллектТранс-2011». - СПб.: ПГУПС, 2011. - С. 130 - 134.

10. Корниенко A.A., Глухарев М.Л., Диасамидзе C.B., Захарченко С.С., Поляничко М.А. Методологические аспекты оценки й подтверждения соответствия и формальной верификации программных средств железнодорожного транспорта по требованиям качества и информационной безопасности // Интеллектуальные системы на транспорте: материалы П международной научно-практической конференции «ИнтеллектТранс-2012». -СПб.: ПГУПС, 2012. - С. 407-421.

Подписано к печати 20 .11.2012 г. ■• Печ.л. 1,0

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

Тираж 100 экз. 11Л(.

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

Оглавление автор диссертации — кандидата технических наук Диасамидзе, Светлана Владимировна

ВВЕДЕНИЕ.

1 СИСТЕМНЫЙ АНАЛИЗ ПРОБЛЕМЫ ПОДТВЕРЖДЕНИЯ

СООТВЕТСТВИЯ ПРОГРАММНЫХ СРЕДСТВ ПО ТРЕБОВАНИЯМ

БЕЗОПАСНОСТИ ИНФОРМАЦИИ НА ЖЕЛЕЗНОДОРОЖНОМ

ТРАНСПОРТЕ.

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

1.2 Анализ стандартов критериального аппарата и проблемных вопросов подтверждения соответствия программных средств по требованиям безопасности информации.

1.3 Общая характеристика методов исследования программ, верификации и выявления недекларированных возможностей программных средств

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

1.5 Постановка научной задачи исследования.

2 ОБОСНОВАНИЕ ПОДХОДА К СТРУКТУРИРОВАНИЮ

МОДЕЛЕЙ ПРЕДСТАВЛЕНИЯ ПРОГРАММ И МЕТРИК

СЛОЖНОСТИ НА ОСНОВЕ АНАЛИЗА СЕМАНТИК.

2.1 Анализ трактовок и подходов к формальному описанию семантики языков программирования.

2.2 Выбор моделей представления программ на основе структурированных семантик.

2.3 Построение логической модели программы с использованием граф-ориентированных схем Янова.

2.4 Построение метрической модели на основе требований к контролю отсутствия недекларированных возможностей.

Выводы по главе 2.

3 МЕТОД ВЫЯВЛЕНИЯ НЕДЕКЛАРИРОВАННЫХ

ВОЗМОЖНОСТЕЙ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ

СТРУКТУРИРОВАННЫХ МЕТРИК СЛОЖНОСТИ.

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

3.2 Построение метрического базиса как совокупности структурированных метрик топологической и информационной сложности.

3.3 Приведение программы к продуктивной структуре на основе канонического представления схем Янова.

3.4 Формирование системы критериев для классификации выявленных дефектов как подобных НДВ.

Выводы по главе 3.

4 МЕТОДИКА ВЫЯВЛЕНИЯ НЕДЕКЛАРИРОВАННЫХ

ВОЗМОЖНОСТЕЙ ПРОГРАММ И ПРАКТИЧЕСКИЕ

РЕКОМЕНДАЦИИ ПО ИСПОЛЬЗОВАНИЮ

СТРУКТУРИРОВАННЫХ МЕТРИК СЛОЖНОСТИ.

4.1 Место и роль метрических оценок в системе статического анализа программных средств.

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

Выводы по главе 4.

Введение 2012 год, диссертация по информатике, вычислительной технике и управлению, Диасамидзе, Светлана Владимировна

Угрозы информационной безопасности, как указано в Стратегии национальной безопасности Российской Федерации до 2020 года, предотвращаются за счет совершенствования безопасности функционирования информационных и телекоммуникационных систем критически важных объектов инфраструктуры и объектов повышенной опасности в Российской Федерации, повышения уровня защищенности корпоративных и индивидуальных информационных систем. Также, на основании документа ФСТЭК России от 18.05.2007 г. «Общие требования по обеспечению безопасности информации в ключевых системах информационной инфраструктуры» система управления железнодорожным транспортом определяется как ключевая система информационной инфраструктуры. Это, в свою очередь, определяет информационно-управляющие, автоматизированные системы, программные и программно-технические комплексы инфраструктуры железнодорожного транспорта и железнодорожного подвижного состава, в том числе и высокоскоростного, как системы управления критически важными объектами или технологическими процессами. Таким образом, для данных систем на железнодорожном транспорте выдвигаются усиленные требования к обеспечению информационной безопасности и защите информации.

Важную роль при обеспечении функциональной и информационной безопасности информационно-управляющих и автоматизированных систем играет верификация и оценка соответствия программных средств и программно-технических комплексов информационно-управляющих систем. Вопросам общей теории верификации и оценки соответствия программного обеспечения посвящены работы ряда отечественных и зарубежных специалистов: В. В. Липаева, А. А. Корниенко, М. А. Еремеева, А. Г. Ломако, И. Б. Шубинского, В. В. Кулямина, Д. В.

Богданова, В. В. Фильчакова, Г. Майерса, Б. Боэма, Ч. Хоара, Э. Дейкстры и др. Вопросы построения и применения метрической теории программ к проблеме верификации программных средств рассматривают в своих работах М. Холстед, У. Хансен, Дж. Майерс, Т. Мак-Кейб, 3. Чен и другие авторы. Оценивание трудоемкости проектирования и качества разработки программ с использованием метрик сложности проводится с помощью специализированного программного обеспечения, разрабатываемого компаниями Programming Research (PRQA), Scientific Toolworks, MathWorks, Parasoft, McCabe Software, Rational Software, Abraxas Software, IBM, Microsoft, M Squared Technologies, SonarSource, NDepend, ООО "Program Verification Systems" и др.

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

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

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

• неопределенность действий экспертов и достоверности получаемых результатов при отсутствии точно декларированных способов проведения некоторых предписанных проверок;

• сложность проведения испытаний в отсутствие исходных текстов программ.

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

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

Предмет диссертационного исследования - контроль наличия/отсутствия НДВ ПС с использованием метрического анализа.

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

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

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

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

• обоснование структурированных формальных моделей представления ПС и оценивающих их метрик сложности;

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

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

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

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

• метод выявления дефектов, подобных НДВ, в программных средствах с использованием модели программы в виде схемы Янова и совокупности структурированных метрик сложности;

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

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

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

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

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

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

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

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

Практическая ценность и новизна работы подтверждаются актами внедрения, выданными ФГБОУ ВПО ПГУПС, ООО «ЦБИ», ФГУП «ЗащитаИнфоТранс».

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

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

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

Заключение диссертация на тему "Метод выявления недекларированных возможностей программ с использованием структурированных метрик сложности"

Выводы по главе 4

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

ВДВ.

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

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

ЗАКЛЮЧЕНИЕ

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

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

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

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

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

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

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

6. Проведено исследование оперативности и полноты выявления НДВ на этапе статического анализа с использованием подсистемы метрического анализа. Показано, что оперативность и полнота выявления НДВ повышается в 1,5 - 2 раза.

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

Библиография Диасамидзе, Светлана Владимировна, диссертация по теме Методы и системы защиты информации, информационная безопасность

1. Федеральный закон «О техническом регулировании» № 184-ФЗ от 27.12.2002 г. эл. ресурс http://www.gost.ru/wps/portal/.

2. Технический регламент о безопасности железнодорожного подвижного состава, утв. постановлением Правительства РФ № 524 от 15 июля 2010 г. эл. ресурс http://www.gost.ru/wps/portal/.

3. Технический регламент о безопасности инфраструктуры железнодорожного транспорта, утв. постановлением Правительства РФ № 525 от 15 июля 2010 г. эл. ресурс http://www.gost.ru/wps/portal/.

4. Технический регламент о безопасности высокоскоростного железнодорожного транспорта, утв. постановлением Правительства РФ № 533 от 15 июля 2010 г. эл. ресурс http://www.gost.ru/wps/portal/.

5. Алферова З.В. Теория алгоритмов. М.: Статистика. 1973.164 с.

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

7. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции. Т. 1: Синтаксический анализ. М.: Мир, 1978. - 612 с.

8. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции. Т. 2: Компиляция. М.: Мир, 1978. - 487 с.

9. Ахо А., Сети Р., Ульман Дж. Компиляторы: принципы, технологии и инструменты. М.: Издательский дом «Вильяме», 2001. -768 с.

10. Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика: пер. с англ. М.: Мир, 1985. - 606 с.

11. Богданов Д.В., Фильчаков В.В. Стандартизация жизненного цикла и качества программных средств: Учебное пособие. СПб.: ГУАП, 2000.-210 с.

12. Боэм Б., Браун Дж., Каспар X., Липов М., Мак-Леод Г., Мерит М. Характеристики качества программного обеспечения. / пер. с англ. -М.: Мир, 1981.-208 с.

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

14. Бэкус Дж. Алгебра функциональных программ: мышление функционального уровня, линейные уравнения и обобщенные определения // Математическая логика в программировании: Сб. статей 1980 1988 гг.: пер. с англ. -М.: Мир, 1991. - С. 8 - 53.

15. Вирт Н. Алгоритмы + структуры данных = программы. М., Мир, 1985.-336 с.

16. Волкова И.А., Руденко Т.В. Формальные грамматики и языки. Элементы теории трансляции. -М.: Издательский отдел факультета ВМиК МГУ им. М.В. Ломоносова, 1999. 62 с.

17. Дал У., Дейкстра Э., Хоар К. Структурное программирование: пер. с англ. М. Мир, 1975. - 247с.

18. Дейкстра Э. Дисциплина программирования. М.: Мир,1978.275 с.

19. Диасамидзе C.B. Метод и методика выявления недекларированных возможностей программ с использованием структурированных метрик сложности // Известия Петербургского университета путей сообщения. СПб: ПГУПС, 2012. - Вып. 3 (32). - С. 29 -36.

20. Диасамидзе C.B. Принцип сертификационных испытаний программных средств // Автоматика, связь, информатика. 2009, № 7. - С. 29-30.

21. Диасамидзе C.B. Проблемы сертификационных испытаний программных средств связи // Автоматика, связь, информатика. 2009, № 2.-С. 31-32.

22. Донаху Д. Взаимодополняющие определения семантики языка программирования. / В кн.: Семантика языков программирования. М.: Мир, 1980.-С. 222-394.

23. Ершов А.П. Введение в теоретическое программирование (беседы о методе). -М.: Наука, 1977. 288 с.

24. Ершов А.П. Современное состояние теории схем программ // В сб.: Проблемы кибернетики, вып. 27. -М.: Наука, 1973. С. 87 - 110.

25. Ершов А.П. Об операторных схемах Янова // В сб.: Проблемы кибернетики, вып. 20. -М.: Физматгиз, 1968. С. 181 - 200.

26. Ершов IO.JI. Определимость и вычислимость. Новосибирск: Научная книга, 1996. - 300 с.

27. Ершов IO.JI. Теория нумераций.-М.: Наука, 1977.-416 с.

28. Изосимов A.B., Рыжко A.JL Метрическая оценка качества программ. М.: Изд. МАИ, 1989. - 96 с.

29. Казиев В.М. Введение в анализ, синтез и моделирование систем. М.: Интернет-Университет Информационных технологий «Интуит.ру»; БИНОМ. Лаборатория знаний, 2008. - 248 с.

30. Кауфман В.Ш. Языки программирования. Концепции и принципы. М., Радио и связь, 1993. - 432 с.

31. Клини C.K. Введение в метаматематику. М.: ИЛ, 1957. - 526 с.

32. Клини C.K. Математическая логика. М.: Мир, 1973. - 480 с.

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

34. Корниенко A.A., Бубнов В.П. Проблемы подтверждения соответствия и сертификации программных средств информационно-управляющих систем железнодорожного транспорта // Сборник докладов XIIIМНПК «Инфотранс-2008». СПб.: ПГУПС, 2008. - С. 7 - 14.

35. Корниенко A.A., Диасамидзе C.B. Подтверждение соответствия и сертификация программного обеспечения по требованиям безопасности информации: Учебное пособие. СПб.: ПГУПС, 2009. - 55 с.

36. Корниенко A.A., Сафонов В.И. Обязательное подтверждение соответствия программных средств железнодорожного транспорта // Транспорт Российской Федерации. 2009, № 3(22). - С. 36 - 39.

37. Криницкий H.A. Равносильные преобразования алгоритмов и программирование. М.: Советское радио, 1970. - 304 с.

38. Лаврищева Е.М., Петрухин В.А. Методы и средства инженерии программного обеспечения: Учебник. М.: МФТИ (ГУ), 2006. - 304 с.

39. Липаев В.В. Тестирование программ. М.: Радио и связь, 1986. - 296 с.

40. Ляпунов A.A. О логических схемах программ. // В сб.: Проблемы кибернетики, вып. 1. М.: Физматгиз, 1958. - С. 46 - 74.

41. Маевский Д.А., Яремчук С.А. Оценка количества дефектов программного обеспечения на основе метрик сложности //

42. Электротехнические и компьютерные системы. Одесса: ОНПУ, 2012. -№ 07(83).-С. 113-120.

43. Майерс Г. Надежность программного обеспечения. / пер. с англ.; под ред. В.Ш. Кауфмана. М.: Мир, 1980. - 360 с.

44. Манна 3. Теория неподвижной точки программ // Кибернетический сборник, № 15. -М.: Мир, 1978. С. 38 - 100.

45. Молчанов А.Ю. Системное программное обеспечение: учебник для вузов. 3-е изд. СПб.: Питер, 2010. - 400 с.

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

47. Платонов А.А., Горемыкин Д.В., Еремеев М.А., Ломако А.Г., Новиков В.А., Гнидко К.О. Метод обнаружения дефектов в бинарных дампах памяти. // Компьютерные системы. Проблемы информационной безопасности. № 3. - СПб.: 2009. - С. 25 - 32.

48. Подловченко Р.И. О проблеме эквивалентных преобразований программ // Программирование. 1986, № 6. - С. 3 - 14.

49. Подловченко Р.И. От схем Янова к теории схем программ // В сб.: Математические вопросы кибернетики, вып. 7. М., Физматлит, 1998. -с. 281 -302.

50. Пратт Т., Зелковиц М. Языки программирования: разработка и реализация. 4-е изд. СПб.: Питер, 2002. - 688 с.

51. Себеста Р.У. Основные концепции языков программирования. -М.: Издательский дом «Вильяме», 2001. 672 с.

52. Серебряков В.А., Галочкин М.П., Гончар Д.Р., Фуругян М.Г. Теория и реализация языков программирования. М.: МЗ Пресс, 2006. -352 с.

53. Синицын С.В., Налютин Н.Ю. Верификация программного обеспечения: учебное пособие. М.: Интернет-Университет

54. Информационных технологий.«Интуит.ру»; БИНОМ. Лаборатория знаний, 2008.-368 с.

55. Скотт Д.С. Области в денотационной семантике. // Математическая логика в программировании: Сб. статей 1980 1988 гг. / пер. с англ.-М.: Мир, 1991.-С. 56-118.

56. Смит Д. Дж., Симпсон К. Дж. Л. Функциональная безопасность. Простое руководство по применению стандарта МЭК 61508 и связанных с ним стандартов. М.: Издательский дом «Технологии», 2004. - 208 с.

57. Турчин В. Ф. Алгоритмический язык рекурсивных функций (РЕФАЛ). — М.: ИПМ АН СССР, 1968.

58. Турчин В.Ф. Метаалгоритмический язык. // Кибернетика. -1968, №4.- С. 116-124.

59. Турчин В.Ф. Эквивалентные преобразования программ на РЕФАЛе. // В сб.: Автоматизированная система управления строительством. Труды ЦНИПИАСС, № 6. М.: ЦНИПИАСС, 1974. -С. 36-68.

60. Филд А., Харрисон П. Функциональное программирование. -М.: Мир, 1993.-637 с.

61. Холстед М.Х. Начала науки о программах / пер. с англ. В.М. Юфы. М.: Финансы и статистика, 1981. - 128 с.

62. Яблонский С. В. Элементы математической кибернетики. М.: Высшая школа, 2007. - 191 с.

63. Янов Ю.И. Предельно полная система правил эквивалентных преобразований для программ, вычисляющих всюду определенные функции. // В сб.: Проблемы кибернетики, вып. 37. — М.: Наука, 1980. С. 215-238.

64. Янов Ю.И. О локальных преобразованиях схем алгоритмов. // В сб.: Проблемы кибернетики, вып. 20. -М.: Физматгиз, 1968. С. 201 - 216.

65. Янов Ю.И. О логических схемах алгоритмов. // В сб.: Проблемы кибернетики, вып. 1. -М.: Физматгиз, 1958. С. 29 - 53.

66. Church A. An Unsolvable Problem of Elementary Number Theory // Bulletin of the American Mathematical Society. 1935. Vol. 41. - P. 332-333.

67. Cook W., Hill W.L., Canning P.S. Inheritance is not subtyping. // In: Proc. 17th ACM Symposium on Principles of Programming Langauges, Jan. 1990.-P. 125- 135.

68. Dijkstra T.W. Finding the Correctness proof of a concurrent program // Proc.Konf. Nederland Acad.Wetenach, 1978. Vol. 81, № 2. - P. 207-215

69. Floyd R. Assigning meaning to programs // Mathematical Aspects Computer Science. Amer. Math. Soc. 1967. Vol. XIX. - P. 19 - 32.

70. Hoare C.A. An axiomatic basis for computer programming // Communications ACM. 1969. Vol.12, № 10. - P. 576 - 583.

71. Hoare C.A. Proof of correctness of data representation // Acta Informatica, № 1(4), 1972. P. 214-224.

72. Knuth D.E. Semantics of Context-Free Languages // Mathematical Systems Theory, 1968. Vol. 2, № 2. - P. 127 - 146.

73. McCabe T.J. A complexity measure // IEEE Transactions on Software Engineering, December, 1976. Vol. SE-2, № 4. - P. 308 - 320.

74. McCarthy J., Abrahams P.W., Edwards J., Hart T.P., Levin M.I. LISP 1.5 Programmer's Manual. M.I.T. Press, Cambridge, Massachusetits, 1965.

75. Sommerville I. Software Engineering . Hardcover, Addison Wesley Longman, 1996. - 742 p.

76. Scott D.S. Lectures on a mathematical theory of computations. -Oxford University Computing Laboratory Technical Monograph. PRG-19, 1981.- 148 p.

77. Stoy J. E. Denotational semantics: the Scott-Strachey approach to programming language theory. M.I.T. Press, Cambridge, Massachusetts, 1977.