Пределы кли (инструмент анализа программы LLVM)
http://klee.llvm.org/ - это инструмент анализа программ, который работает с помощью символьного выполнения и решения ограничений, находит возможные входные данные, которые могут вызвать сбой программы, и выводит их в качестве тестовых случаев. Это чрезвычайно впечатляющий пример разработки, который дал некоторые хорошие результаты на данный момент, в том числе обнаружение ряда ошибок в наборе реализаций утилит Unix с открытым исходным кодом, которые считались одними из самых тщательно протестированных программ, когда-либо написанных.
Мой вопрос: что он не делает?
Конечно, любому такому инструменту присущи ограничения, по которым он не может прочитать мысли пользователя и угадать, каким должен быть результат. Но оставляя в стороне невозможное в принципе, большинство проектов еще не используют Klee; Каковы ограничения текущей версии, какие ошибки и рабочие нагрузки она еще не может обработать?
3 ответа
Как я могу сказать после прочтения http://llvm.org/pubs/2008-12-OSDI-KLEE.html
Он не может проверить все возможные пути большой программы. Не удалось даже на sort полезность. Эта проблема - проблема остановки (неразрешимая проблема), а KLEE - эвристика, поэтому она может проверять только некоторые пути за ограниченное время.
Он не может работать быстро, согласно статье, для генерации тестов для 141000 строк кода в COREUTILS понадобилось 89 часов (с использованием в них кода libc). А самая большая отдельная программа имеет всего ~10000 строк.
Он ничего не знает о плавающей точке, longjmp/setjmp, потоках, asm; объекты памяти переменного размера.
Обновление: / из блога llvm / 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 отслеживает все случаи использования символической памяти.
В целом, KLEE должен быть довольно хорошим символическим механизмом исполнения для академических исследований. Для использования на практике это может быть ограничено следующими аспектами:
[1] Модель памяти, используемая ИК-интерпретатором LLVM в 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 не обязательно требует инструментария над программой для маркировки символических переменных. Как упоминалось выше, символические значения могут быть введены в программу через командные строки. На самом деле, пользователи также могут указывать файлы как символические. При необходимости пользователи могут просто использовать функции библиотеки, чтобы сделать ввод символическим (один раз для всех).
Я разочарован Klee тем, что у него нет встроенной поддержки структур данных. Сам Клее не понимает, что такое связанный список. Вы не можете использовать его для проверки реализации какого-либо графового алгоритма. Кроме того, он не может помочь обнаружить ошибки переполнения интергератора, которые являются наиболее важным источником исправлений безопасности.