Symbolic Liveness Analysis of real-world software building upon KLEE to detect liveness violations (e.g. infinite loop bugs)
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
cmake
docs
examples
include
lib
runtime
scripts
test
tools
unittests
utils
.clang-format
.codecov.yml
.dockerignore
.gitattributes
.gitignore
.travis.yml
CMakeLists.txt
LICENSE.TXT
NEWS
README-CMake.md
README-KLEE.md
README.md
TODO.txt

README.md

Symbolic Liveness Analysis of Real-World Software

In Symbolic Liveness Analysis, we extended KLEE, a popular Symbolic Execution engine, for the detection of liveness violations. To this end, we defined a generic and practically useful livenss violation for real-world software:

A program is live iff it always eventually consumes input or terminates. [1]

This liveness property allows us to detect infinite loop bugs, while excluding intentional infinite loops, such as event loops in GUI or server applications.

For detection, we constructed a fingerprinting scheme that allows us to efficiently compute and update fingerprints of symbolic execution states, which can then be compared against each other.

Additional information on our technique can be found in our paper [1], as well as an evaluation of its runtime and memory overhead.

Bugs Found

During our evaluation on GNU Coreutils, BusyBox, toybox and GNU sed, we found a total of five previously undiscovered software defects:

In addition, we identified a bug in the long decommissioned GNU regex, which is still used in klee-uclibc by default:

Requirements

We recommend to compile our version of KLEE against LLVM 3.8.1. For information on how to compile KLEE in general, please refer to README-CMake.md.

In addition to the usual requirements of KLEE, we use CryptoPP (Version 7.0.0) to generate BLAKE2b hashes (for fingerprint creation). If CMake does not find CryptoPP, it automatically switches to a SHA1 implementation included in this repository.

If CryptoPP is located at a custom location on your system, you can use the following to tell CMake where to find it:

cmake [...] -DCRYPTOPP_INCLUDE_DIRS="/path/to/CryptoPP/include" -DCRYPTOPP_LIBRARIES="/path/to/CryptoPP/libcryptopp.so"

In addition, make sure that KLEE can find libcryptopp.so in the library path at runtime.

Usage

To use our analysis, we added the following options to KLEE:

-detect-infinite-loops

Enable detection of infinite loops (default=false)

-debug-infinite-loop-detection={state:stderr,trace:stderr}

Log all MemoryState / MemoryTrace information to stderr

-infinite-loop-detection-truncate-on-fork

Truncate memory trace (used for infinite loop detection) on every state fork (default=true)

-infinite-loop-detection-disable-two-predecessor-optimization

Disable infinite loop detection optimzation that only starts searching for loops on basic blocks with at least two predecessors (default=false)

CAV 2018 Artifact Evaluation

Along with submission to CAV 2018, we prepared an artifact for evaluation, which can be obtained through the following links:

Publication

If you use any portion of Symbolic Liveness Analysis in your work, please cite the following paper:

[1] Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus Wehrle. Symbolic Liveness Analysis of Real-World Software. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18). Lecture Notes in Computer Science, vol 10982. Springer, Cham

BibTeX:

@inproceedings {SymbolicLivenessAnalysis,
   author = {Schemmel, Daniel and B{\"{u}}ning, Julian and Soria Dustmann, Oscar and Noll, Thomas and Wehrle, Klaus},
   title = {{Symbolic Liveness Analysis of Real-World Software}},
   booktitle = {Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18)},
   pages = {447--466},
   series = {Lecture Notes in Computer Science},
   volume = {10982},
   publisher = {Springer},
   address = {Cham},
   year = {2018}
}