As mentioned in the overview of KLEE’s basic command-line options, KLEE provides several options as part of its symbolic environment. Their usage, however, is often not easily understood by new users. This tutorial provides basic usage examples for -sym-arg and -sym-files, which are perhaps the most essential among the options.
We note that -sym-arg <N> provides a command-line argument of length N to the program under test. Its variant -sym-args <MIN> <MAX> <N> provides at least MIN arguments and at most MAX symbolic arguments, each with maximum length N. To demonstrate -sym-arg, let us first consider the following program password.c that checks its command-line argument for a match with a hard-coded password.
To enable symbolic environment, KLEE has to be given the -posix-runtime option. We run KLEE given the bitcode of password.c as input and using -sym-arg option as follows.
As can be seen, due to the command-line argument being symbolic, KLEE executed six paths, with one of the path having the command-line argument match the password.
The option -sym-files <NUM> <N> creates NUM symbolic files, where the first file is named ‘A’, the second ‘B’, and so on, each with size N. Its sibling options -sym-stdin and -sym-stdout make the standard input and output symbolic, respectively.
Let us now consider a password checker, still called password.c that reads a string from a file specified by the user and checks if it matches a hard-coded password. If the file name is not specified, or if there is an error when opening the file, it reads the string from the standard input.
We now run the program using KLEE. For the program not to get stuck trying to read data, we need to provide some input. In our first run, we provide a symbolic standard input using -sym-stdin option. The symbolic input will make KLEE explore the path with successful password check.
We have now discovered the password using KLEE.
Our program can also read the password from a disk file, but we want to read a file with symbolic content so that KLEE executes the path where the password check is successful. The -sym-files option provides several such files named ‘A’, ‘B’, ‘C’, and so on. By specifying the option -sym-files 1 10 below, we ask KLEE to provide one symbolic file of size 10 bytes, and that file is named ‘A’ by KLEE. We therefore provide this file name as an argument to our program.
The password was successfully read from the symbolic file A in one of the execution paths.