Сборники трудов ИСП РАН


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

Федотов А.Н. (ИСП РАН, Москва, Россия)
Каушан В.В. (ИСП РАН, Москва, Россия)
Гайсарян С.С. (ИСП РАН, Москва, Россия; МГУ, Москва, Россия; МФТИ, Московская. обл., Россия; ВШЭ, Москва, Россия)
Курмангалеев Ш.Ф. (ИСП РАН, Москва, Россия)

Аннотация

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

Ключевые слова

ошибки; символьное выполнение; предикат безопасности; анализ бинарного кода; динамический анализ

Издание

Труды Института системного программирования РАН, том 29, вып. 6, 2017, стр. 151-162.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(6)-8

Полный текст статьи в формате pdf Вернуться к содержанию тома