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

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ИМЕНИ М.В.ЛОМОНОСОВА Механико-математический факультет

Пучков Федор Михайлович

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

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

АВТОРЕФЕРАТ диссертации па соискание ученой степени кандидата физико-математических наук

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

Москва - 2010

2 5 Щ? 20(0

003494530

Работа выполнена на Механико-математическом факультете и в Институте проблем информационной безопасности Московского государственного университета имени М. В. Ломоносова.

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

доктор физико-математических наук, профессор Васенш Валерий Александрович.

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

доктор технических наук, профессор Тимонина Елена Евгеньевна;

кандидат физико-математических наук, Когжюхин Константин Александрович.

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

Институт системного программирования РАН.

Защита состоится 24 марта 2010 г. в 16 час. 45 мин. на заседании диссертационного совета Д 501.002.16 при Московском государственном университете имени М. В. Ломоносова по адресу: Российская Федерация. 119991, Москва, ГСП-1, Ленинские горы, д. 1, Московский государственный университет имени М. В. Ломоносова. Механико-математический факультет, ауд. 14-08.

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета Московского государственного университета имени М. В. Ломоносова.

Автореферат разослан 24 февраля 2010 г.

Ученый секретарь

Л11 ее ерта щ I о 11 н о го со ве га,

доктор физико-математических паук, доцент

Ж'

Корпев А. А.

Общая характеристика работы

Актуальность работы. Одним из важнейших условий успешного функционирования практически значимых объектов, потенциально уязвимых для кибератак, является защита используемого в их составе программного обеспечения от возможных сбоев в работе. Это условие становится особенно важным при проектировании автоматизированных систем с высоким уровнем требований к их защищенности, в том числе — при разработке и реализации программно-технических средств защиты информации, что отражено в соответствующих Руководящих документах ФСТЭК РФ.1'2-3 Появление подобных сбоев зачастую связано с наличием уязвимостей (ошибок, дефектов) в программных средствах подобных систем. В их числе такие, использование которых злоумышленником может привести к нерегламентнрованному политикой информационной безопасности повышению его привилегий на том или ином узле системы, подлежащей защите. Кроме того, сбои в работе программ могут приводить к аварийному завершению работы важных программно-аппаратных компонентов, создавая угрозу отказа для системы в целом. Имея в виду существующие подходы к разработке и последующему сопровождению программного обеспечения,4 в частности, на основе уже существующих средств с открытым исходным кодом, на первый план выходят следующие задачи:

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

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

■. • • обоснование отсутствия других уязвимостей (дефектов) в используемом программном обеспечении.

Актуальность выбора для анализа именно программ, написанных с использованием языка программирования С, обусловлена широкой распространенностью этого языка в среде программного обеспечения с открытым исходным кодом. Согласно проведенным исследованиям, на долю языка С приходится более 80%

'Защита от несанкционированного доступа к информации. Термины и определения. //' Руководящий документ. Гостехкомиссия России. 1902.

2Средства вычислительной техники. Защита от несанкционированного доступа к информации. Показатели защищенности от несанкционированного доступа к информации. // Руководящий документ. Гостехкомиссия России. 1992.

^Средства вычислительной техники. Защита от несанкционированного доступа к информации. Чисть 1. Программное обеспечение средств защиты информации. Классификация по уровню контроля отсутствия ¡^декларированных возможностей. // Руководящий документ. Гостехкомиссия России, 1992.

4Лнпаев В. В. Программная инженерия. Методологические основы. — М.: Теис, 2006. — (¡08 с.

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

Следует отметить, что в настоящее время эффективных и широко распространенных автоматизированных средств, позволяющих проверять корректность программ на языке С и выявлять в них возможные уязвимости, не существует. Традиционные средства статического анализа (аудита) исходного кода недостаточно точно анализируют семантику программы, и, как следствие, — приводят к большому количеству ложных предупреждений. Например, программный комплекс ITS47 анализирует лишь наборы лексем, сопоставляя их с образцами «потенциально опасных конструкций», хранящимися в специальной базе данных. Подобный алгоритм проверки может выдавать до 100% ложных предупреждений, не обнаружив при этом в исследуемой программе ни одной реальной уязвимости. Программный комплекс Splint,8 позволяет находить лишь простейшие уязвимости такие, как, например, выход за границу статического массива при обращении по фиксированному индексу. Для обнаружения уязвимостей в более сложных ситуациях анализатору необходимо предоставить специальные аннотации, составление которых представляется весьма трудоемкой процедурой. Программный комплекс BOON9 реализует один из простейших вариантов «интервального анализа» — для каждой целочисленной переменной х вычисляется интервал [а, Ь] ее возможных значений такой, что в каждой точке программы справедливо соотношение а < х < Ъ. К недостаткам алгоритма можно отнести следующие факторы, значительно снижающие точность анализа.

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

• Отсутствует анализ указателей.

• Не исследуются зависимости между различными переменными.

5Wheeler D. More Than a Gigabuck: Estimating GNU/Linux's Size. [Электронный pccypc|. Режим доступа: http://www.dwhe9ler.com/sloc/rediiat71-vl/redhat71sloc,html, свободный. — Электрон, текст, док.

ßMeasuring Libre Software Using Dobian 3.1 (Sarge) as A Case Study: Preliminary Results. (Электронный ресурс]. Режгш доступа: http://www.upgrade-cepis.Org/is5ues/2005/3/up6-3Amor.pdi, свободный. — Электрон, текст, док.

7ITS4: Software Security Tool. [Электронный pccypcj. Режим доступа: http://www.cigital.com/its4/, свободный.

"Splint - Secure Programming T.iut- [Э-лектронпьгА ресурс] Режим доступа: http : .//www. splint. org, свобод-

ный.

''BOON - Buffer Overrun deteetiON. [Электронный pecypc|. Режим доступа: http://www.eecs.berkley. edu/~daw/boon/. свободный.

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

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

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

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

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

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

И|0<¡verity. |Э.лектронный ресурс]. Режим доступа: http://www.coverity.com/, свободный.

"PolySpace Embedded Software Verification. [Электронный ресурс]. Режим доступа; http://www.mathworks. com/productз/polyspace/. свободный.

12Thu ASTREE StaLic Analyzer. [Электронный ресурс]. Режим доступа: http://www.astree.ens.fr/, свободный.

13Valsi'ind. [Электронный ресурс]. Режим доступа: http://www.valgrind.org, свободный.

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

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

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

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

• предложен метод автоматизированного обнаружения дефектов в программах на языке С, основанный па преобразовании исходной программы в промежуточный формат «IAL» (от Intermediate Analyser Language) с последующей верификацией полученной IAL-нрограммы;

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

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

• создан прототип программного комплекса автоматизированного обнаружения дефектов в программах на языке С, эффективность которого продемонстрирована как на ряде специально подобранных модельных примеров, так и на примере программы xorg-server — основной части подсистемы управления графикой в UNIX-подобных операционных системах.

Апробация работы. Основные результаты диссертации докладывались на международной научной конференции «Информационная безопасность регионов России (ИБРР-2003)», на международных конференциях «Математика и безопасность информационных технологий» (2004-2006), «Ломоносовские чтения» (20062007), па механико-математическом факультете МГУ имени М.В. Ломоносова на семинаре «Проблемы современных информационно-вычислительных систем» под руководством д.ф.-м.н., проф. В.А. Васенина (2004. 2009).

Публикации. По теме диссертации опубликовано 10 научных работ, в том числе в зарубежных журналах, из них одна статья [3] в журнале из перечня ВАК ведущих рецензируемых журналов, а также — 4 патента на изобретения. Материалы работы вошли в главу 7 опубликованной в 2008 году книги «Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия» под ред. д.ф.-м.н., проф. В.А. Васенина [6].

Личный вклад автора. Автором проведено исследование современного состояния в области автоматизации процессов верификации и обнаружения дефектов программного обеспечения; предложен метод обнаружения дефектов в программах на языке С, основанный на преобразовании исходной программы в промежуточный формат «IAL» (от Intermediate Analyser Language) с последующей верификацией полученной IAL-программы; разработан язык IAL (описаны его синтаксис и семантика); предложена математическая модель и алгоритм верификации IAL-программ, в рамках которой автором доказана корректность предложенного алгоритма; разработан модуль верификации IAL-программ, являющийся основой программного комплекса автоматизированного обнаружения дефектов в С-программах, созданного автором совместно с К. А. Шапченко и О. О. Андреевым.

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

Содержание работы

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

Первая глава является вводной и посвящена исследованию и систематизации рассматриваемой предметной области. В па,чале главы приводится ряд определений.

Определение 1.1. Уязвимость вычислительной системы — такое ее состояние, которое позволяет субъекту (потенциальному злоумышленнику) получить несанкционированный политикой информационной безопасности доступ к ее ресурсам, кыятть отказ в обслуживании, или каким-либо другим образом нарушить штатный режим функционирования.

Определение 1.2. Уязвимость программного обеспечения (программы,J — такое ее свойство, которое позволяет субъекту (потенциальному злоумышленнику) привести систему в состояние уязвимости, воздействуя определенным образом на внешнее окружение, в котором выполняется программа.

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

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

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

Определение 1.5. Программным дефектом (применительно к программам на некотором языке программирования) будем называть операцию в программе, результат выполнения которой (при определенном воздействии на внешнее окружение программы) приводит к аварийному завершению работы программы, либо является неопределенным согласно спецификации используемого языка программирования.

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

• некорректные операции с памятью;

• некорректные операции с целыми типами;

• некорректное использование функций стандартной библиотеки;

• операции чтения неопределенного значения;

• утечки памяти;

• другие.

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

В разделе 1.2 проводится обзор существующих методов и средств обнаружения уязвимостей (дефектов) в программах на языке С.

В подразделе 1.2.1 на примере программных средств GNU grep,14 Flawfinder,15 ITS410 показана неэффективность использования только средств лексического и синтаксического анализа для решения задачи автоматизированного обнаружения уязвимостей в программах на языке С.

В подразделах 1.2.2-1.2.3 рассматриваются программные средства Splint,17 BOON,18 реализующие несложный семантический анализ. Основными их недо-

!4The GNU Grep.3;3 [Электронный рссуре]. Режим доступа: http://wwu.gnu.org/softvare/grep/, свободный.

i5F¡awñndcr. [Электронный рсеурс[. Режим доступа: http://www.dweeler.com/flawfinder/, свободный.

lhÍTS4: Software Security Tool. [Электронный peeypc[. Режим доступа: bttp://www.cigital.con/its4/. свободный.

17Splint — Secure Programming Lint. [Электронный ресурс]. Режим доступа: http://www.splint.org, свободный.

'"BOON Buffer Overrun detcctiON. ¡Электронный ресурс]. Режим доступа: http://www.eecs.berkley. edu/~daw/boon/, свободный.

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

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

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

1) проведение лексического и синтаксического анализа С-программы, построение

дерева разбора/абстрактного синтаксического дерева;

2) преобразование дерева разбора в промежуточное представление;

3) верификация программы на языке промежуточного представления.

Лексический и синтаксический анализ представляет собой процесс сопоставления линейной последовательности символов программы с формальной грамматикой языка С (согласно стандарта «С99»). Результатом является дерево разбора или абстрактное синтаксическое дерево.

Преобразование дерева разбора в промежуточное представление. Структура абстрактного синтаксического дерева С-программы является достаточно сложной. По этой причине на втором шаге осуществляется преобразование дерева в более простой формат, называемый «промежуточным представлением». Промежуточное представление является программой, в некотором смысле эквивалентной исходной, написанной на специально разработанном для этого языке IAL (от Intermediate Analyser Language). Подробное описание языка IAL представлено в разделе 2.3 диссертации. Рассмотрим наиболее значимые его особенности.

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

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

• Переменные в IAL-программе играют роль «регистров». А именно, они позволяют хранить значения различных типов, однако для переменной отсутствует понятие адреса или участка памяти, содержащего ее значение. Участки памяти, доступные по указателю, выделяются в IAL-программе динамически инструкцией new, а освобождаются — инструкцией del.

• В языке IAL принята упрощенная система типов. Определено восемь целых типов,.а именно: int8, intl6, int32, int64,. uint8, uintl6, uint32, uint64, а. также тип указателя ptr. Для каждого из представленных типов в точности определена его разрядность, множество допустимых значений, семантика арифметических операций со значениями этого типа. Вместе с тем, отсутствуют типы чисел с плавающей точкой, массивы, структуры, объединения. Операции с объектами этих типов моделируются соответствующими операциями с участками памяти.

• Язык IAL представляет собой разновидность трехадрсспого кода. Сложные выражения представлены в виде последовательности «атомарных» инструкций, а управляющие конструкции преобразованы в эквивалентные с использованием операторов if-goto и goto.

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

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

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

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

Свойство корректности алгоритма верификации 1АЬ-программ (в предположении корректности алгоритма преобразования С-программ в промежуточное представление) является необходимым и достаточным условием полноты всего алгоритма обнаружения программных дефектов в программах на языке С.

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

Определение 2.7. Пусть п — номер некоторой инструкции 1АЬ-программы Р. Инвариантом программы Р в точке п будем называть логическую формулу <р, связывающую значения переменных и состояние памяти программы, истинную всякий раз, когда текущая выполняемая инструкция имеет номер п.

Определение 2.8. Пусть п — номер некоторой инструкции 1АЬ-программы Р. Условием корректности программы Р в точке п будем называть логическую формулу ф', связывающую значения переменных и состояние памяти программы, которая выражает необходимые и достаточные условия, при которых выполнение инструкции с Номером п пе приведет к аварийному состоянию.

Пусть <р — инвариант программы Р в точке п, а ф — условие корректности в этой же точке. Тогда, если формула (<р ф) истинна при любых значениях входящих в нее свободных переменных (нлн, что эквивалентно, формула Л -<ф) невыполнима), то корректность выполнения инструкции с номером п будем считать доказанной. Данный принцип положен в основу следующего алгоритма (через \P.Stmtl обозначено число инструкций в программе Р, а через Р.81т1[п\ — инструкция с номером п):

IAL-VERIFY(P)

1 сс := GENERATE-CC(P) t> Сгенерировать массив условий корректности сс

2 inv := GENERATE-INV(P) £> Сгенерировать массив инвариантов inv

3 ит n := С s> Текущей список предупреждений turn

4 Г, for n := 1 to \P.Stmt\ do > P. Stmt ~ массив инструкций программы Р

G if СНЕОК-ЯАТ(тф) Л -cc|nj) then

7 u-rn := (icrn,P.S,imt[n]) > Добавить инструкцию P.Simi[n] в конец

& текущего списка предупреждений

8 end

9 return wf ii

В разделе 2.3 диссертации приводится детализированное описание языка IAL, его синтаксиса и семантики.

В разделе 2.4 строится математическая модель языка IAL. Программа представляет собой тройку Р = (Vor, Туре, Stmt), где Vai— множество переменных; Туре — отображение, сопоставляющее каждой переменной ее тип; Stmt — конечное упорядоченное множество инструкций программы. С целью формализации процесса выполнения IAL-программы рассматривается система переходов состояний Ер = (5, Т, s-initi Е), гДе S ~ множество состояний системы (не обязательно конечное): Т С S х S — отношение, определяющее возможность перехода в следующее состояние; ,3;„й — начальное состояние; Е С S — множество ошибочных состояний, причем $ш £ (S\E). Состояния множества (S\E) называются корректными. В разделе 2.4 описан каждый из указанных компонентов.

В разделе 2.5 исследуется формальная логическая система 7, являющаяся основой для построения инвариантов и условий корректности. При этом инварианты и условия корректности являются формулами системы 3\

В разделе 2.6 приведен базовый алгоритм решения задачи генерирования инвариантов, сформулирована и доказана теорема о корректности базового алгоритма.

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

Пусть задана программа Р, и G = (V, Е) — ее управляющий граф, start — начальная вершина. При этом предполагается, что

1) любая вершина графа G достижима из start;

2) prev(start) = 0.

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

белый —» серый —» черный.

Множество черных вершин будем обозначать через В1, множество серых вершин — через Gr.

Определение 3.1. Раскраской графа G будем называть пару (Bl,Gr), позволяющую определить цвет каждой его вершины.

Сформулируем правила, перекрашивания вершин и укажем порядок их использования.

Правило А. Пусть V — белая вершина и пусть одна из соседних предшествующих вершин (то есть одна из вершин множества ргеу (и)) является мерной. Тогда V может быть перекрашена в серый цвет (рис. 2.1).

Правило В. Пусть V 6 Сг и пусть ргеь(у) С ¡31. Тогда V может быть перекрашена в черный цвет (рис. 2.2).

adiM ** sdi(v) *»

Рис. 2.1. Схема, действия правила А.

adiivi /' adi(v)

Рис. 2.2. Схема действия правила В.

Рис. 2.3. Схема действия правила С. На рисунке обозначены множество ребер Bl-Gr(v) (пунктирная стрелка) и подграф SCCV = SCC(v, Bl-Gr{v)).

Для произвольного множества ребер Е' С Е и произвольной вершины v 6 V рассматриваются:

G'(E') — граф, получающийся из G удалением ребер множества Е'\

SCC(v,E') — сильносвязанная компонента графа G'(E'), содержащая вершину v\

Bl-Gr(v) = {(и, v) Е Е : и € В1} — множество ребер, входящих в вершину v, другой конец которых окрашен в черный цвет.

Правило С. Пусть v 6 Gr, и в графе G'(Bl-Gr(v)) не существует пути, ведущего из вершины start в v. Тогда v может быть перекрашена в черный цвет (рис. 2.3).

Пусть Е' — произвольное подмножество ребер, а V' — .произвольное непустое подмножество вершин графа б. Рассмотрим граф С(Е') = (V, Е\Е'). В графе С(Е') существует такая сильносвязанная компонента Я, что выполнены два свойства:

• множество Я О V' не пусто;

• для всех вершин и,у таких, что и е Я\У, а и € ЙП V', в графе С(Е') не существует пути из вершины и в вершину V.

Обозначим такую компоненту через 8СС(У, Е').

Правило Б. Пусть вг -ф 0, Вг-(?г(£г) = [)иеСг В1-Сг(у). Тогда вершины множества 8СС{Сг,В1-Сг(Сг)) П бг могут быть перекрашены в черный цвет (рис. 2.4).

Рис. З.4, Схема действия правила D. На рисунке тржтирнгши стрелками обозначены «черно-серые» ребра Bl-Gr(Gr) = {(2,4), (2,5)}, а таю/ce выделена компонента SC С (Gr, Bl-Gr(Gr)) = {3,4,6,5}.

Базовый алгоритм генерирования инвариантов изображен на рис. 2.5.

С каждым из правил В, С, D связана соответствующая процедура определения инвариантов в перекрашенных в черный цвет вершинах:

G ene rat е-Invar i ant s-В;

Generate-Invariants-C;

Generate-Invariants-D.

Сформулируем некоторые свойства базового алгоритма, изображенного на рис. 2.0, которые используются в далыюпшсм при обосновании его корректности.

Лемма 2.1. Приведенный па схеме алгоритм завершает свою работу за конечное число шагов. По завершении его выполнения все вершины графа будут черными.

( Начало ^

— Generate-Invariants-C (V,SCC(V,вх-or(V)))

а

— Gene rate- Inva riant s - D (Gr, Root-SCCtGr, Bl-Gr(Gr)))

^ Конец ^

Рис. 2.5. Схема алгоритма решения задачи генерирования инвариантов. Определение применимости правил А. В, С, D и выделение соответствующих множеств выполняется

па этапе, обхода графа. Процедуры Generate-Invariants-B, Generate-Invariants-C, Generate-Invariants-D отвечают за определение инвариантов в вершинах, перекрашенных

в черный цвет.

Лемма 2.2. Если при попадании в точку, обозначенную па схеме 2.6 цифрой 2, для вершины v выполнены условия применимости правила В, то любой путь (не обязательно простой) в графе G из вершины start в вершину v имеет вид

start -*...—>■ причем вершина и окрашена в черный цвет.

V,

Лемма 2.3. Если при попадании и точку, обозначенную на схеме 2.6 цифрой 3, для вершины v выполнены условия применимости правила С, то любой путь в графе G из вершины start в вершину v имеет вид

start

-+ и

причем:

• вершина и окрашена в мерный цвет;

• цикл С принадлежит компоненте SCC(v, Bl-Gr(v)).

Лемма 2.4. Если при попадании в точку, обозначенную на схеме 2.6 цифрой 4, выполнены условия применимости правила D (то есть Gr ф 0), то любой путь в графе G из вершины start в любую вершину v Е (Gr Л SCC(Gr, Bl-Gr(Gr))) имеет вид

start. v" —► у' —> ... —> ц,

v

где v' Е Gr, v" Е Bl, а путь L' принадлежит компоненте SCC{Gr,Bl-Gr(Gr)).

В подразделах 2.6.3 определена реализация процедур Generate-Invariants-B, Generate-Invariants-C, Generate-Invariants-D.

Пусть задана программа Р = (Var, Type, Stmt) и ее управляющий граф G(P). Для произвольной вершины v Е V введем следующие обозначения:

• inv[i.'j — формула, выражающая инвариант в точке v\

• /¡.[с] — формула, выражающая априорно (наперед) заданный инвариант в точке v.

Реализация процедуры Generate-Invariants-B. Пусть v — перекрашиваемая вершина, prev(v) = {щ,... ,Uk} — множество предшествующих ей (черных) вершин. Тогда инвариант в точке v определяется следующим образом:

к

inv[v] = (\Jupdate(inv[iij], Stmt[ui\fj Ah[v}. >=i

Реализация процедуры Generate-Invariants-C. Пусть v — перекрашиваемая вершина, prev(v) = {wi,... Щ+i, ■ ■ ■ ,v-k+i} — множество предшествующих соседних вершин, причем вершины щ,..., щ — черные, а вершины Uk+i, ■ ■ ■ > uk+i — белые или серые.

Рассмотрим множество Q — {(?ь... .,qs} переменных, значения которых могут быть изменены в цикле SGC(v,Bl-Gr(v)). Тогда положим:

к

inv0[v] ~ (V update(inv[ui] :_1 , Simtju;])^;

invi [и] I—1 — n.pda,te-va.r(in.VQ M , <?0;

inv 2\v\ =■ update-uar(invi[v] . 92);

invs[v] — update-var(invs-i\

inv[v J — invs[v] A h[v\.

Реализация процедуры Сепега1е-1пуапап1з-В. Пусть Р = Сг П б'СС^Сг, В1-Сг(Сг)) — множество перекрашиваемых в черный цвет вершин. Рассмотрим множество ¿¡) = {^1,.. неременных, значения которых могут быть изменены в цикле 5СС(Сг, В1-Сг(Сг)). Тогда для каждого у £ Р т положим:

тг>оМ

гт\ [и] ту г [У]

шг>.,[г>] - ирс^е-тг^пг^-!^], д.,);

¿™[г>] = тиДи] Л Л [г;].

В таких условиях оказывается возможным сформулировать и доказать теорему о корректности алгоритма генерирования инвариантов. Таким образом, свойство корректности алгоритма верификации 1АЬ-программ, а вместе с ним — свойство полноты алгоритма обнаружения программных дефектов в С-нрограммах, будет формально обосновано.

Теорема 2.13 Алгоритм генерирования инвариантов является корректным.

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

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

1. Формирование некоторого количества «пробных» инвариантов (гипотез) в различных вершинах управляющего графа.

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

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

= ^ ирйаЬе^пуЩ, й^т^и])^;

(и,у)еВ1-вт(Р)

= ирсЫе-ь'аг(тго[у], 91); = ирйаЬе-ьаг{ту\Щ, <72);

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

Пусть проверяемая в точке V гипотеза (полученная каким-либо способом) имеет вид формулы <р. Рассмотрим лишь случай, когда при применении алгоритма генерирования инвариантов вершина и перекрашивается в черный цвет по правилу С. Таким образом, вершина у является «входом» в цикл БСС,, —

БСС(у, В1-Сг(у)).

Проверка гипотезы осуществляется по принципу индукции. На первом шаге проверяется, что «начальные» значения переменных при входе в цикл БССУ удо-аяетворнют формуле </;. Для достижения данной цели построим вспомогательную формулу:

т1\)[г>] = ^ ирс1а1е(ту[и], Л Н{у\.

Для проверки базы индукции достаточно исследовать выполнимость формулы (гпг'оМл-1^). Если указанная формула является невыполнимой, то базу индукции будем считать доказанной.

На втором шаге осуществляется проверка индуктивного перехода, для чего строится вспомогательный управляющий граф, состоящий из вершин множества 5СС,. и новой вершины у' (рис. 2.6). Все ребра, компоненты ЗСС(у,В1-Сг(у)) сохраняются, за исключением ребер, входящих в вершину V. Каждое ребро указанной компоненты вида (ю,1>) заменяется новым ребром («;,?/).

Рис. 2.6. Построение вспомогательного управляющего графа.

В построенном графе начальной объявляется вершина V, а конечной — вершина г/. Инструкции, приписанные вершинам ЗСС„ нового управляющего графа, остаются прежними.

Рассмотрим задачу анализа новой программы. Априорно заданные инварианты в каждой вершине сохраняются, однако в вершине V наперед задается инвариант ф. Задача анализа программы будет заключаться в проверке истинности формулы ¡р в точке и'.

Если можно гарантировать истинность формулы <р в вершине г/, то индуктивную пшоте;з.у будем считать доказанной.

В третьей главе рассматриваются аспекты программной реализации средства автоматизированного обнаружения дефектов в программах на языке С. Основным объектом исследования является программное средство «Статический анализатор программных дефектов» (далее — просто «Анализатор»).

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

1. Метод должен гарантировать обнаружение всех дефектов.

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

• месторасположение «подозрительной» точки кода;

• тип возможного дефекта;

• условия, при которых возможно возникновение ошибки.

3. Метод должен быть применим для анализа, крупных программных комплексов, содержащих до 500 тысяч строк кода.

4. Метод должен быть по-возможности наиболее эффективным. Критериями эффективности являются:

• время работы;

• количество ложных срабатываний на строку кода;

• способность находить реальные дефекты в программах.

Схематично процедура статического анализа исходного кода С-программ и выявления потенциальных уязвимостей представлена па рис. 3.1. В ней можно выделить следующие этапы:

• этап лексического и синтаксического анализа;

• этап, осуществляющий трансляцию абстрактного синтаксического дерева. в промежуточное представление, называемое IAL-представлением (от Intermediate Analyser Language);

s этап анализа программы в виде промежуточного представления.

Рассмотрим задачи,; которые решаются на каждом из указанных этапов.

Лексический и синтаксический анализ представляет собой процесс сопоставления линейной последовательности символов программы с формальной грамматикой языка С (согласно стандарта ISO./IEC 9899:1999 «Programming

' Исходный/ код Г

Лексический и синтаксический анализ

Абстрактное синтаксическое дерево

Отчет об уязвимостях

Анализ IAL программы

Трансляция в промежуточное представление

IAL программа

Рис. 3.1. Этапы статического анализа программы: лексичехкй и синтаксический анализ, трансляция в промежуттное предстплвлеиие, анализ ¡АЬ-програмлт.

Languages — С»), Результатом является дерево разбора или абстрактное синтаксическое дерево.

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

Этап трансляции абстрактного синтаксического дерева в IAL-программу носит, в основном, рутинный характер. К преобразованиям, выполняемым на данном этапе, относятся:

• устранение неявных преобразований типов в соответствии с правилами стандарта С99;

е разворачивание сложных выражений (преобразование сложных выражений в последовательность простых с использованием временных переменных);

• вычисление и подстановка константных выражений (включая выражения, содержащие операторы sizeof);

• разворачивание структур управления, таких как циклы и условные выражения;

• разворачивание вызовов функций.

Анализ программы на языке промежуточного представления. Анализ IAL-программы является главным этапом разрабатываемого метода. Основными задачами, которые решаются на данном этапе, являются: проведение статического анализа программы; выявление свойств программы, связывающих значения пере-

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

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

В четвертой, главе исследуется эффективность разработанного программного комплекса для автоматизированного обнаружения программных дефектов. Объектом исследования является программное средство «Статический анализатор программных дефектов» (далее — просто «Анализатор»), Примеры, на которых производится тестирование «Анализатора», разделены на две группы, к которым относятся модельные примеры и реальные приложения.

Под модельным примером будем понимать пару небольших программ на языке С, одна из которых содержит некоторую разновидность программного дефекта, а. в другой этот дефект устранен. Каждый модельный пример ориентирован па тестирование определенной функциональной возможности «Анализатора». В разделе 4.1 рассматриваются модельные примеры stack-overflow, heap-overflow,направленные, соответственно, на определение возможности выявления переполнения буфера в стеке, переполнение буфера в куче.

В разделе 4.2 диссертационной работы исследуется применение «Анализатора» к программе xorg-server (основной части графической подсистемы X.Org). Программа xorg-server выбрана в качестве примера для исследования и демонстрации масштабируемости разработанного прототипа. Ее исходный код содержит 552 модуля с исходным кодом, что составляет около 470 тыс. строк кода.

Далее рассматриваются следующие величины:

• LOC (от Lines Of Code) — количество строк кода в исследуемой программе на языке С;

• PVL (от Potentially Vulnerable Locations) — количество потенциально уязвимых участков кода;

• WRN (от WaRNings) — количество выданных предупреждений;

• TP (от True Positives) — количество реальных дефектов, обнаруженных «Анализатором»;

в FP (от False Positives) — количество ложных срабатываний «Анализатора».

Для оценки эффективности применения «Анализатора» к программе xorg-server введем две дополнительные величины, а именно — плотность ложных срабатываний (DFP) и эффективность верификации (EFV).

Определение 4.1. Под плотностью ложных срабатываний будем понимать относительную величину

FP

DFP = — • 1000.

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

Определение 4.2. Под эффективностью верификациг1 будем понимать относительную величину

РУЬ-РР ЕРУ = 'Ш%■

гуЬ

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

Полный синтаксический разбор исходного кода хо^-Бегуег и преобразование абстрактного синтаксического дерева в промежуточное представление заняло около 80 минут. Всего в исходном коде программы присутствовало 29310 потенциально уязвимых участков, 4058 из которых были в результате анализа отмечены, как возможные дефекты. Для остальных 25252 участков «Анализатором» была доказана их корректность. В следующих таблицах представлены результаты проведенного эксперимента:

№ ит. ЮС РУЬ IV ЯМ ТР РР : ОРР ЯРУ

.. 1 469537 29310 4 573 ТР, > 0 РР) < 4573 ОРР, < 9.74 РРЦ > 84.40%

. 2 469537 29310 4058 ТРЪ > 0 РР3 < 4058 ПРР2 < 8.64 ЕРУ2 > 86.16%

3 469537 29310 4058 ТРз > 0 РРз < 4058 £>РР3 < 8.64 ЕР\'Ъ > 86.16%

Таблица 4.1. 'Результат анализа программы хогд-ветиег. Функциональные характеристики.

№ ит. Время, мин. Память, МБ

1 315 1819

2 324 1830

3 324 1832

Таблица 4-3- Результат анализа программы хогд-зегиег. Показатели ресурсоемкости.

Замечание. В связи с тем, что ручной анализ кода программы хо^-эегуег в данной работе не проводился (по причине большого объема исследуемого кода), точные значения величин ТР, РР, а следовательно, и БРР, и ЕРУ на итерациях 1, 2, 3 неизвестны. По этой причине для величин ТР и РР используются лишь их оценки 0 < ТР, РР < \VFtN. Исходя из этих неравенств, а также принимая во внимание тождество ТР + РР — \VR.N, получаются оценки для величин ОРР, ЕРУ. Указанные оценки для величин ТР, РР, ОРР, ЕРУ на каждой из трех проведенных итераций представлены в таблице 4.1 вместо точных значений.

Во втором эксперименте автором было преднамеренно внесено два реальных дефекта в исходный код программы хо^-вегуег. Операции, корректность которых ранее была доказана «Анализатором», были заменены на некорректные.

Затем проект был повторно исследован «Анализатором». Как видно из результатов эксперимента (табл. 4.3, 4.4), заключительный отчет об уязвимостях содержит ровно на 2 предупреждения больше, чем в предыдущем эксперименте, причем обе некорректные операции были успешно обнаружены. Результаты эксперимента свидетельствуют о возможности «Анализатора» находить реальные уязвимости, в том числе, при анализе больших программ.

№ ut. LOG PVL WRN TP FP DFP EFV

1 469537 29310 4576 TPy >2 FPi < 4574 DFPX < 9.74 EFV! > 84.40%

2 460537 29 310 4060 TP2 > 2 FP2 < 4058 DFP2 < 8.64 EFV2 > 86.16%

3 469537 29310 4060 TP3>2 FP3 < 4058 DFP;i < 8.64 EFV3 > 86.16%

Таблииа ^.S. Результат анализа модифицированной програмлш. xorg-server. Функциональные характеристики.

№ ит. Время, мин. Память, МБ

1 315 1819

2 324 1830

3 324 1832

Таблица 4-4- Результат анализа модифицированной программы xorg-server. Показатели

pecypcoeJUKOctnu.

Результаты проведенных экспериментов позволяют сделать следующие выводы.

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

Проведенные эксперименты свидетельствуют о применимости на практике разработанного прототипа для анализа крупных программных проектов: время анализа всего проекта является приемлемым (не превышает 20 часов); плотность количества ложных срабатываний не превышает 10 (на 1000 строк исходного кода); эффективность верификации составила около 86%. Отметим, что в известных а,втору аналогах «Анализатора» по функциональному значению эффективность верификации достигала лишь 52%.19

"Elloiibogen R. Fully Automatic Vérification of Absence of Errors via Interprocedural Integer Analysis. Master's thesis, School of Computer Science, Te!-Aviv University, Tel-Aviv, Israel, December 2004.

В заключении перечислены основные результаты диссертационной работы.

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

2. Предложен метод автоматизированного обнаружения дефектов в программах на языке С, основанный на преобразовании исходной программы в промежуточный формат «IAL» (от Intermediate Analyser Language) с последующей верификацией полученной IAL-программы.

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

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

5. Создан прототип программного комплекса автоматизированного обнарул«-пия дефектов в программах на языке С, эффективность которого продемонстрирована как на. ряде специально подобранных модельных примеров, так и па примере программы xorg-server — основной части подсистемы управления графикой в UNIX-подобных операционных системах.

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

Список литературы

[lj Галатепко А. В., Пучков Ф. М., Шапченко К. А. Способ анализа программ на наличие угроз переполнения буферов // Информационная безопасность регионов России (ИБРР-2003): Материалы конференции. — Санкт-Петербург, 2003. — С. 33. (Ф. М. Пучкову принадлежат результаты но описанию метода статического анализа блок-схем).

[2] Пучков Ф. М., Шапченко К. А. К вопросу о выявлении возможных переполнений буферов посредством статического анализа исходного кода программ. // Материалы конференции МаБИТ-04. — М.: МЦНМО, 2005. —

С. 347-359. (Ф. М. Пучкову принадлежат результаты по описанию метода статического анализа блок-схем).

|3] Пучков Ф. М., Шапчсико К. А. Статический метод анализа программного обеспечения на наличие угроз переполнения буферов. // Программирование.

— 2005. — N.4. — С. 19-34. (Ф. М. Пучкову принадлежат результаты по описанию математической модели и алгоритмов статического анализа блок-схем, доказательствам основных утверждений).

[4] Puchkov, F., Shapchenko, К. Static Analysis Method for Detecting Buffer Overflow Vulnerabilities // Programming and Computer Software, Volume 31, Number 4, July 2005, pp. 179-189(11).

[5] Пучков Ф. M., К. А. Шапченко, О. О. Андреев. К созданию автоматизированных средств верификации программного кода. // Материалы Второй международной научной конференции по проблемам безопасности и противодействия терроризму. Пятая общероссийская научная конференция «Математика и безопасность информационных технологий» (МаБИТ-06). МГУ имени М.В. Ломоносова, 25-26 октября 2006 г. - М.: МЦНМО, 2007. -С. 401-439. (Ф. М. Пучкову принадлежат результаты систематизации рассматриваемой предметной области, в том числе классификации существующих уязвимостей программного обеспечения; исследования и анализа существующих подходов к верификации программного обеспечения; описания метода трансляции дерева разбора С-программы в блок-схему; описания метода статического анализа блок-схемы и проверки условий корректности).

[6| Пучков Ф. М. Средства аудита программного обеспечения на предмет обнаружения уязвим,остей. // Критически важные объекты и кибертерро-ризм. Часть 2. Аспекты программной реализации средств противодействия. / О. О. Андреев и др. Под ред. В. А. Васешша. - М.: МЦНМО, 2008, 607 с.

- С. 375-455.

[7] Способ генерации баз данных для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Пучков Ф. М., Шапченко К. А. // Патент на изобретение № 2364929. - 2009.

[8] Способ генерации баз знаний для систем, верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Пучков Ф. М., Шапченко К. А. // Патент па изобретение .V« 2364930. - 2009.

[9] Способ генерации баз данных и баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и

устройство для его реализации. / Пучков Ф. М., Шапчепко К. А. // Патент на изобретение № 2373569. - 2009.

¡10] Способ верификации программного обеспечения распределенных вычислительных комплексов и система для его рехьшзации. / Пучков Ф. М., Шап-ченко К, А. // Патент на изобретение № 2373570. — 2009.

Отпечатано в копицентре « СТ ПРИНТ » Москва, Ленинские горы, МГУ, 1 Гуманитарный корпус, e-mail: globus9393338@yandex.ru тел.: 939-33-38 Тираж 100 экз. Подписано в печать 24.02.2010 г.

Список обозначений

Введение

1 Автоматизированное обнаружение уязвимостей в программах на языке С

1.1 Типы существующих программных дефектов.

1.1.1 Некорректные операции с памятью.

1.1.2 Некорректные операции с целыми типами.

1.1.3 Операции чтения неопределенного значения.

1.1.4 Некорректное использование функций стандартной библиотеки

1.1.5 Утечки памяти

1.2 Методы и средства обнаружения программных дефектов.

1.2.1 Методы лексического и синтаксического анализа.

1.2.2 Программный комплекс Splint.

1.2.3 Программный комплекс BOON.

1.2.4 Метод абстрактной интерпретации программ.

1.3 Выводы.

2 Метод обнаружения дефектов в программах на языке С

2.1 Введение.

2.2 Общий подход к решению задачи обнаружения дефектов в программах на языке С

2.2.1 Лексический и синтаксический анализ С-программы.

2.2.2 Преобразование,дерева разбора в промежуточное представление.

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

2.3 Описание языка IAL.

2.3.1 Синтаксическая структура IAL-программы.

2.3.2 Типы данных.

2.3.3 Константы.

2.3.4 Инструкции.

2.4 Математическая модель языка IAL.

2.5 Инварианты IAL-программы.

2.6 Базовый алгоритм генерирования инвариантов.

2.6.1 Алгоритм обхода управляющего графа.

2.6.2 Свойства систем интервальных уравнений.

2.6.3 Определение инвариантов в вершинах.

2.6.4 Теорема о корректности алгоритма генерирования инвариантов

2.7 Построение и проверка индуктивных гипотез.

2.8 Выводы.

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

3.1 Требования к программному комплексу.

3.2 Основные этапы метода автоматизированного обнаружения уязвимостей.

3.2.1 Лексический и синтаксический анализ С программы.

3.2.2 Трансляция абстрактного синтаксического дерева в промежуточное представление . 96

3.2.3 Верификация IAL-программы.

3.3 Выводы.

4 Исследование эффективности средства автоматизированного обнаружения уязвимостей в программах на языке С

4.1 Модельные примеры.

4.1.1 Модельный пример stack-overflow.

4.1.2 Модельный пример heap-overflow.

4.2 Анализ программы xorg-server.

4.3 Выводы.•.

Актуальность

Одним из важнейших условий успешного функционирования практически значимых объектов, потенциально уязвимых для кибератак, является защита используемого в их составе программного обеспечения от возможных сбоев в работе. Это условие становится особенно важным при проектировании автоматизированных систем с высоким уровнем требований к их защищенности, в том числе — при разработке и реализации программно-технических средств защиты информации, что отражено в соответствующих Руководящих документах ФСТЭК РФ [1-3]. Появление подобных сбоев зачастую связано с наличием уязвимостей (ошибок, дефектов) в программных средствах подобных систем. В их числе такие, использование которых злоумышленником может привести к нерегламентированному политикой информационной безопасности повышению его привилегий на том или ином узле системы, подлежащей защите. Кроме того, сбои в работе программ могут приводить к аварийному завершению работы важных программно-аппаратных компонентов, создавая угрозу отказа для системы в целом. Имея в виду существующие подходы к разработке и последующему сопровождению программного обеспечения [12-14,35,37,44,55], в частности, на основе уже существующих средств с открытым исходным кодом, на первый план выходят следующие задачи:

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

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

• обоснование отсутствия других уязвимостей (дефектов) в используемом программном обеспечении.

Актуальность выбора для анализа именно программ, написанных с использованием языка программирования С, обусловлена широкой распространенностью этого языка в среде программного обеспечения с открытым исходным кодом. Согласно проведенным исследованиям [63,64], на долю языка С приходится более 80% объема кода, используемого в современных программных средствах. Дополнительным фактором такого выбора является и то обстоятельство, что обеспечение корректности операций с памятью и указателями в языке С является задачей разработчика программного обеспечения.

Следует отметить, что в настоящее время эффективных и широко распространенных автоматизированных средств, позволяющих проверять корректность программ на языке С и выявлять в них возможные уязвимости, не существует. Традиционные средства статического анализа (аудита) исходного кода недостаточно точно анализируют семантику программы, и, как следствие, — приводят к большому количеству ложных предупреждений. Например, программный комплекс ITS4 [36, 74] анализирует лишь наборы лексем, сопоставляя их с образцами «потенциально опасных конструкций», хранящимися в специальной базе данных. Подобный алгоритм проверки может выдавать до 100% ложных предупреждений, не обнаружив при этом в исследуемой программе ни одной реальной уязвимости. Программный комплекс Splint [47,76] позволяет находить лишь простейшие уязвимости такие, как, например, выход за границу статического массива при обращении по фиксированному индексу. Для обнаружения уязвимостей в более сложных ситуациях анализатору необходимо предоставить специальные аннотации, составление которых представляется весьма трудоемкой процедурой. Программный комплекс BOON [58,67] реализует один из простейших вариантов «интервального анализа» — для каждой целочисленной пер'еменной х вычисляется интервал [а, 6] ее возможных значений такой, что в каждой точке программы справедливо соотношение а < х < Ь. К недостаткам алгоритма можно отнести следующие факторы, значительно снижающие точность анализа.

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

• Отсутствует анализ указателей.

• Не исследуются зависимости между различными переменными.

На рынке информационных технологий представлен также ряд коммерческих продуктов (Coverity [70], PolySpace [75]), позволяющих (по мнению их разработчиков) проводить более точный анализ исходного кода 'программ. Однако, результаты использования указанных продуктов, а также применяемые методы и алгоритмы не были опубликованы.

Программный комплекс ASTREE [65] позволяет верифицировать программы на языке С, не содержащие операций динамического выделения/освобождения памяти, а также не использующие рекурсию.

Средства динамического анализа, применяемые непосредственно во время работы исследуемой программы (например, Valgrind [49,77]), могут быть весьма эффективными для обнаружения «ошибок времени выполнения» (runtime errors). Однако, во-первых, они существенно замедляют работу программы, а во-вторых, указанные средства проверяют корректность выполнения программы лишь на конечном множестве наборов входных данных (тестов) и не могут гарантировать корректность работы исследуемой программы в процессе ее дальнейшей эксплуатации. По этой причине, методы динамического анализа не являются полноценной заменой статическим методам аудита исходного кода С-программ.

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

Цель работы

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

Основные результаты работы

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

1) систематизирована исследуемая предметная область, введено понятие программного дефекта, предложена классификация существующих программных дефектов С-программ;

2) предложен метод автоматизированного обнаружения дефектов в программах на языке С, основанный на преобразовании исходной программы в промежуточный формат «IAL» (от Intermediate Analyser Language) с последующей верификацией полученной IAL-программы;

3) разработан язык IAL промежуточного представления С-программ, описаны его синтаксис и семантика, разработана математическая модель языка IAL, в рамках которой формализована задача верификации IAL-программ;

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

5) создан прототип программного комплекса автоматизированного обнаружения дефектов в программах на языке С, эффективность которого продемонстрирована как на ряде специально подобранных модельных примеров, так и на примере программы xorg-server — основной части подсистемы управления графикой в UNIX-подобных операционных системах.

Методы исследования

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

Научная новизна

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

Практическая значимость

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

Апробация работы

Основные результаты диссертации докладывались на международной научной конференции «Информационная безопасность регионов России (ИБРР-2003)», на международных конференциях «Математика и безопасность информационных технологий» (2004-2006), «Ломоносовские чтения» (2006-2007), на механико-математическом факультете МГУ имени М.В. Ломоносова на семинаре «Проблемы современных информационно-вычислительных систем» под руководством д.ф.-м.н., проф. В.А. Васенина <2004, 2009).

Публикации

По теме диссертации опубликовано 10 научных работ, в том числе в зарубежных журналах, из них одна статья [24] в журнале из перечня ВАК ведущих рецензируемых журналов, а также — 4 патента на изобретения [29-32]. Материалы работы вошли в главу 7 опубликованной в 2008 году книги «Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия» под ред. д.ф.-м.н., проф. В.А. Васенина [27].

Структура и объем диссертации

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

4.3 Выводы

Настоящая глава посвящена исследованию эффективности (тестированию) созданного прототипа программного комплекса. Тестирование проводилось на ряде модельных примеров, представляющих собой специально подготовленных программы небольшого размера, а также на примере крупной программы xorg-server, содержащей около 470 тыс. строк кода, представляющей собой основную часть подсистемы управления графикой в UNIX-подобных операционных системах.

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

Проведенные эксперименты с программной xorg-server свидетельствуют о применимости на практике разработанного прототипа для анализа крупных программных проектов: время анализа всего проекта является приемлемым (не превышает 20 часов), плотность количества ложных срабатываний не превышает 10 на 1000 строк исходного кода, а эффективность верификации составила около 86%. Отметим, что эффективность верификации существующих известных автору средств аудита исходного кода программ на языке С не превышает 52%.

Заключение

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

1) систематизирована исследуемая предметная область, введено понятие программного дефекта, предложена классификация существующих программных дефектов С-программ;

2) предложен метод автоматизированного обнаружения дефектов в программах на языке С, основанный на преобразовании исходной программы в промежуточный формат «IAL» (от Intermediate Analyser Language) с последующей верификацией полученной IAL-программы;

3) разработан язык IAL промежуточного представления С-программ, описаны его синтаксис и семантика, разработана математическая модель языка IAL, в рамках которой формализована задача верификации IAL-программ;

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

5) создан прототип программного комплекса автоматизированного обнаружения дефектов в программах на языке С, эффективность которого продемонстрирована как на ряде специально подобранных модельных примеров, так и на примере программы xorg-server — основной части подсистемы управления графикой в UNIX-подобных операционных системах.

1. Нормативные документы

2. Защита от несанкционированного доступа к информации. Термины и определения. // Руководящий документ. Гостехкомиссия России, 1992.

3. Средства вычислительной техники. Защита от несанкционированного доступа к информации. Показатели защищенности от несанкционированного доступа к информации. // Руководящий документ. Гостехкомиссия России, 1992.

4. Научно-техническая литература

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

6. Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 1. Начала теории множеств. — М.: МЦНМО, 2002. — 128 с.

7. Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. — М.: МЦНМО, 2002. — 288 с.

8. Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. — М.: МЦНМО, 2002. — 192 с.

9. Вирт Н. Алгоритмы и структуры данных. — М.: Мир, 1989. — 360 с.

10. Гайсарян С. С., Чернов А. В., Белеванцев А. А., Маликов О. Р., Мельник Д. М., Меньшикова А. В. О некоторых задачах анализа и трансформации программ. // Труды ИСП РАН, 2005. 78 с.

11. Галатенко А. В., Пучков Ф. М., Шапченко К. А. Способ анализа программ на наличие угроз переполнения буферов. // Материалы конференции «Информационная безопасность регионов России» (ИБРР-2003). — СПб.: 2003. С. 33.

12. Кормен Т., Лейзерсон Ч., Ривест Р., Штайн К. Алгоритмы: построение и анализ. Второе издание. — М.: Издательский дом «Вильяме», 2005. — 1296 с.

13. Липаев В. В. Методы обеспечения качества крупномасштабных программных средств. — М.: Синтег, 2003. — 520 с.

14. Липаев В. В. Программная иноюенерия. Методологические основы. — М.: Теис, 2006. — 608 с.

15. Липаев В. В. Процессы и стандарты жизненного цикла сложных программных средств. Справочник. — М.: Синтег, 2006. — 276 с.

16. Мак-Клар С., Скембрей Дж., Курц Дж. Секреты хакеров. Безопасность сетей — готовые решения, 3-е издание. — М.: Издательский дом «Вильяме», 2002. — 736 с.

17. Маликов О. Р. Автоматическое обнаружение уязвимостей в исходном коде программ. // Известия ТРТУ №4, 2005. С. 48-53.

18. Маликов О. Р., Несов В. С. Автоматический поиск уязвимостей в больших программах. // Известия ТРТУ, Тематический выпуск «Информационная безопасность», №7, 2006. — С. 114-120.

19. Маликов О. Р. Исследование и разработка методики автоматического обнаружения уязвимостей в исходном коде программ на языке Си. // Дис. . канд. физ.-мат. наук: 05.13.11. — М.: 2006. 101 с.

20. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С-программ. Часть 1. Язык C-light. // Препр./ РАН. Сиб. Отд-ние. ИСИ; №84, 2001.

21. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С-программ. Часть 2. Язык C-light-kemel и его аксиоматическая семантика. // Препр./ РАН. Сиб. Отд-ние. ИСИ; №87, 2001.

22. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С-программ. Язык CLlight и его формальная семантика. // Программирование, №6, 2002. С. 65-80.

23. Несов В. С., Маликов О. Р. Использование информации о линейных зависимостях для обнаружения уязвимостей в исходном коде программ. // Труды ИСП РАН №9, 2006. — С. 51-57.

24. Промский А. В. Формальная• семантика C-light программ и их верификация методом Хоара. // Дис. . канд. физ.-мат. наук: 05.13.11 / ИСИ СО РАН. — Новосибирск, 2004. — 158 с.

25. Пучков Ф. М., Шапченко К. А. Статический метод анализа программного обеспечения на наличие угроз переполнения буферов. // Программирование №4, 2005. — С. 19-34.

26. Пучков Ф. М., Шапченко К. А. К вопросу о выявлении возможных переполнений буферов посредством статического анализа исходного кода программ. // Материалы конференции МаБИТ-04. М.: МЦНМО, 2005. - С. 347-359.

27. Пучков Ф. М., Шапченко К. А., Андреев О. О. К созданию автоматизированных средств верификации программного кода. // Материалы конференции МаБИТ-06. — М.: МЦНМО, 2007. С. 401-439.

28. Юдин Д. В., Гольштейн Е. Г. Линейное программирование. Теория, методы и приложения. — М.: Государственное издательство физико-математической литературы, 1969. — 424 с.1. Патенты

29. Пучков Ф. М., Шапченко К. А. Способ генерации баз данных для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. // Патент на изобретение №2364929. — 2009.

30. Пучков Ф. М., Шапченко К. А. Способ генерации баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. // Патент на изобретение №2364930. — 2009.

31. Пучков Ф. М., Шапченко К. А. Способ генерации баз данных и баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. // Патент на изобретение №2373569. — 2009.

32. Пучков Ф. М., Шапченко К. А. Способ верификации программного обеспечения распределенных вычислительных комплексов и система для его реализации. // Патент на изобретение №2373570. — 2009.

33. Зарубежные нормативные документы

34. ISO/IEC 10967-1:1994 International Standard. Information Technology — Language Independent Arithmetic — Part 1: integer and floating point arithmetic.

35. ISO/IEC 9899:1999 International Standard. Programming languages — C.

36. Зарубежная научно-техническая литература

37. Beck К. Extreme Programming Explained: Embrace Change. // Addison Wesley Professional, November 2004.

38. Bloch J. Т., Kohno Т., McGraw G., Viega J. ITS4: A Static Vulnerability Scanner for С and С++ Code. // Annual Computer Security Applications Conference, December 11-15, 2000, pp. 257-267.

39. Boehm B. A Spiral Model of Software Development and Enhancement. // TRW Defense Systems Group. — COMPUTER Journal, May 1988, pp. 61-72.

40. Cooper D. C. Theorem Proving in Arithmetic without Multiplication. // Machine Intelligence №, 1972, pp. 91-99.

41. Cousot P., Cousot R. Abstract Interpretation: A Uniffied Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints //In Proc. POPL'77, P. 238-252. ACM Press, 1977.

42. Dor N., Rodeh M., Sagiv M. CSSV: Towards a Realistic Tool for Statically Detection All Buffer Overflows in C. // Proceedings of the ACM SIGPLAN 2003 conference, San Diego, California, USA, 2003, pp. 155-167.

43. Ellenbogen R. Fully Automatic Verification of Absence of Errors via Interprocedural Integer Analysis. Master's thesis, School of Computer Science, Tel-Aviv University, Tel-Aviv, Israel, December 2004.

44. Floyd R. W. Assigning meanings to Programs. // Proc. Symposium in Appl. Math. Vol. 19. Mathematical Aspects of Computer Science. AMS, Providence, P. 19-32., 1967.

45. Fogel K. Producing Open Source Software. — O'Reilly, October 2005.

46. Ganesh V. Decision Procedures for Bit-Vectors, Arrays and Integers. // PhD Dissertation, Department of Computer Science, Stanford University, September 2007, p. 125.

47. Kaluzny B. L. Polyhedral computation: A Survey of Projection Methods. // School of Computer Science, McGill University. "April, 2002.

48. Larochelle D., Evans D. Statically Detecting Likely Buffer Overflow Vulnerabilities. // Proceedings of the 10th USENIX Security Symposium, Washington, D. C., August 13-17, 2001.

49. Nethercote N., Fitzhardinge J. Bounds-Checking Entire Programs without Recompiling. // Informal Proceedings of the SPACE 2004, Venice, Italy, January 2004, p. 12.

50. Nethercote N., Seward J. Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation. // Proceedings of the 2007 PLDI conference. ACM SIGPLAN Notices. Volume 42, Issue 6, June 2007, pp. 89-100.

51. Nielson F., Nielson H. R., Hankin C. Principles of Program Analysis. Springer Berlin Heidelberg New York. 1st edition 1999. Corrected 2nd printing 2005.

52. Norrish M. С Formalized in HOL // PhD Dissertation, Computer Laboratory, University of Cambridge 1998.

53. Plotkin G. A Structural Approach to Operational Semantics. Tech. Rep. DAIMI FN-19, Computer Science Department, University of Aarhus, Denmark, 1981.

54. Puchkov F., Shapchenko K. Static Analysis Method for Detecting Buffer Overflow Vulnerabilities // Programming and Computer Software, Volume 31, Issue 4, July 2005, pp. 179-189.

55. Royce W. Managing the Development of Large Software Systems: Concepts and Techniques. // Technical Papers of Western Electronic Show and Convention, Los Angeles, USA, 1970, pp. 328-338.

56. Sankaranarayanan Sriram.' Mathematical Analysis of Programs // PhD Dissertation, Department of Computer Science, Stanford University, September 2005, p. 163.

57. Shacham H., Page M., Pfaff В., Goh E.-J., Modadugu N., Boneh D. On the Effectiveness of Address-Space Randomization // CCS'04, October 25-29, 2004, Washington, DC, USA.

58. Wagner D., Foster J., Brewer E., Aiken A. A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. // Proceedings of the 2000 Network and Distributed'Systems Security Conference, February 2000, pp. 423-460.

59. Zitser M. Securing Software: An Evaluation of Static Source Code Analyzers. // MSc thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute" of Technology, August, 2003, p. 130.

60. Ссылки на Интернет-ресурсы

61. Aleph One. Smashing the stack for fun and profit. // Phrack Magazine, 49(14), Nov. 1996. Электронный ресурс]. Режим доступа: http://www.phrack.org/phrack/49/P49-14, свободный. — Электрон, текст, док.

62. Drepper U. Security Enhancements in Red Hat Enterprise Linux (beside SELinux). // Red Hat, Inc., December 9, 2005. Электронный ресурс]. Режим доступа: http://people .redhat. com/drepper/nonselsec. pdf, свободный. — Электрон, текст, док.

63. Lea D. A Memory Allocator. Электронный ресурс]. Режим доступа: http://gee.cs. oswego.edu/dl/html/malloc.html, свободный. — Электрон, текст, док.

