Верификация программного обеспечения. Текущее состояние и проблемы ИВАННИКОВ Виктор Петрович, Институт системного программирования РАН (ИСП РАН) ivan@ispras.ru. - презентация

1 Верификация программного обеспечения. Текущее состояние и проблемы ИВАННИКОВ Виктор Петрович, Институт системного программирования РАН (ИСП РАН) 16 апреля 2012 года

2 Сложность современного ПО СистемаГодРазмер (10 6 LOC) Размер команды Windows Windows NT Windows NT Windows Windows XP Linux Kernel ,7 Open Solaris20059,7 Mac OS X Windows Vista2007> 50 Вся авионика США (бортовая и наземная) 2007~1000 Дистрибутив Debian

3 Статистика ошибок Количество ошибок на 1000 строк кода (до тестирования) остается практически неизменным за 30 лет Программные системыЧисло ошибок на 1000 строк кода Microsoft (до тестирования)10-20 NASA JPL (до тестирования)6-9 Среднее по индустрии (продукты)6-30 Linux~7 Microsoft (продукты)0.5 NASA JPL (продукты)

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

5 Технологии верификации Экспертиза Тестирование (динамические испытания) Аналитическая верификация Статический анализ Комбинированные подходы 5

6 Экспертиза Поиск ошибок, оценка и анализ свойств ПО человеком (обычно группа 2-5 человек) Техники –Списки важных ограничений и шаблонов ошибок –Групповые обсуждения Производительность : строк / час –Не более 2-3 часов в день Результаты : выявляется 50-90% ошибок (обнаруживаемых за все время жизни ПО) Нужны настоящие эксперты, программисты с менее чем 10-летним стажем могут участвовать лишь как обучающиеся 6

7 Тестирование Оценка корректности системы по ее работе в выбранных ситуациях, с определенными данными Техники: –Шаблоны сценариев, перебор и фильтрация –Синтез тестов по структуре реализации или модели Производительность : сильно зависит от целей, техники, опыта и пр. –Microsoft : производительность разработки тестов и тестирования примерно такая же, как у создателей кода, 10 строк/час Результаты : выявляется 30-80% ошибок Часто используется неопытный персонал, что отрицательно сказывается на качестве 7

8 Пример : проект DMS (ИСП РАН) Разработка тестов для ОС телефонного коммутатора Nortel Networks с использованием формальных методов Размер системы : строк, 230 интерфейсных функций Трудоемкость : ~ 10 человеко-лет Результаты: –Тестовый набор использовался для проверки всех новых версий ОС –> 300 ошибок в системе с заявленной надежностью % –12 ошибок, требующих холодного рестарта –~ 50% всех ошибок найдены в ходе экспертизы –Остальные выявлены тестами, сгенерированными из формальных спецификаций и нацеленными на их покрытие 8

9 Показатели качества тестирования Метрики тестового покрытия –Функциональности программы и требований –Структуры кода: строк, ветвлений, комбинаций условий в ветвлениях Для адекватной оценки нужно сочетание нескольких метрик Примеры достигаемого тестового покрытия : –Обычное коммерческое ПО : 15-20% ветвлений в коде –Системное ПО : 60-80% ветвлений в коде –Тесты на базе формальных моделей : 70-80% ветвлений в коде –Аналитическая верификация : 100% ветвлений в коде 9

10 Аналитическая верификация Формальное описание семантики программы и требований и доказательство выполнения требований Техники: –Метод Флойда (дедуктивный метод) –Provers, solvers, интерактивные инструменты Инструменты: –Мировые лидеры: PVS, Isabelle/HOL, Frama-C Примеры приложений: микропроцессоры, ядро операционной системы seL4 Опыт ИСП РАН: практикум по верификации с помощью Frama-C (~ 100 человеко-часов на программу размером порядка 100 строк) 10

11 Пример: верификация ядра ОС seL4 Ядро встроенной ОС seL4 –8700 строк на C, 600 строк на ассемблере –Для реализации ~2.5 человеко-года Верификация – строк формальной модели –Инструмент: Isabelle/HOL –Трудоемкость – 20 человеко-лет (12 чел.) Доказано ~10000 лемм 11

12 Статический анализ программ 12

