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

Question

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

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

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

Answer 1

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

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

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

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

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

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

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

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

Answer 2

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

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

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

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

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