This tutorial assumes that you have already built S2E and prepared VM image as described on the Building the S2E Framework page.
Contents
We want to cover all of the code of the following program by exploring all the possible paths through it.
#include <stdio.h>
#include <string.h>
int main(void)
{
char str[3];
printf("Enter two characters: ");
if(!fgets(str, sizeof(str), stdin))
return 1;
if(str[0] == '\n' || str[1] == '\n') {
printf("Not enough characters\n");
} else {
if(str[0] >= 'a' && str[0] <= 'z')
printf("First char is lowercase\n");
else
printf("First char is not lowercase\n");
if(str[0] >= '0' && str[0] <= '9')
printf("First char is a digit\n");
else
printf("First char is not a digit\n");
if(str[0] == str[1])
printf("First and second chars are the same\n");
else
printf("First and second chars are not the same\n");
}
return 0;
}
Before testing the program in S2E, compile and run it in the native QEMU build (the one in the i386-softmmu directory). Launch QEMU with the following command:
$ $S2EDIR/build/i386-softmmu/qemu-system-i386 your_image.raw
You need to copy the example source code into the VM. As you will likely need to do this frequently, we recommend to install either ssh or an http server on your host machine. Then you can copy the code using scp:
guest$ scp <your_login_on_host>@<your_host_name>:path/to/tutorial1.c .
guest$ scp <your_login_on_host>@<your_host_name>:path/to/s2e/guest/include/s2e.h .
Compile and run the example with the following commands:
guest$ gcc -O3 tutorial1.c -o tutorial1
guest$ ./tutorial1
Enter two characters: ab
First char is lowercase
First char is not a digit
First and second chars are not the same
In order to execute the program symbolically, it is necessary to specify what values should become symbolic. There are many ways to do it in S2E, but the simplest one is to use the S2E opcodes library. This library provides a way for guest code to communicate with the S2E system.
In order to explore all possible paths through the program that correspond to all possible inputs, we want to make these inputs symbolic. To accomplish this, we replace the call to fgets() by a call to s2e_make_symbolic():
...
char str[3];
// printf("Enter two characters: ");
// if(!fgets(str, sizeof(str), stdin))
// return 1;
s2e_make_symbolic(str, 2, "str");
str[3] = 0;
...
By default, S2E propagates the symbolic values through the program but does not fork on branches. To enable forking, call s2e_enable_forking() before making symbolic values, and s2e_disable_forking() after exploring all branches.
Finally, it would be interesting to see an example of input value that cause a program to take a particular execution path. This can be useful to reproduce a bug in a debugger, independently of S2E. For that, use the s2e_get_example() function. This function gives a concrete example of symbolic values that satisfy the current path constraints (i.e., all branch conditions along the execution path).
After these changes, the example program looks as follows:
#include <stdio.h>
#include <string.h>
#include "s2e.h"
int main(void)
{
char str[3];
// printf("Enter two characters: ");
// if(!fgets(str, sizeof(str), stdin))
// return 1;
s2e_enable_forking();
s2e_make_symbolic(str, 2, "str");
if(str[0] == '\n' || str[1] == '\n') {
printf("Not enough characters\n");
} else {
if(str[0] >= 'a' && str[0] <= 'z')
printf("First char is lowercase\n");
else
printf("First char is not lowercase\n");
if(str[0] >= '0' && str[0] <= '9')
printf("First char is a digit\n");
else
printf("First char is not a digit\n");
if(str[0] == str[1])
printf("First and second chars are the same\n");
else
printf("First and second chars are not the same\n");
}
s2e_disable_forking();
s2e_get_example(str, 2);
printf("'%c%c' %02x %02x\n", str[0], str[1],
(unsigned char) str[0], (unsigned char) str[1]);
return 0;
}
Compile and run the program as usual:
guest$ gcc -O3 tutorial1.c -o tutorial1
guest$ ./tutorial1
Illegal instruction
You see the Illegal instruction message because all s2e_* functions use special CPU opcodes that are only recognized by S2E.
To run a program in S2E, we have to write a configuration file, then reboot the system in S2E.
-- File: config.lua
s2e = {
kleeArgs = {
-- Pick a random path to execute among all the
-- available paths.
"--use-random-path=true",
-- Run each state for at least 1 second before
-- switching to the other:
"--use-batching-search=true", "--batch-time=1.0"
}
}
plugins = {
-- Enable a plugin that handles S2E custom opcode
"BaseInstructions"
}
Note: At the end of this tutorial, there is a section that shows an even simpler configuration file.
Booting the system in S2E takes a long time. Use a two-step process to speed it up. First, boot the system in the version of QEMU that has S2E disabled. Then, save a snapshot and load it in the S2E:
guest$ su -c halt # shut down qemu
$ $S2EDIR/build/qemu-release/i386-softmmu/qemu-system-i386 -net none your_image.raw.s2e
> Wait until Linux is loaded, login into the system. Then press
> Ctrl + Alt + 2 and type 'savevm 1' then 'quit'.
> Notice that we use i386-softmmu, which is the build with S2E **disabled**.
$ $S2EDIR/build/qemu-release/i386-s2e-softmmu/qemu-system-i386 -net none your_image.raw.s2e -loadvm 1 \
-s2e-config-file config.lua -s2e-verbose
> Wait until the snapshot is resumed, then type in the guest
guest$ ./tutorial1
> Notice that we use i386-s2e-softmmu, which is the build with S2E ENABLED.
After you run this command, S2E starts to symbolically execute the example. The configuration file instructs S2E to pick a random state once per second. You will see the QEMU screen content changing every second for different possible outputs of the example.
Each state is a completely independent snapshot of the whole system. You can even interact with each state independently, for example by launching different programs. Try to launch tutorial1 in one of the states again!
In the host terminal (i.e., the S2E standard output), you see various information about state execution, forking and switching. This output is also saved into the s2e-last/messages.txt log file. As an exercise, try to follow the execution history of a state through the log file.
In the previous section, we made the program run along multiple execution paths. However, each path continued to run even after the program terminated, executing operating system code. This is great to visually experience how S2E works, but in general we want S2E to stop executing each path as soon as the program to analyze terminates.
Terminating an execution path is accomplished with the s2e_kill_state() function. A call to this function immediately stops executing the current state and exits S2E if there are no more states to explore. Add a call to this function just before the program returns control to the OS. Before that, we might want to print example values in the S2E log using s2e_message() or s2e_warning() functions:
int main(void)
{
char buf[32];
memset(buf, 0, sizeof(buf));
...
...
s2e_get_example(str, 2);
snprintf(buf, sizeof(buf), "'%c%c' %02x %02x\n", str[0], str[1],
(unsigned char) str[0], (unsigned char) str[1]);
s2e_warning(buf);
s2e_kill_state(0, "program terminated");
return 0;
}
Now, resume the snapshot in QEMU with S2E disabled, edit and recompile the program, re-save the snapshot and re-load it in S2E. Your image needs to be in S2E format.
$ $S2EDIR/build/qemu-release/i386-softmmu/qemu-system-i386 -net none your_image.raw.s2e -loadvm 1
guest$ edit tutorial1.c
guest$ gcc -O3 tutorial1.c -o tutorial1
> press Ctrl + Alt + 2 and type 'savevm 1' then type 'quit'.
$ $S2EDIR/build/qemu/i386-s2e-softmmu/qemu-system-i386 -net none your_image.raw.s2e -loadvm 1 \
-s2e-config-file config.lua -s2e-verbose
guest$ ./tutorial1
Running tutorial1 this time will make S2E quickly terminate, leaving a log file that you can examine.
Please note that in case your program crashes or exits at some other point without calling s2e_kill_state(), S2E will not terminate and will continue to execute paths that returned to the system. To avoid this, you can use the s2ecmd utility (in $S2EDIR/guest). Launch it right after the invocation to the program that can crash, e.g., as follows:
guest$ ./tutorial; ./s2ecmd kill 0 "done"
The following is a minimal configuration file that you can use to run this example:
-- File: config.lua
s2e = {
kleeArgs = {}
}
plugins = {
-- Enable a plugin that handles S2E custom opcode
"BaseInstructions"
}
In this case S2E uses the default depth-first searcher (DFS). The current state will run until it is explicitely killed. After that, S2E will select another path, according to the DFS strategy. You must use s2ecmd or s2e_kill_state(), otherwise the current path will run forever and there will not be any progress.