13 f(char * p) {char s[6]; strcpy(s,p); } main1 () {f(hello); } main2 () {f(privet); } \0 o l l e h t e v i r p Стек после выполнения функции f, вызванной из main1 массив s Стек после выполнения функции f, вызванной из main2 В случае main2 адрес возврата перезапишется и управление будет передано не на main2, а на другой участок кода адрес возврата На место адреса main2 записали лишний байт Адрес main1 Простейший пример 13

14 Альтернативы решения Тестирование Проверки времени выполнения Статический анализ программы Смешанный 14

15 Можно использовать специальные функции с дополнительными параметрами – ограничениями сверху на объем записываемой информации. Например, вместо strcpy(a,b) использовать strncpy(a,b,n), где n- максимальное количество переписываемых символов Вставка проверок подразумевает инструментацию исходного кода и так как такие проверки должны присутствовать во всех потенциально опасных местах, инструментированный код может работать на порядок медленнее исходного f(char * p) {char s[10]; strcpy(s,p) ; } f(char * p) {char s[10]; if (strlen(p)

16 От динамической защиты к статическому обнаружению Даже в случае минимизации количества проверок инструментированный код работает гораздо медленнее исходного Среди вставляемых проверок много «бесполезных», то есть тех, которые проверяют заведомо истинные условия Необходимо статически обнаружить в тексте программы только те места, в которых действительно возможно нарушение системы защиты 16

17 Цели статического анализа – выявление дефектов в программах Дефекты (ситуации в исходном коде) могут приводить к: Уязвимостям защиты Потере стабильности работы программы Уязвимость защиты (security vulnerability) – ошибка в тексте программы, которая позволяет пользователю при некоторых сценариях использования программы обходить средства разграничения прав доступа программы или ОС, в которой программа выполняется. 17

18 Рассматриваемые виды дефектов Переполнение буфера Format string: недостаточный контроль параметров при использовании функций семейства printf/scanf Tainted input: некорректное использование непроверяемых на корректность пользовательских данных Разыменование нулевого указателя Утечки памяти Использование неинициализированных данных 18

19 Преимущества статического анализа Автоматический анализ многих путей исполнения одновременно Обнаружение дефектов, проявляющихся только на редких путях исполнения, или на необычных входных данных (которые могут быть установлены злоумышленником в процессе атаки) Возможность анализа на неполном наборе исходных файлов Отсутствие накладных расходов во время выполнения программы 19

20 Первое поколение анализаторов Flowfinder, ITS4, RATS, Pscan (распространяются бесплатно) CodeSurfer (инструмент для обнаружения уязвимостей на базе CodeSurferа недоступен) FlexeLint (продается на рынке), Splint (распространяется бесплатно) 20

21 Недостатки первого поколения Большое число ложных срабатываний – 90% и выше Пропуск реальных уязвимостей Необходима ручная проверка результатов работы, которая требует привлечения значительных ресурсов (материальных, людских, временных) 21

22 Современные анализаторы Coverity Prevent Klockwork Insight Svace 22

23 Наш подход Для обнаружения уязвимостей мы предлагаем применять следующее: Межпроцедурный data-flow анализ с итерациями на внутрипроцедурном уровне Анализ указателей Анализ интервалов и значений целочисленных объектов Контекстно-зависимый (использующий индивидуальные входные параметры для каждой точки вызова) анализ 23

24 Целью целочисленного анализа программы является получение необходимой информации о значении целочисленных атрибутов объектов программы (значение переменной, размер массива и т.д.) Чем точнее и полнее представляются целочисленные значения, тем точнее возможно проведение поиска уязвимостей void f(int i) { char p[5]; int a; if (i>0) a=4; else a=3; p[a]=0; } i>0 a=4a=3 p[a]=0 yesno Value(a)=3Value(a)=4 Value(a)=[3..4] - нет уязвимости Целочисленный анализ на основе интервалов 24

25 Потеря точности в некоторых случаях. Отсутствие информации о связях между переменными: в случае анализа на основе интервалов в последней инструкции примера будет обнаружена ложная уязвимость. void f(int i) { char p[5]; int a,b,c; if (i>0) a=0; else a=1; b=a+4; c=b-a; p[c]=0 } i>0 a=0a=1 b=a+4 yesno Value(a)=1Value(a)=0 Value(a)=[0..1] c=b-a p[c]=0 Value(a)=[0..1] Value(b)=[4..5] Value(c)=[3..5] Value(a)=[0..1] Value(b)=[4..5] Value(a)=[0..1] Value(b)=a+4 Value(a)=[0..1] Value(b)=a+4 Value(c)=4 Size(p)=5 Value(c) ложная ошибка Недостатки целочисленного анализа интервалов 25

26 Необходимость межпроцедурного анализа f(char *p, char *s) {strcpy(p,s); // произойдет копирование 6 байт, включая //конец строки } main() {char *p; p=malloc(5); f(p,hello); } В приведенном примере указатель на объект размером 5 байт передается в функцию f, поэтому без межпроцедурного анализа эта информация никаким образом не попадет на вход вызову функции strcpy и ошибку не зафиксируется 26

27 Необходимость анализа указателей … char a[10]; char * p; p=a; p[10]=0; … Для данного примера в случае отсутствия анализа указателей невозможно сделать никаких предположений о размере массива, на который указывает p и, следовательно, невозможно определить наличие ошибки 27

28 Спецификация окружения char* strcpy(char *dst, const char *src) { char d1 = *dst;//dst и src char d2 = *src;// разыменовываются в функции //необходимо проверить на корректность src //(в случае пользовательского ввода) sf_set_trusted_sink_ptr(src); //содержимое src копируется в dst sf_copy_string(dst, src); //возвращается входной параметр return dst; } 28 Внутренние обработчики инфраструктуры анализа

29 Схема работы Svace Анализируемая программа Система сборки Файлы с исходным кодом Утилита перехвата Компилятор LLVM-GCC или CLANG Исходный код Измененная командная строка Командная строка Биткод-файл Входные биткод-файлы Биткод-файлы для исходных файлов Биткод-файлы спецификаций библиотек Инфраструктура анализа Детекторы Вызовы внутреннего интерфейса Инструмент статического анализа Биткод-файлы Исходный код Работа с результатами анализа через компонент Eclipse Список предупреж- дений Биткод-файл 29

30 Построение аннотаций Биткод-файлы для исходных файлов Спецификации библиотечных функций на языке Си Биткод-файлы спецификаций библиотек Компилятор LLVM- GCC или CLANG Функции анализируемой программы Функции спецификаций Построение графа вызовов Аннотации Анализ Анализ* *Анализ отдельной функции Анализ вызова функции Вызов подпрограммы 30

31 Топологический порядок обработки функций Граф вызовов функции main qw a b c prinf strcpy Построение топологического порядка функций abcqwmain Порядок анализа Создание аннотаций библиотечных функций printf strcpy aqb Анализ функции c Аннотации : Межпроцедурный анализ (интервальный, tainted, нулевых указателей, алиасов и др.) 31

32 Время анализа ПроектСтрок Си и Си++ кода Время анализа* Строк в секунду libxml с 134 gperf с 197 aide с 240 ffmpeg м 20 с944 gstreamer м 43 с625 qtiplot м 07 с517 openssl м 51 с 202 postgresql м 38 с355 firefox ч 35 м 40 с306 android11 млн.13 ч 58 м218 * Не учитывается время компиляции проекта 32

33 Сравнение с Coverity Prevent Тип предупрежденияИстинные срабатывания Svace Истинные срабатывания Prevent Воспроизведено истинных срабатываний Prevent, % Переполнение буфера60%10%100% Работа с динамически выделенной памятью 50%70%20% Разыменование NULL70%60%50% Испорченный ввод70% 80% Неинициализированные данные 60%40%50% Несоотвестие типов возвращаемых значений 60%90%30% Состояние гонки90% 80% Передача по значению100% Другие (более 30)50%70%30% 33

34 Текущее состояние Анализ программ на Си\Си++. Информация об исходном коде собирается при помощи компилятора LLVM-GCC (или CLANG) Нет ограничений на размер программы (линейная масштабируемость) Полностью автоматический анализ Поддержка пользовательских спецификаций функций Набор спецификаций стандартных библиотечных функций (Си, Linux) Набор подсистем поиска различных дефектов (переполнение буфера, разыменование нулевого указателя и др.) Набор подсистем поиска дефектов расширяем Графический пользовательский интерфейс, реализованный в виде расширения среды Eclipse 34

35 Avalanche: Обнаружение ошибок при помощи динамического анализа 35

36 Динамический и статический анализ кода Динамический анализ - анализ программы во время выполнения Статический анализ - анализ без выполнения программы 36

37 Обнаружение ошибок при помощи анализа программ Динамический анализ –Требуется набор входных данных и/или среда выполнения –Высокие требования к ресурсам –Высокая точность обнаружения Статический анализ –Работает на исходном или бинарном коде –Анализ абстрактной модели –Хорошая масштабируемость –Ложные срабатывания 37

38 Valgrind Фреймворк динамической инструментации Обнаруживаемые ошибки: –Утечки памяти –Ошибки работы с динамической памятью –Неиницилизированные данные –Ошибки в многопоточных программах 38

39 Valgrind: общая схема работы Команды CPU Базовый блок Valgrind IR Плагин Инструментация Базовый блок Valgrind IR Команды CPU Внутреннее представление команд Valgrind – абстрактная RISC машина 39

40 Трасса выполнения программы 40

41 Трасса выполнения программы 41

42 Трасса выполнения программы 42

43 Трасса выполнения программы 43

44 Работы в этой области EXE tool, Stanford University - символические вычисления SAGE framework, Microsoft Research - white-box fuzz testing KLEE, LLVM project 44

45 Пример char *names[] = { one, two,...}; char buf[3]; fread(buf, 3, 1, f); // чтение 3-х байт из файла if (buf[0] == 1) { // ветвление #1 int index; if (buf[1] + buf[2] > 0) { // ветвление #2 index =...; } name = names[index]; // index не инициализирован // выход за границы массива... } else {... } 45

46 Пример fread(buf, 3, 1, f) buf[0] == 1 buf[1] + buf[2] > 0 x1, x2, x3: byte x1 = 1 x2 + x3 > 0 x1 = 1 x2 = 100 x2 =

47 Пример fread(buf, 3, 1, f) buf[0] == 1 buf[1] + buf[2] > 0 Система уравнений: x1, x2, x3: byte ¬(x1 = 1) x1 = 2 Решение: 47

48 Пример fread(buf, 3, 1, f) buf[0] == 1 buf[1] + buf[2] > 0 Система уравнений: x1, x2, x3: byte x1 = 1 ¬(x2 + x3 > 0) x1 = 1 x2 = 0 x3 = 0 Решение: 48

49 Avalanche Отслеживает поток помеченных (потенциально опасных) данных Изменяет входные данные, чтобы спровоцировать ошибку, или обойти новые части программы Обнаруживает критические ошибки - разыменование нулевого указателя, деление на ноль, неинициализированные данные, ошибки работы с памятью Генерирует набор входных данных для каждой найденной ошибки 49

50 Входные данные \ Avalanche: итерация Tracegrind Трасса Управляющий модуль Трасса STP Решение Управляющий модуль Входные данные Covgrind Метрики Управляющий модуль 50

51 Управляющий модуль Avalanche Координация работы других компонентов Обход различных путей исполнения программы, инвертирование условий Поддержка параллельного и распределенного анализа 51

52 Tracegrind Отслеживает поток помеченных данных в программе Все данные прочитанные из внешних источников (файлы, сетевые сокеты, аргументы коммандной строки, переменные окружения) Переводит трассу выполнения в булевскую формулу (STP утверждения) 52

53 Tracegrind Моделирует оперативную память, регистры и временные переменные при помощи бит-векторов Моделирует комманды при помощи операций и утверждений STP 53

54 Covgrind Вычисление метрики покрытия кода программы (количество новых ББ покрытых на текущей итерации) Перехват сигналов (обнаружение критических ошибок) Обнаружение ошибок работы с памятью при помощи Memcheck Обнаружение бесконечных циклов при помощи таймаутов 54

55 STP - Simple Theorem Prover SAT решатель (основан на MiniSat) Проект с открытым исходным кодом Поддерживает бит-векторы, широкий набор операций 55

56 Проект Опубликован на Google Code Лицензии: –Valgrind и Memcheck - GPL v2 –STP - MIT license –Драйвер Avalanche, Tracegrind, Covgrind - Apache license 56

57 Avalanche: возможности Поддержка клиентских сетевых сокетов Поддержка переменных окружения и параметров коммандной строки Поддержка платформ х86/Linux и amd64/Linux, ARM/Linux, Android Поддержка параллельного и распределенного анализа 57

58 Результаты Более 15-ти ошибок на проектах с открытым исходным кодом Ошибки подтверждены и/или исправлены разработчиками Проект Тип ошибок mencoderNPD wgetNPD swtoolNPD libmpeg2DBZ gnashUE audiofileIL libsndfileDBZ libjpegDBZ libmpeg3NPD libquicktimeNPD, IL libwmfNPD monoNPD parrotNPD, IL llvmNPD Null Pointer Dereference (разуменование нулевого указателя) = NPD Division By Zero (деление на ноль) = DBZ Unhandled Exception (необработанная исключительная ситуация) = UE Infinite Loop (бесконечный цикл) = IL 58

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

60 UniTESK 60

61 Случай тестирования отдельной функции: –Подобрать набор входных (тестовых) данных –Вычислить ожидаемый результат для каждого из тестовых данных А если это трудно или невозможно, например для функции random() ? –Запустить тест с каждым из тестовых данных, сопоставить результат с ожидаемым –Принять решение о продолжении или завершении тестирования А каков критерий завершения ? Разработка теста по-простому 61

62 Случай тестирования группы функции, класса/объекта, модуля с несколькими интерфейсами (обычно есть переменные состояния и побочный эффект): –Подобрать набор входных (тестовых) данных для каждой функции –Вычислить ожидаемый результат для каждого из тестовых данных Новая проблема – как учесть побочный эффект? –Вызвать каждую функцию с каждым из тестовых данных в различных состояниях модуля, сопоставить результат с ожидаемым Какие состояния считать различными, как прийти в нужное состояние (построить тестовую последовательность), если побочный эффект вычислить невозможно? –Принять решение о продолжении или завершении тестирования А каков критерий завершения ? Разработка теста по-простому (2) 62

63 Типичные размеры тестовых наборов Ядро ОС Linux (LTP) –18 Mbyte (при этом покрывает менее половины строк кода) Библиотеки стандарта OS Linux (LSB) –Более 100 тысяч вариантов –Более 80 Mbyte Для компилятора C (например, ACE или Perennial) –Более тысяч вариантов –Более 1 Gbyte 63 Не удивительно, что на тестирование тратиться существенная доля усилий (в Майкрософте около 70%), а средняя плотность ошибок, которая считается приемлемой – 2-3 ошибки на 1 тысячу строк кода.

64 Решения UniTESK Исходная точка построения теста – формализация программного контракта в форме пред- и пост-условий –пред- и пост-условия определяют тестовые оракулы и критерии полноты покрытия Тестовую последовательность конструировать не вручную, а на основе интерпретации модели теста Нотации – максимально приближенные к языкам программирования 64

65 Формализация требований Выделение модельного состояния Описание формального контракта операций –Предусловия – задают область определения –Постусловия – задают основные ограничения на результаты работы операций –Инварианты – ограничения целостности данных, общая часть всех пред- и постусловий –Аксиоматическая часть контракта (если нужно) 65

66 Простой пример спецификации в JavaTESK public specification class SqrtSpecification { public specification double sqrt(double x) { pre { return x >= 0; } post { branch SingleCase; return sqrt * sqrt == x; } public specification int sqrt(int x) { pre { return x >= 0; } post { branch SingleCase; return sqrt * sqrt x ; } 66

67 Общая схема тестирования Тестовая система Тестируемая система Отчеты Тестовый сценарий Тестовые данные Ожидаемые результаты, критерии полноты 67

68 Общая схема. Данные, оракул, покрытие Пред-условия, итераторы Пост-условия Тестовая система Отчеты Тестовый сценарий Тестовые данные Ожидаемые результаты, критерии полноты Тестируемая система 68

69 Общая схема. Тестовый сценарий описать и обойти КА обходить и строить КА налету Тестовая система Отчеты Тестовый сценарий Тестовые данные Ожидаемые результаты, критерии полноты Тестируемая система написать вручную Варианты: 69

70 Общая схема UniTESK Модель состояния Обходчик автоматов Оракулы Генератор Итераторы данных Метрика покрытия Тестируемая система Генерация тестовой последовательности налету Предусловия- фильтры Постусловия Оракул Отчеты 70

71 Применение UniTESK Операционные системы –Ядро ОС телефонной станции –Linux Standard Base –Тестовый набор для ОС 2000 (НИИСИ) Протоколы –IPv6 Microsoft Research –Мобильный IPv6 (в Windows CE 4.1) –IPv6 Октет2002 –Тестовый набор для IPsec –Тестовый набор для SMTP2010 Оптимизаторы компиляторов Intel Оптимизатор трансляции графических моделей 2005 Информационные системы –Компоненты CRM-системы2004 –Биллинговая система и EAI2005-… Микропроцессоры –Процессоры Комдив 64 (НИИСИ) –Компоненты процессоров и шин (МЦСТ)

72 Спасибо! 72