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

Ошибки при работе с библиотечными функциями обработки строк в языке Си являются частой причиной переполнения буфера, что в свою очередь нередко приводит к отказу в обслуживании, некорректной работе программы или появлению эксплуатируемой уязвимости. Одним из способов устранения различных ошибок на стадии разработки программы является статический анализ. Существующие методы статического анализа, ориентированные на работу со строками, либо не обеспечивают должный уровень истинных срабатываний, либо пропускают большое количество ошибок, либо неприменимы к промышленным программам большого размера, либо реализованы в рамках закрытых инструментов. Для наиболее полного покрытия дефектов в реальных программах необходимо обнаруживать ошибки, происходящие лишь на некоторых путях выполнения и не определяемые единственной точкой программы, и, кроме того, находить ошибки, связанные с некорректным использованием не только библиотечных, но и пользовательских функций. Целью данного исследования является построение алгоритма поиска ошибок при работе со строками, удовлетворяющего этим свойствам, ограничению на количество ложных срабатываний (не более 40%), применимого к любым программам на языке Си и масштабирующегося на проекты из нескольких миллионов строк. Для решения этой задачи был использован ранее разработанный подход символьного исполнения с объединением состояний, который был адаптирован для поддержки строковых операций. На основе алгоритма отслеживания операций с целыми числами был предложен алгоритм отслеживания длин строк. Разработанный алгоритм реализован в качестве одного из детекторов семейства детекторов переполнения буфера в рамках инструмента статического анализа Svace. В результате на тестовом наборе Juliet test suite на тестах, связанных с переполнением правой границы буфера, покрытие срабатываниями увеличилось с 15,4% до 41,5%, при этом не было выдано ни одного ложного предупреждения. По сравнению с известным анализатором Infer на наборе Juliet инструмент Svace без поддержки строк показывает приблизительно те же результаты, за исключением случая сложных циклов, а связанные со строками переполнения Infer, как правило, не находит.

1. Wagner D., Foster J., Brewer E., Aiken A. A first step towards automated detection of buffer overrun vulnerabilities. In Proc. of the Network and Distributed System Security Symposium, 2000, pp. 3-17.

2. Zitser M., Lippmann R., Leek T. Testing static analysis tools using exploitable buffer overflows from open source code. ACM SIGSOFT Software Engineering Notes, vol. 29, issue 6, 2004, pp. 97-106.

3. Kratkiewicz K. Evaluating Static Analysis Tools for Detecting Buffer Overflows in C Code. Master's Thesis, Harvard University, 2005.

4. Dor N., Rodeh M., Sagiv M. CSSV: Towards a Realistic Tool for Statically Detecting All Buffer Overflows in C. ACM SIGPLAN Notes, vol. 38, 2003, pp. 155-167.

5. Simon A., King A. Analyzing String Buffers in C. Algebraic Methodology and Software Technology, vol. 2422, 2002, pp. 365-379.

6. Allamigeon X. Static analysis of memory manipulations by abstract interpretation. Algorithmics of tropical polyhedra, and application to abstract interpretation. PhD Thesis, École Polytechnique, 2009.

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

8. Dudina I. A., Belevantsev A. A. Using static symbolic execution to detect buffer overflows. Programming and Computer Software, vol. 43, issue 5, pp. 277–288, 2017. DOI: 10.1134/S0361768817050024

9. Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Berzish, M., Dolby, J., Zhang, X. Z3str2: an efficient solver for strings, regular expressions, and length constraints. Formal Methods in System Design, vol. 50, 2017, pp.249-288.

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

11. Juliet Test Suite v1.2 for C/C++. User Guide. Center for Assured Software National Security Agency, December 2012.

12. Infer static analyzer Infer. URL: https://fbinfer.com/ (Дата обращения: 21.09.2018)

13. Inferbo: Infer-based buffer overrun analyzer. URL: https://research.fb.com/inferbo-infer-based-buffer-overrun-analyzer/ (Дата обращения: 21.09.2018)

14. Calcagno C., Distefano D. et al. Moving Fast with Software Verification. Lecture Notes in Computer Science, vol. 9058, 2015, pp. 3-11.

15. Calcagno C., Distefano D., O’Hearn P., Hongseok Y. Compositional Shape Analysis by means of Bi-Abduction. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL '09), 2009, pp. 289-300.