Пределы Klee (инструмент анализа программ LLVM)

http://klee.llvm.org/ - это инструмент анализа программ, который работает благодаря символическому исполнению и решению ограничений, нахождение возможных входов, которые могут привести к сбою программы, и вывод их в качестве тестовых примеров. Это чрезвычайно впечатляющая часть техники, которая до сих пор дала хорошие результаты, включая обнаружение множества ошибок в коллекции программных средств Unix с открытым исходным кодом, которые считались одним из наиболее тщательно протестированных программ, когда-либо написанных.

Мой вопрос: что он не делает?

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

Ответ 1

Как я могу сказать после прочтения http://llvm.org/pubs/2008-12-OSDI-KLEE.html

Невозможно проверить все возможные пути большой программы. Это не удалось даже в утилите sort. проблема - проблема с остановкой (неразрешимая проблема), а KLEE - эвристика, поэтому она может проверять только некоторые пути за ограниченное время.

Он не может работать быстро, согласно бумаге, потребовалось 89 часов для создания тестов для 141000 строк кода в COREUTILS (с использованием кода libc в них). И самая большая одиночная программа имеет только ~ 10000 строк.

Он ничего не знает о плавающей запятой, longjmp/setjmp, threads, asm; объекты памяти переменного размера.

Обновление:/из llvm blog/http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html

5. Подпроект LLVM "Klee" использует символический анализ, чтобы "попробовать каждый возможный путь" через кусок кода, чтобы найти ошибки в коде, и он создает тестовый файл. Это большой маленький проект, который в основном ограничен, не будучи практичным для работы на крупномасштабных приложениях.

Update2: KLEE требует, чтобы программа была изменена. http://t1.minormatter.com/~ddunbar/klee-doxygen/overview.html

. Символическая память определяется введением специальных вызовов в KLEE (а именно klee_make_symbolic). Во время выполнения KLEE отслеживает все использование символической памяти.

Ответ 2

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

[1] Модель памяти, используемая ИК-интерпретатором LLVM в KLEE, занимает много времени и занимает много времени. Для каждого пути выполнения KLEE поддерживает частное "адресное пространство". Адресное пространство поддерживает "стек" для локальных переменных и "кучу" для глобальных переменных и динамически распределенных переменных. Однако каждая переменная (локальная или глобальная) обернута в объект MemoryObject (MemoryObject поддерживает метаданные, связанные с этой переменной, такие как начальный адрес, размер и информация о размещении). Размер памяти, используемой для каждой переменной, будет размером исходной переменной плюс размер объекта MemoryObject. Когда нужно получить доступ к переменной, KLEE сначала ищет "адресное пространство", чтобы найти соответствующий объект MemoryObject. KLEE проверит MemoryObject и посмотрит, законен ли доступ. Если это так, то доступ будет завершен, и состояние MemoryObject будет обновлено. Такой доступ к памяти, очевидно, медленнее, чем оперативная память. Такая конструкция может легко поддерживать распространение символических ценностей. Тем не менее, эта модель может быть упрощена путем изучения анализа taint (обозначение символьного статуса переменных).

[2] В KLEE отсутствуют модели для системных сред. Единственным системным компонентом, смоделированным в KLEE, является простая файловая система. Другие, такие как сокеты или многопоточность, не поддерживаются. Когда программа вызывает системные вызовы для этих немодулированных компонентов, KLEE либо (1) завершает выполнение, либо вызывает предупреждение, либо (2) перенаправляет вызов на базовую ОС (проблемы: символические значения должны быть конкретизированы, а некоторые пути будут пропущенные системные вызовы из разных путей исполнения будут мешать друг другу). Полагаю, это причина того, что "он ничего не знает нитей", как упоминалось выше.

[3] KLEE не может напрямую работать с двоичными файлами. KLEE требует LLVM IR тестируемой программы. В то время как другие инструменты Symbolic Execution, такие как S2E и VINE из проекта BitBlaze, могут работать с двоичными файлами. Интересно, что проект S2E полагается на KLEE как на его символический механизм выполнения.

Что касается вышеприведенного ответа, у меня лично разные мнения. Во-первых, верно, что KLEE не может отлично работать с крупномасштабными программами, но какой символический инструмент выполнения может? Взрыв пути - скорее теоретическая открытая проблема, а не инженерная проблема. Во-вторых, как я уже упоминал, KLEE может работать медленно из-за своей модели памяти. Однако KLEE не замедляет выполнение ни для чего. Он консервативно проверяет повреждение памяти (например, переполнение буфера) и записывает набор полезной информации для каждого исполняемого пути (например, ограничения на входные данные, которые следуют по пути). Кроме того, я не знал других символических инструментов исполнения, которые могут работать очень быстро. В-третьих, "плавающие точки, longjmp/setjmp, потоки, asm, объекты памяти переменного размера" - это просто инженерные работы. Например, автор KLEE фактически сделал что-то, что позволило KLEE поддерживать плавающую точку (http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf). В-третьих, KLEE не обязательно требует инструментария для обозначения символических переменных. Как упоминалось выше, символические значения могут быть переданы в программу через командные строки. Фактически, пользователи могут также указывать файлы, которые должны быть символическими. При необходимости пользователи могут просто выполнять функции библиотеки, чтобы сделать ввод символическим (один раз для всех).