Лекция 7. Статический анализ (Лекции)

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 7:Статический анализВМиК МГУ им. М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.2План лекции• Статический анализ– Модели программ– Алгоритмы статического анализа– Обнаружение дефектов• Другие статические методы• Заключение2Литература• Карпов Ю.Г. Model Checking.Верификация параллельных ираспределенных программныхсистем, БХВ-Петербург, 2010.• Кларк, Грумберг, Пелед.Верификация моделей программ:Model checking, МЦНМО, 2002.• Peled. Software Reliability Methods,Springer, 2001.3О чём этот курс• Концепции и связи• Аналитические модели и средстваподдержки• Методы для увеличения надёжности ПО:––––––ВерификацияСтатический анализТестированиеРасчёт надёжностиАнализ статистики ошибокБезопасность4Статические методыобеспечения качества5• Формальные инспекции, аудит• Формальная верификация– Дедуктивная верификация– Model checking• Статический анализ• Трансформации– Рефакторинги– Модификации56Статический анализ• Использует исходный код ПО для анализа• Применяется для–––––––––Форматирования программВычисления программных метрикОптимизации программРаспараллеливания программПреобразования программОбфускации программДеобфускации программОбнаружения дефектов…6Статический анализ дляобнаружения дефектов7• Использует исходный код ПО ВС дляанализа• Позволяет проанализировать всевозможные трассы исполнения• Позволяет проанализировать все наборывходных данных• Может быть полностью автоматизирован• Позволяет обнаружить нефункциональныедефектыx=1 y=2 z=9 x=2z = 13y=5 z=07Нефункциональные дефекты• Ошибки этапа кодирования• Не являются явным нарушениемспецификации• Являются следствием– сложности языков программирования– сложности библиотек– сложности алгоритмов и структурданных88Нефункциональные дефекты• Выход за границу массива• Переполнение буфера• Использование неинициализированныхобъектов• Работа с некорректным указателем• Арифметические ошибки• Утечки ресурсов• Ошибки форматных строк• Ошибки работы с ресурсами• и т.д.9910Проявление дефектов••••••Без проявленияЗависанияСбоиПаденияДеградация производительности…1011Опасные конструкции• Язык С–––––––МакроопределенияУказателиМассивыАдресная арифметикаУказатели на функцииПриведения типовОбъединения (union)1112Характеристики анализа• Полнота – доля найденных дефектовпо отношению ко всем дефектампрограммы• Точность – доля найденныхистинных дефектов по отношению ковсем найденным• Ресурсоемкость12Общая схема обнаружениядефектов1313Модели программ.Требования14• Полнота представления объектовпрограммы• Восстанавливаемость– Идеально: возможность полноговосстановления исходного кода– Желательно: связь с исходным кодом• Эффективность поиска объектов1415Модели программ.

Типы•Структурные––•Поведенческие–––•Синтаксическое дерево разбораАбстрактное синтаксическое дерево (AST –abstract syntax tree)Граф потока управления (CFG – control flow graph)Граф зависимостей по данным (DDG – datadependence graph)SSA - static single assignmentГибридные–Абстрактный семантический граф (ASG - abstractsemantic graph)1516Модели программ: ASTint main(){int n = 10;int f = 1;while (n >0){f *= n;--n;}return f;}1617Модели программ: ASGint main(){int n = 10;int f = 1;while (n >0){f *= n;--n;}return f;}1718Модели программ: DDGint main(){int n = 10;int f = 1;while (n >0){f *= n;--n;}return f;}1819Модели программ: CFGint main(){int n = 10;int f = 1;while (n >0){f *= n;--n;}return f;}1920Модели программ: SSAint main(){int n = 10;int f = 1;while (n >0){f *= n;--n;}return f;}20Модели программ.

