Documentation
Learn How to Use KLEE
NOTE: This is the documentation for KLEE 3.1, which might differ from the latest version of KLEE from the master branch. For documentation relevant to KLEE’s master branch see the homepage.
If you have a question on using KLEE:
- Please first check the documentation below
- Then check the searchable mailing list archive
- If this still doesn’t answer your questions then:
- If you think it is a bug, please open an issue on GitHub
- If it is a general question, then please send an email to the klee-dev mailing list
Usage
- Intrinsics: Overview of the main KLEE intrinsic functions.
- KLEE Options: Overview of KLEE’s main command-line options.
- Generated Files: Overview of the main files generated by KLEE.
- Tools: Overview of the main auxiliary tools provided by KLEE.
- Solver Chain: Overview of the solver chain and related command-line arguments.
- Kleaver Options: Overview of Kleaver’s main command-line options.
- KQuery: The reference manual for the KQuery language, used for interacting with Kleaver.
- Coreutils Experiments: Some information about the Coreutils experiments presented in our KLEE OSDI’08 paper.
Tutorials
- First tutorial: Testing a small function.
- Second tutorial: Testing a simple regular expression library.
- Using a symbolic environment: Guide with examples on how to use the symbolic environment such as symbolic files and command-line arguments for the program under test.
- Testing Coreutils: In-depth description of how to use KLEE to test GNU Coreutils.
External Resources
We also recommend the following external resources. When using them, please take into account that they might be using old versions of KLEE.
- Symbolic execution with KLEE: A set of four instructional videos introducing KLEE, starting with how to get started with KLEE and ending with a demo that finds memory corruption bugs in real code.
- Solving a maze with KLEE: A nice explanation of how symbolic execution can be used to generate interesting program inputs. The example shows how to use KLEE to find all the solutions to a maze game.
- Keygenning with KLEE and Hex-Rays: A beginners explanation of using symbolic execution to solve a small binary’s pseudocode.
- Keygenning with KLEE: A more in-depth guide to using KLEE for key generation.
- How to generate tests automatically?: A basic introduction to symbolic execution with KLEE.
- Using KLEE to generate tests for binary search: A tutorial on using KLEE to test a binary search implementation).
- A Guide to KLEE LLVM Execution Engine Internals: A quick overview of KLEE’s internals and core classes in PoC||GTFO 0x18 (pp. 51).
- Testing Rust programs with KLEE: A collection of tools/libraries to support testing of Rust programs with KLEE.
- SAT/SMT by example: A comprehensive guide focusing on using SAT and SMT solvers, which includes lots of interesting examples involving KLEE.
- Measuring the coverage achieved by symbolic execution: A blog post that discusses the difference between the internal coverage reported by KLEE and the external coverage reported by a tool such as GCov.
- Binary symbolic execution with KLEE-Native: An extension of KLEE that analyses binaries by lifting them to LLVM IR
- SHA-3 Buffer Overflow: Finding a bug in a sha-3 implementation with KLEE