KLEE: symbolic execution for software testing

KLEE is a symbolic execution engine for LLVM: it executes programs symbolically, starting with the set of all possible inputs. At each branch point in the program, constraints are added according to the branch condition and the program is forked. For example, if (x < 10) forks into a branch with an x < 10 constraint and a branch with a x >= 10 constraint. When KLEE reaches an assertion, pointer dereference, or other unsafe operation, it uses a SMT solver to check if there are inputs that would cause the operation to fail given the current constraints.

The authors used a number of heuristics to reduce the number of SMT queries by a factor of 10. To reduce memory usage, KLEE uses copy-on-write data structures to store program state.

To allow KLEE to work on real world programs, system calls are mocked. KLEE was run against GNU Coreutils, BusyBox, the MINIX core utilities, and an operating system kernel, and found bugs in all of them. It achieved greater line coverage than all of the manually constructed test suites. KLEE can also be used to check for equivalence between two programs by calling both and asserting their output is the same. This was run on GNU Coreutils and BusyBox and to uncover correctness errors.

References

1. C. Cadar, D. Dunbar, and D. Engler, “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,” USENIX Symposium on Operating Systems Design and Implementation, vol. 8, pp. 209–224, 2008, Accessed: Apr. 10, 2020. [Online]. Available: https://llvm.org/pubs/2008-12-OSDI-KLEE.pdf
2. https://klee.github.io/