Поиск ошибок доступа к буферу в программах на языке C/ C++
Автор: Дудина И.А., Кошелев В.К., Бородин А.Е.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 4 т.28, 2016 года.
Бесплатный доступ
В статье рассматривается алгоритм статического анализа для поиска в исходном коде программы ошибок доступа к буферу. Алгоритм использует символьное исполнение с объединением состояний и является чувствительным к путям. Рассматриваются только обращения к буферам, имеющим известный в момент компиляции размер и размещённым в статической памяти либо на стеке. В работе приведено формальное определение ошибки доступа к буферу, возникающей при прохождении некоторой последовательности рёбер графа потока управления программы. Приведён алгоритм, позволяющий для переменных программы суммировать информацию о возможных значениях по всем путям с учётом совместности условий переходов, взаимосвязи переменных через арифметические операции, инструкции преобразования типов, бинарные отношения в условиях переходов. Для инструкций доступа к буферу с помощью вычисленной для переменной индекса информации о возможных значениях вычисляются достаточные условия выхода за границы. Выполнимость достаточных условий проверяется SMT-решателем и, в случае нахождения модели, с её помощью обнаруживается ошибочный путь и выдаётся предупреждение. На основе данного подхода в инструменте статического анализа Svace был реализован межпроцедурный чувствительный к путям детектор ошибок доступа к буферу, способный обнаруживать новые, не покрытые предыдущими реализациями детекторов типы ошибок.
Статический анализ, поиск дефектов, переполнение буфера, чувствительность к путям, символьное исполнение
Короткий адрес: https://sciup.org/14916368
IDR: 14916368 | DOI: 10.15514/ISPRAS-2016-28(4)-9
Список литературы Поиск ошибок доступа к буферу в программах на языке C/ C++
- CVE and CCE Statistics Query Page. https://web.nvd.nist.gov/view/vuln/statistics
- A. One, "Smashing the Stack for Fun and Profit", Phrack Magazine, Volume 7, Issue 49, November 1996.
- D. Larochelle, D. Evans. Statically detecting likely buffer overflow vulnerabilities. 10th USENIX Security Symposium, Washington, D.C., August 2001.
- V.P. Ivannikov, A.A. Belevantsev, A.E. Borodin, V.N. Ignatiev, D.M. Zhurikhin, A.I. Avetisyan, M.I. Leonov. Static analyzer Svace for finding of defects in program source code. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 231-250 DOI: 10.15514/ISPRAS-2014-26(1)-7
- 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.o DOI: rg/10.1145/2345156.2254088
- V. Koshelev, I. Dudina, V. Ignatyev, A. Borzilov. Path-Sensitive Bug Detection Analysis of C# Program Illustrated by Null Pointer Dereference. Trudy ISP RAN/Proc. ISP RAS, 2015, vol. 27, issue 5, pp. 59-86. 5 DOI: 10.15514/ISPRAS-2015-27(5)-
- A. Borodin, A. Belevancev. A Static Analysis Tool Svace as a Collection of Analyzers with Various Complexity Levels. Trudy ISP RAN/Proc. ISP RAS, 2015, vol. 27, issue 6, pp. 111-134 DOI: 10.15514/ISPRAS-2015-27(6)-8
- A. Borodin. PhD thesis. Interprocedural contex-sensitive static analysis for error detection in C/C++ source code. ISP RAN, Moscow, 2016