Резюме• Для простейшего статическогоанализа достаточно структурныхмоделей (AST)• Для обнаружения дефектовнеобходим учет семантики:– ASG– CFG– CFG в форме SSA2121Модели программ.Построение22• Построение парсера вручную• Использование генераторов парсеров(ANTLR, YACC, etc)• Использование самостоятельных парсеров(Elsa)• Использование парсеров в составе средствразработки (NetBeans, Eclipse CDT)• Использование Front-End компиляторов(gcc)• Использование фреймворков длястатического анализа (SUIF, CIL, LLVM, etc)22Общая схема обнаружениядефектов2323Анализ на основе состоянийпрограммы• Состояние программы – совокупностьсостояний всех объектов программы вкакой-либо точке• Цель – вычислить все возможныесостояния программы во всех точках• Обнаружение дефектов происходит наоснове проверки вычисленных состояний2424Алгоритмы статическогоанализа25• По типу алгоритму– Интервальный анализ– Анализ указателей– Ресурсный анализ• По масштабу– Внутрипроцедурный– Межпроцедурный• По консервативности– Пессимистический (консервативный) анализ– Оптимистический анализ2526Интервальный анализ• Состояние переменных представляютсяинтервальными значениями–––a = [10;20]b = (-40;20) U (30;100)c = [0;∞)• Вычисление состояния после выполненияоператора языка производится на основеинтервальной арифметики• Каждому оператору ставится в соответствиеуравнение, связывающее состояние довыполнения и после2627Интервальный анализЭлемент моделиИнтервальное правилоint a;Sl = Sl-1  <a, noninit>a = С;Sl = Sl-1 \ Ui<a, i>  <a, С>a = b;φ(…)if(cond) Strue else SfalseSl = Sl-1 \ Ui<a, i>  Uj<a, bj>Sl = Ui SiStrue= Sl-1  condSfalse= Sl-1  cond27Интервальный анализ.Примерint a;a=10;int b =if (b <…a = a}else{…a = b}f(…);100){28<a, noninit><a, [10:10]><a, [10:10]>, <b, (-; )>+ b;<a, [10:10]>, <b, (-; 100)><a, [-+10:110]>, <b, (-; 100)>/ 2;<a, [10:10]>, <b, [100; )><a, [50: /2]>, <b, [100; )>2829Анализ указателей• Отличие от интервального анализа:– хранятся не интервалы значений, асписки связи “points-to”– значения одних объектов могут влиятьна другиеoj10oj21...k1...01...k2...2930Анализ указателей.

Пример• p, q1 и q2 – указатели на динамическуюпамять• Пример для конструкции free(p);oj2p01...0k2q2q1oj101...0oj2p010...k2...0q20q100oinvalid...k1...oj101...k1...3031Анализ указателей. Пример• p, q – указатели• Пример для конструкции *p = qot1p1...k2...p0oj1q001...j2...q0ok101...k20...oj101...j2...ok101...k2...03132Анализ указателей. Пример• p, q – указатели• Пример для конструкции p = *qpp00ot1ok101...k2q01...k2oj1...q0oj21...k2...01...k2...01...k2......oinvalidoj100oj2001...k2...oj301...k2...oj301...k2...ot101...k2...ot101...k2...3233Ресурсный анализ••••Ресурсы – объекты программы, имеющие свойжизненный циклПримеры ресурсов:––––––––Выделенная динамическая памятьФайлыСемафорыМьютексыСокетыПотокиНити…Обычно ресурсы характеризуются состоянием иатрибутамиКаждый тип ресурса изменяет свое состояние поопределенным правилам33Ресурсный анализ.Объект в куче34• Правила использования– Создается ( p = malloc(…) )– Используется ( *p )– Освобождается ( free(p) )• Примеры дефектов– Использование не созданного объекта– Повторное освобождение– Утечка3435Ресурсный анализ.

Файл• Правила использования– Открыть ( f = fopen(“…”, “r” )– Читать/писать ( fprintf(f, …) )– Закрыть ( close(f) )• Примеры дефектов– Чтение из не открытого файла– Попытка писать в файл открытый начтение– …3536Ресурсный анализ• Отличие ресурсов от других объектовпрограммы:– Управляются операционной системой– Управление сменой состояний и атрибутовпроисходит через функции API• Необходимо анализировать неконструкции ЯП, а библиотечные вызовы• Необходима информация о семантикебиблиотечных вызовов:– Семантика зашита в анализатор– Семантика описывается через аннотированиебиблиотек3637Масштаб анализа• Внутрипроцедурный анализ– Каждая функция анализируетсяотдельно– Информация не передается междуфункциями– Ресурсоемкость относительно низкая– Точность и/или полнота – снижаются– Реализуется большинствоманализаторов3738Масштаб анализа• Межпроцедурный анализ– Все функция анализируется совместно– Информация передается междуфункциями– Ресурсоемкость очень высокая– Точность и/или полнота – выше– Реализовано в небольшом числесредств38Консервативность анализа• Определяется правилами объединенияветвей• Консервативный (пессимистический) анализ–––При объединении ветвей объединяет интервалыСохраняет полноту (обнаруживаем все ошибки)Теряет точность (много ложных обнаружений)• Оптимистический анализ–––При объединении ветвей пересекает интервалыТеряет полноту (может пропускать ошибки)Сохраняет точность (мало ложных обнаружений)3939Консервативность анализаint arr1[10];int arr2[5];if (…){…}// <i, [1..8]>else {…}// <i, [6..15]>a = arr1[i]; // возможноошибкаb = arr2[i]; // ошибка•Консервативныйанализ:––•<i, [1..15]>обнаружит обе ошибки(возможно первая –ложная)Оптимистическийанализ––<i, [6..8]>обнаружит вторую ошибку(пропустив первую)404041Решение уравнений• В результате применения алгоритмов в явномили неявном виде строится системауравнений• Решение системы––С использованием теории решетокМетодами абстрактной интерпретации• Завершаемость процесса решенияобуславливается––Монотонностью уравненийКонечностью системы уравнений41Общая схема обнаружениядефектов424243Обнаружение дефектов• На основе анализа допустимостисостояний в элементах модели• Использование неинициализированнойпеременной:– Конструкция: a = b– Условие: <a, noninit>  Sl-1• Повторное освобождение объекта– Конструкция: free(p)– Условие: <p, invalid>  Sl-14344Обнаружение дефектов• Разыменование некорректного указателя––Конструкция: a = *pУсловие: <p, invalid>  Sl-1• Арифметические операции над указателямина разные объекты––Конструкция: a = p – q;Условие: <p, o1>,<q, o2>  Sl-1, o1≠o2• Выход за границы объекта––Конструкция: a = *p;Условие: <p, o, k>  Sl-1, k≥≠osize44Проблемы статическогоанализа45• Анализ циклов• Анализ рекурсии и глубокойвложенности вызовов• Анализ больших типов данных• Анализ программ с исключениями• Анализ программ с полиморфизмоми указателями на функции45Статический анализ.