Preview

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

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

Обнаружение ошибок доступа к буферу в программах на языке C/C++ с помощью статического анализа

https://doi.org/10.15514/ISPRAS-2016-28(5)-7

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

Аннотация

В данной работе рассматривается метод поиска межпроцедурных ошибок доступа к буферу с помощью статического анализа. В основе рассматриваемого подхода лежит разработанный ранее алгоритм внутрипроцедурного анализа на базе символьного исполнения с объединением состояний, который является чувствительным к путям и учитывает взаимосвязи между переменными, такие как сравнения, арифметические операции и инструкции приведения типа. В работе предложено формальное определение межпроцедурного дефекта и рассмотрены некоторые типы межпроцедурных ошибок доступа к буферу. Межпроцедурный анализ реализован с помощью метода резюме, что позволяет в некоторой степени добиться контекстной чувствительности. Показано, как можно расширить внутрипроцедурный алгоритм для отслеживания межпроцедурных связей между переменными. Кроме этого, приведен алгоритм построения двух типов достаточных условий наличия ошибки доступа к буферу в функции, которые сохраняются в резюме и проверяются при вызове этой функции. Описанный подход был реализован в инструменте статического анализа Svace. На проекте Android 5.0.2 было получено 351 предупреждение об ошибке доступа к буферу, среди которых 64% оказались истинными, при этом существенного замедления анализа не произошло.

Об авторе

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


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

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

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

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: 10.1145/2345156.2254088

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

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

8. Shahriar, H., and Zulkernine, M. Classification of static analysis-based buffer overflow detectors. SSIRI-C 2010 - 4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion, 2010, pp. 94-101.

9. Y. Xie, A. Chou, and D. Engler, “ARCHER: Using Symbolic, Path-sensitive Analysis to Detect Memory Access Errors,” Proceedings of the 9th European Software Engineering Conference, Helsinki, Finland, 2003, pp. 327-336.


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


Дудина И.А. Обнаружение ошибок доступа к буферу в программах на языке C/C++ с помощью статического анализа. Труды Института системного программирования РАН. 2016;28(5):119-134. https://doi.org/10.15514/ISPRAS-2016-28(5)-7

For citation:


Dudina I... Inter-procedural buffer overflows detection in C/C++ source code via static analysis. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(5):119-134. (In Russ.) https://doi.org/10.15514/ISPRAS-2016-28(5)-7

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


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


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