Поиск ошибок доступа к буферу в программах на языке C/ C++
Автор: Дудина И.А., Кошелев В.К., Бородин А.Е.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 4 т.28, 2016 года.
Бесплатный доступ
В статье рассматривается алгоритм статического анализа для поиска в исходном коде программы ошибок доступа к буферу. Алгоритм использует символьное исполнение с объединением состояний и является чувствительным к путям. Рассматриваются только обращения к буферам, имеющим известный в момент компиляции размер и размещённым в статической памяти либо на стеке. В работе приведено формальное определение ошибки доступа к буферу, возникающей при прохождении некоторой последовательности рёбер графа потока управления программы. Приведён алгоритм, позволяющий для переменных программы суммировать информацию о возможных значениях по всем путям с учётом совместности условий переходов, взаимосвязи переменных через арифметические операции, инструкции преобразования типов, бинарные отношения в условиях переходов. Для инструкций доступа к буферу с помощью вычисленной для переменной индекса информации о возможных значениях вычисляются достаточные условия выхода за границы. Выполнимость достаточных условий проверяется SMT-решателем и, в случае нахождения модели, с её помощью обнаруживается ошибочный путь и выдаётся предупреждение. На основе данного подхода в инструменте статического анализа Svace был реализован межпроцедурный чувствительный к путям детектор ошибок доступа к буферу, способный обнаруживать новые, не покрытые предыдущими реализациями детекторов типы ошибок.
Статический анализ, поиск дефектов, переполнение буфера, чувствительность к путям, символьное исполнение
Короткий адрес: https://sciup.org/14916368
IDR: 14916368 | DOI: 10.15514/ISPRAS-2016-28(4)-9
Statically detecting buffer overflows in C/ C++
The paper describes a static analysis approach for buffer overflow detection in C/C++ source code. This algorithm is designed to be path-sensitive as it is based on symbolic execution with state merging. For now, it works only with buffers on stack or on static memory with compile-time known size. We propose a formal definition for buffer overflow errors that are caused by executing a particular sequence of program control-flow edges. To detect such errors, we present an algorithm for computing a summary for each program value at any program point along multiple paths. This summary includes all joined values at join points with path conditions. It also tracks value relations such as arithmetic operations, cast instructions, binary relations from constraints. For any buffer access we compute a sufficient condition for overflow using this summary for index variable and the reachability condition for the current function point. If this condition is proved to be satisfiable by an SMT-solver, we use its model given by the solver to detect error path and report the warning with this path. This approach was implemented for Svace static analyzer as the new buffer overflow detector, and it has found a significant amount of unique true warnings that are not covered by the old buffer overflow detector implementations.
Список литературы Поиск ошибок доступа к буферу в программах на языке 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
