Preview

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

Расширенный поиск

Поиск ошибок доступа к буферу в программах на языке C/C++

https://doi.org/10.15514/ISPRAS-2016-28(4)-9

Полный текст:

Аннотация

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

Об авторах

И. А. Дудина
Институт системного программирования РАН; Московский государственный университет имени М.В. Ломоносова
Россия


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


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


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

1. CVE and CCE Statistics Query Page. https://web.nvd.nist.gov/view/vuln/statistics

2. A. One, "Smashing the Stack for Fun and Profit", Phrack Magazine, Volume 7, Issue 49, November 1996.

3. D. Larochelle, D. Evans. Statically detecting likely buffer overflow vulnerabilities. 10th USENIX Security Symposium, Washington, D.C., August 2001.

4. В.П. Иванников, А.А. Белеванцев, А.Е. Бородин, В.Н. Игнатьев, Д.М. Журихин, А.И. Аветисян, М.И. Леонов. Статический анализатор Svace для поиска дефектов в исходном коде программ Труды ИСП РАН,, том 26, 2014 г. стр 231–250. DOI: 10.15514/ISPRAS-2014-26(1)-7.

5. V. Kuznetsov, J. Kinder, S. Bucur, and G. Candea. 2012. Efficient state merging in symbolic execution. SIGPLAN Not. 47, 6 (June 2012), 193-204. DOI=http://dx.doi.org/10.1145/2345156.2254088

6. В.К. Кошелев, И.А. Дудина, В.И. Игнатьев, А.И. Борзилов. Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 59-86. DOI: 10.15514/ISPRAS-2015-27(5)-5.

7. А.Е. Бородин, А.А. Белеванцев. Статический анализатор Svace как коллекция анализаторов разных уровней сложности. Труды ИСП РАН, том 27, вып. 6. 2015 г. стр. 111-134. DOI: 10.15514/ISPRAS-2015-27(6)-8.

8. А.Е. Бородин, Межпроцедурный контекстно-чувствительный статический анализ для поиска ошибок в исходном коде программ на языках Си и Си++: дис. канд. ф.-м. наук. Москва, 2016г.


Для цитирования:


Дудина И.А., Кошелев В.К., Бородин А.Е. Поиск ошибок доступа к буферу в программах на языке C/C++. Труды Института системного программирования РАН. 2016;28(4):149-168. https://doi.org/10.15514/ISPRAS-2016-28(4)-9

For citation:


Dudina I..., Koshelev V..., Borodin A... Statically detecting buffer overflows in C/C++. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(4):149-168. (In Russ.) https://doi.org/10.15514/ISPRAS-2016-28(4)-9

Просмотров: 87


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


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