Статический анализ для поиска переполнения буфера: актуальные направления развития

В последние десятилетия переполнение буфера остаётся одним из главных источников программных ошибок и эксплуатируемых уязвимостей. Среди прочих подходов к устранению подобных дефектов активное развитие получили различные методы статического анализа. В работе рассматриваются основные подходы и инструменты, используемые для решения этой задачи, с целью выявить наиболее популярные методы и типы обнаруживаемых ошибок. Также исследованы наборы синтетических тестов (Juliet Test Suite, Toyota ITC benchmark) и выборка фрагментов кода реальных приложений, содержащих эксплуатируемую ошибку переполнения буфера. Для понимания направлений развития промышленного статического анализатора важно рассматривать оба эти источника примеров ошибочных программ. Наборы тестов очерчивают круг ситуаций, которые необходимо поддержать в анализаторе, при этом их легко понять, классифицировать и проверить. С другой стороны, они не отражают распределение таких ситуаций в реальном коде. Выборка уязвимостей из промышленных проектов также представляет интерес для исследования, но оказывается смещённой в сторону эксплуатируемых ошибок и к тому же не включает ошибки, исправленные на стадии разработки (возможно, как раз с использованием статического анализатора). Полученные данные были использованы для выделения основных шаблонов дефектов, которые должен обнаруживать статической анализатор с точки зрения пользователя. В результате исследования к наиболее важным возможностям статического анализатора были отнесены межпроцедурный путе- и контекстно-чувствительный анализ, а также базовая поддержка циклов. Кроме того, полезными оказываются отслеживание аффинных отношений между переменными и моделирование строк как важного случая использования массивов. Результаты данного исследования используются для улучшения детектора переполнения буфера, реализованного в рамках инфраструктуры статического анализатора Svace. На данный момент используется межпроцедурный чувствительный к путям и контексту анализ, позволяющий обнаруживать переполнения буфера на стеке и в статической памяти с долей истинных срабатываний 65%. По результатам исследования наиболее перспективными направлениями представляются поддержка строковых операций и внедрение анализа помеченных данных в имеющиеся подходы.