Как использовать символьное выполнение для поиска ошибки, например SAGE,KLEE,S2E

Question

Как и в заголовке, кто-нибудь знает разницу в способах использования этих инструментов для поиска ошибок? Возможно, kLEE и SAGE могут найти доступ за пределами границ и переполнение буфера, KLEE может использовать утверждения, но есть ли другие способы?

Answer 1

Ваш вопрос очень общий. Я рекомендую прочитать научные статьи и документацию для углубленной информации.

Тем не менее, SAGE в основном использует Concolic Execution, в то время как KLEE использует (vanilla) символическое выполнение. S2E по-прежнему отличается от них (хотя и является отдаленным форком KLEE) тем, что использует динамическое переключение между символьным и конкретным исполнением, используя jit, который позволяет трансляцию на лету между QEMU-BC и LLVM-BC.

Это относится к принципиальной разнице в парадигме исполнения, используемой этими конкретными инструментами, но, очевидно, она может только поцарапать поверхность.

Для конечного пользователя одно существенное различие заключается в том, что KLEE должен быть скомпилирован с конкретным компилятором, способным генерировать код llvm (например, llvm-gcc или clang), и разработчик должен возиться с системой сборки. Обычно это означает, что KLEE ограничен простым C. S2E не заботится о том, какой язык вы используете, и вы можете запускать скомпилированные двоичные файлы, но недостатком является то, что некоторые переполнения буфера не могут быть обнаружены, а выполнение немного медленнее (до фактора 100x). Это зависит от того, что вы пытаетесь проанализировать.