64. Measuring Libre Software Using Debian 3.1 (Sarge) as A Case Study: Preliminary Results. Электронный ресурс]. Режим доступа: http://www.upgrade-cepis.Org/issues/2005/3/ up6-3Amor.pdf, свободный. — Электрон, текст, док.

65. Wheeler D. More Than a Gigabuck: Estimating GNU/Linux's Size. Электронный ресурс]. Режим доступа: http://www.dwheeler.com/sloc/redhat71-vl/redhat71sloc.html, свободный. — Электрон, текст, док.

66. The ASTREE Static Analyzer. Электронный ресурс]. Режим доступа: http: //www. astree. ens. fг/, свободный.

67. Bison — GNU Parser Generator. Электронный ресурс]. Режим доступа: http://www.gnu. org/software/bison/, свободный.

68. BOON — Buffer Overrun detectiON. Электронный ресурс]. Режим доступа: http://www. eecs.berkley.edu/~daw/boon/,свободный.

69. Common Vulnerabilities and Exposures. Электронный ресурс]. Режим доступа: http: //www. cve.mitre.org, свободный.

70. Computer Emergency Response Team. Электронный ресурс]. Режим доступа: http://www. kb.cert.org/vuls/, свободный.

71. Coverity. Электронный ресурс]. Режим доступа: http://www.coverity.com/, свободный.

72. Flawfinder. Электронный ресурс]. Режим доступа: http://www.dweeler.com/ flawfinder/, свободный.

73. The GNU Grep. Электронный ресурс]. Режим доступа: http://www.gnu.org/software/ grep/, свободный.

74. The GNU Compiler Collection. Электронный ресурс]. Режим доступа: http://gcc.gnu. org/, свободный.

75. ITS4: Software Security Tool. Электронный ресурс]. Режим доступа: http: //www. cigital. com/its4/, свободный.

76. Poly Space Embedded Software Verification. Электронный ресурс]. Режим доступа: http: //www.mathworks.com/products/polyspace/,свободный.

77. Splint — Secure Programming Lint. Электронный ресурс]. Режим доступа: http://www. splint. org, свободный.

78. Valgrind. Электронный ресурс]. Режим доступа: http://www.valgrind.org, свободный.