Buffer overflow detection via static analysis: expectations vs. reality
Автор: Dudina I.A.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 3 т.30, 2018 года.
Бесплатный доступ
Over the last few decades buffer overflow remains one of the main sources of program errors and vulnerabilities. Among other solutions several static analysis techniques were developed to mitigate such program defects. We analyzed different approaches and tools that address this issue to discern common practices and types of detected errors. Also, we explored some popular sets of synthetic tests (Juliet Test Suite, Toyota ITC benchmark) and set of buggy code snippets extracted from real applications to define types of defects that a static analyzer is expected to uncover. Both sources are essential to understand the design goals of a production quality static analyzer. Test suites expose a set of features to support that is easy to understand, classify, and check. On the other hand, they don’t provide a real picture of a production code. Inspecting vulnerabilities is useful but provides an exploitation-biased sample. Besides, it does not include defects eliminated during the development process (probably with the help of some static analyzer). Our research has shown that interprocedural analysis, path-sensitivity and loop handling are essential. An analysis can really benefit from tracking affine relations between variables and modeling C-style strings as a very important case of buffers. Our goal is to use this knowledge to enhance our own buffer overrun detector. Now it can perform interprocedural context- and path-sensitive analysis to detect buffer overflow mainly for static and stack objects with approximately 65% true positive ratio. We think that promising directions are improving string manipulations handling and combining taint analysis with our approaches.
Software error detection, static analysis, buffer overrun
Короткий адрес: https://sciup.org/14916540
IDR: 14916540 | DOI: 10.15514/ISPRAS-2018-30(3)-2
Статический анализ для поиска переполнения буфера: актуальные направления развития
В последние десятилетия переполнение буфера остаётся одним из главных источников программных ошибок и эксплуатируемых уязвимостей. Среди прочих подходов к устранению подобных дефектов активное развитие получили различные методы статического анализа. В работе рассматриваются основные подходы и инструменты, используемые для решения этой задачи, с целью выявить наиболее популярные методы и типы обнаруживаемых ошибок. Также исследованы наборы синтетических тестов (Juliet Test Suite, Toyota ITC benchmark) и выборка фрагментов кода реальных приложений, содержащих эксплуатируемую ошибку переполнения буфера. Для понимания направлений развития промышленного статического анализатора важно рассматривать оба эти источника примеров ошибочных программ. Наборы тестов очерчивают круг ситуаций, которые необходимо поддержать в анализаторе, при этом их легко понять, классифицировать и проверить. С другой стороны, они не отражают распределение таких ситуаций в реальном коде. Выборка уязвимостей из промышленных проектов также представляет интерес для исследования, но оказывается смещённой в сторону эксплуатируемых ошибок и к тому же не включает ошибки, исправленные на стадии разработки (возможно, как раз с использованием статического анализатора). Полученные данные были использованы для выделения основных шаблонов дефектов, которые должен обнаруживать статической анализатор с точки зрения пользователя. В результате исследования к наиболее важным возможностям статического анализатора были отнесены межпроцедурный путе- и контекстно-чувствительный анализ, а также базовая поддержка циклов. Кроме того, полезными оказываются отслеживание аффинных отношений между переменными и моделирование строк как важного случая использования массивов. Результаты данного исследования используются для улучшения детектора переполнения буфера, реализованного в рамках инфраструктуры статического анализатора Svace. На данный момент используется межпроцедурный чувствительный к путям и контексту анализ, позволяющий обнаруживать переполнения буфера на стеке и в статической памяти с долей истинных срабатываний 65%. По результатам исследования наиболее перспективными направлениями представляются поддержка строковых операций и внедрение анализа помеченных данных в имеющиеся подходы.
Список литературы Buffer overflow detection via static analysis: expectations vs. reality
- J. Viega, J. T. Bloch, Y. Kohno, and G. McGraw. Its4: A static vulnerability scanner for c and c++ code. In Proceedings of the 16th Annual Computer Security Applications Conference, 2000, pp. 257-269.
- P. Cousot and R. Cousot. Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1977, pp. 238-252.
- X. Allamigeon. Static analysis of memory manipulations by abstract interpretation -Algorithmics of tropical polyhedra, and application to abstract interpretation. PhD thesis, Ecole Polytechnique X, Nov. 2009. . Available: https://pastel.archives-ouvertes.fr/pastel-00005850, accessed: 2018-04-08.
- W. Le and M. L. Soffa. Marple: A Demand-Driven Path-Sensitive Buffer Overflow Detector. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, 2008, p. 272-282.
- L. Li, C. Cifuentes, and N. Keynes. Practical and effective symbolic analysis for buffer overflow detection. In Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, pp. 317-326.
- X. Xie, Y. Liu, W. Le, X. Li, and H. Chen. S-looper: automatic summarization for multipath string loops. In Proceedings of the 2015 International Symposium on Software Testing and Analysis, 2015, pp. 188-198.
- Juliet Test Suite v1.2 for C/C++. User Guide. Available: https://samate.nist.gov/SRD/around.php#juliet_documents, accessed: 2018-04-08.
- S. Shiraishi, V. Mohan, and H. Marimuthu. Test suites for benchmarks of static analysis tools. In Proceedings of the 2015 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), Nov 2015, pp. 12-15.
- T. Ye, L. Zhang, L. Wang, and X. Li. An Empirical Study on Detecting and Fixing Buffer Overflow Bugs. In Proceedings of the 2016 IEEE International Conference on Software Testing, Verification and Validation, 2016, pp. 91-101.
- CVE security vulnerability database. Security vulnerabilities, exploits, references and more. Available: https://www.cvedetails.com/index.php, accessed: 2018-04-08.
- K. Kratkiewicz and R. Lippmann. A taxonomy of buffer overflows for evaluating static and dynamic software testing tools. In Proceedings of Workshop on Software Security Assurance Tools, Techniques, and Metrics, vol. 500, 2006, pp. 44-51.
- A. Borodin and A. Belevantcev. A static analysis tool Svace as a collection of analyzers with various complexity levels. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 6, 2015, pp. 111-134.
- I.A. Dudina and A.A. Belevantsev. Using static symbolic execution to detect buffer overflows. Programming and Computer Software, vol. 43, no. 5, 2017, pp. 277-288 DOI: 10.1134/S0361768817050024
- Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: A z3-based string solver for web application analysis. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, 2013, pp. 114-124.
