1# An Introduction to Symbolic Execution23Material for an introduction to [symbolic execution], a [presentation at Hackover'26][HO26].45<!-- TODO: Reference the media.ccc.de recording here. -->67This repository includes the files required to experiment with the live demonstration from the presentation.8Specifically, it includes the setup required to verify the [Base64] implementation provided by the [RIOT operating system][RIOT].9The original, unmodified source code is [available on GitHub][RIOT base64].1011## Usage1213Ideally, use this repository with [Guix](https://guix.gnu.org):1415 $ guix time-machine -C channels.scm -- shell -m manifest.scm1617Within the Guix shell run the following commands:1819 $ make sim2021Alternatively, you can also try to use [KLEE's Docker image]:2223 $ docker run --rm -v "$(pwd):/code" -it klee/klee2425Within the container run:2627 $ cd /code28 $ make sim2930## Tweaking the Example3132The example uses a fixed-size input buffer, defaulting to 3 bytes.33The size can be configured through the `INPUT_SIZE` variable, for example:3435 $ INPUT_SIZE=2 make -B3637For an input size of 3 bytes, 625 execution paths should be discovered.38On my hardware, this takes around 2 minutes.39Depending on the size, the number of execution paths, and the time required to discover them will vary.4041Further, it is possible to experiment with various KLEE optimizations to speed up this example.42A technique particularly beneficial to this example is [state merging].43To enable state merging, invoke `make` as follows:4445 $ CFLAGS=-DKLEE_STATE_MERGING make -B4647This will merge multiple execution paths of `getsymbol` / `getcode` into a single conjugated SMT-LIB expression.48Thereby, increasing SMT-LIB query complexity but reducing the number of execution paths.4950To play around with other optimizations, refer to the [KLEE documentation].5152## More Information5354The following material provides more background information:5556* [Symbolic Execution for Software Testing: Three Decades Later](https://doi.org/10.1145/2408776.2408795)57* [A Survey of Symbolic Execution Techniques](https://doi.org/10.1145/3182657)5859Further, the [KLEE documentation] includes additional practical examples:60611. [Testing a Regular Expression Library]622. [Testing GNU coreutils]6364[symbolic execution]: https://notes.8pit.net/notes/xg1j.html65[HO26]: https://talks.hackover.de/ho26/talk/CKUL8T/66[Guix]: https://guix.gnu.org67[KLEE's Docker image]: https://hub.docker.com/r/klee/klee68[Base64]: https://doi.org/10.17487/RFC464869[RIOT]: https://riot-os.org70[RIOT base64]: https://github.com/RIOT-OS/RIOT/blob/2026.04/sys/base64/base64.c71[state merging]: https://arxiv.org/pdf/1610.00502#page=2272[KLEE documentation]: https://klee-se.org/releases/docs/v3.2/docs/73[Testing a Regular Expression Library]: https://klee-se.org/tutorials/testing-regex/74[Testing GNU coreutils]: https://klee-se.org/releases/docs/v3.2/tutorials/testing-coreutils/