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

Question

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

Answer 1

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

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

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

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