Статический анализатор Svace. Промышленный поиск критических ошибок в безопасном цикле разработки программ

Актуальность задачи

Ошибки в программах серьезно влияют на качество, приводя к сбоям в работе, а в некоторых случаях (уязвимости) – к перехвату контроля над системой. Сложность поиска ошибок существенно возросла в последние 20 лет, т.к. размеры программ достигли сотен миллионов строк кода. Предложено множество методов поиска ошибок, и их совместное применение регламентируется созданными циклами безопасной разработки ПО: например, Microsoft Security Development Lifecycle, ГОСТ Р 56939-2016 «Защита информации. Разработка безопасного программного обеспечения. Общие требования».

Одним из признанных методов поиска ошибок, обязательным к применению в упомянутых выше циклах разработки, является статический анализ исходного кода программ. Преимуществами метода являются:

одновременный анализ многих путей выполнения сразу (масштабируемость),
поиск ошибок на редко выполняющихся путях (плохо покрывающихся тестированием или динамическим анализом).

Недостатком является наличие ложных предупреждений об ошибках, от которых нельзя полностью избавиться из-за принципиальных ограничений технологии статического анализа.

Инструмент статического анализа Svace

Институтом системного программирования РАН разработан инструмент статического анализа Svace, удовлетворяющий всем требованиям для анализатора промышленного качества:

Автоматизация: полностью автоматическая работа анализатора, требующая минимум настройки со стороны пользователя;
Масштабируемость: анализ программ из миллионов строк кода за несколько часов (например, ОС Android 6 – за 5 часов);
Качество: высокий уровень истинных срабатываний (60-90% в зависимости от типа находимой ошибки);
Понятность: подробное объяснение потенциальной ошибки пользователю (текстовое описание, указание места проявления ошибки, а также цепочки причин, приведших к ошибке);
Отслеживание результатов: хранение результатов серии запусков анализатора над заданной программой в базе данных, разметка предупреждений пользователем на ложные/истинные в графическом интерфейсе, сравнение запусков анализа между собой, автоматический перенос разметки результатов между запусками и др.

Инструмент Svace поддерживает языки программирования C/C++, Java, C# (C# может также предоставляться как отдельный инструмент), операционные системы Linux, Windows, а также анализ программ, собираемых на платформах Intel x86/x86-64 Linux/Windows, ARM/ARM64. Для языков C/C++ поддерживаются популярные компиляторы ОС Linux/Windows и множество компиляторов для встраиваемых систем.

Инструмент Svace поддерживает обнаружение большинства известных классов критических ошибок (всего более 50 типов ошибок): разыменование нулевого указателя, ошибки управления динамической памятью, переполнение буфера, деление на ноль, утечки ресурсов (память / дескрипторы), неинициализированные переменные, ошибки использования блокировок. Кроме того, реализовано более сотни легковесных детекторов для ошибок кодирования, неверного использования интерфейсов, соблюдения стандартов кодирования.

Фундаментальные исследования по технологиям статического анализа, реализованные в инструменте Svace, ведутся в ИСП РАН с 2002 года. С 2009 года в партнерстве с компанией Samsung ведутся работы по внедрению инструмента в цикл разработки программ в Samsung. В 2015 году Svace внедрен как основной инструмент статического анализа в Samsung, в том числе он используется для проверки собственного ПО Samsung на базе ОС Android и исходного кода ОС Tizen, применяемого для мобильных телефонов, телевизоров и других устройств компании.

Кроме того, технологии анализа Svace используются во внутренних проектах ИСП РАН по анализу кода.

Все интеллектуальные права на инструмент Svace принадлежат ИСП РАН.

Схема работы инструмента Svace

Применение инструмента Svace (так же, как и других промышленных инструментов статического анализа) можно поделить на три этапа:

Контролируемая инструментом сборка анализируемой программы
Выполняется обычная сборка программы пользователя под управлением системы мониторинга сборки Svace. При обнаружении запусков известных компиляторов поддерживаемых языков (C/C++/Java/C#) параллельно запускаются собственные компиляторы Svace для генерации внутреннего представления для анализа (см. рисунок).
Анализ программы
Для собранного на этапе 1 представления программы сначала запускаются легковесные анализаторы, специфичные для каждого языка программирования и находящие разнообразные ошибки кодирования. Далее запускается основной движок анализа (см. рис.), в ходе которого сначала строится граф вызовов программы, а потом выполняется контекстно-чувствительный межпроцедурный анализ однократным обходом графа вызовов так, что вызывающие функции анализируются после вызываемых. В ходе анализа каждой функции выполняется анализ указателей, анализ возможных значений переменных, создается модель памяти программы и др. По окончании анализа каждой конкретной функции создается специальная структура данных (резюме функции), обобщающая результаты анализа, что позволяет не возвращаться более к телу проанализированной функции, а использовать ее резюме.

Движок анализа делится на две части: ядро анализа и детекторы конкретных видов ошибок. Ядро выполняет основную часть анализа, подготавливая для детекторов информацию о модели памяти программы, потоках данных и управления и т.п. Детекторы могут вычислять дополнительные необходимые им атрибуты программы, опираясь на интерфейсы ядра. Тем самым достигается расширяемость и масштабируемость анализа.

Различение отдельных путей выполнения (чувствительность к путям) для детекторов достигается хранением предикатов, при условии выполнения которых происходят интересующие анализ события. Предикаты проверяются на совместность с помощью промышленного SMT-решателя Z3 от Microsoft Research.
Просмотр результатов
Результаты запуска анализатора сохраняются в базе данных. Для их просмотра предоставляется веб-интерфейс (см. скриншот), позволяющий разметить срабатывания анализатора как истинные либо ложные, при этом при последующих анализах той же программы вся история разметки будет сохранена (см. рисунок).

Svace

Дополнительные возможности Svace

В инструменте Svace реализован ряд дополнительной функциональности, облегчающей его применение на этапе разработки программ:

Возможность выполнения этапов сборки и анализа на отдельных машинах;
Возможность выполнения быстрого повторного анализа части программы с учетом ранее собранных данных о поведении остальной программы (например, быстрый анализ Android-приложения с учетом данных предыдущего полного анализа всей ОС Android);
Возможность написания пользовательских легковесных детекторов для C/C++ и Java.

Уровень истинных срабатываний

Пример результатов инструмента Svace на анализе исходного кода ОС Android 5.0.2 представлен ниже.

Svace

По вопросам определения стоимости, приобретения и использования, обращайтесь по адресу svace@ispras.ru

Исполнитель

Компиляторные технологии

Перейти к списку всех проектов