Using SystemTap with S2E

SystemTap is a powerful tracing framework on Linux. It can intercept any function calls or instructions in the kernel and invoke custom scripts. Such scripts have full access to the system state, can leverage debugging information, etc.

SystemTap provides S2E users a flexible way of controlling symbolic execution. Users write a SystemTap script with embedded calls to S2E custom instructions. This allows injecting symbolic values anywhere, kill states based on complex conditions, etc.

In this tutorial, we describe how to build and run SystemTap on S2E. We also give several examples of useful analyses that can be achieved.

Note

This tutorial assumes the following knowledge:

  1. How to build guest images with s2e-env

  2. How to create Linux analysis projects with s2e-env

  3. How to use SystemTap

Building and running SystemTap in S2E

Using SystemTap in S2E is very simple, the workflow looks like this:

  1. Build the SystemTap probe on your host machine. This will produce a .ko file. You can conveniently do this from the provided Docker image (see below).

  2. Upload the .ko file from the host into the guest using s2ecmd get in the bootstrap.sh file. It is best to store the .ko directly in the project directory.

The S2E images built by s2e-env already have SystemTap pre-installed. If you want to customize the installed version, have a look at the image installation scripts. SystemTap is installed here.

You must build the Linux images from scratch in order to have the required Docker containers and kernel *.deb packages. If you downloaded pre-built images, delete them and rebuild them from scratch. This process will create two Docker images on your host: linux-build-i386 and linux-build-x86_64.

# Create a new analysis project on your host. This tutorial assumes a 32-bit project. Adapt the command lines
# accordingly if you need 64-bit. The --no-target option instructs s2e to create a generic project structure
# that does not target any particular binary. You will then later customize the project manually in order to
# fetch the .ko file generated by SystemTap.
host   $ cd /home/user/s2e/env
host   $ s2e new_project -n systemtap -i debian-12.5-i386 --no-target --type linux

# Start the docker container in order to build the hello world SystemTap probe
host   $ docker run --rm -ti -v $HOME:$HOME linux-build-i386

# Install the kernel packages in the running container
docker # dpkg -i /home/user/s2e/env/images/.tmp-output/linux-4.9.3-i386/*.deb

# Compile the demo probe
docker # cd /home/user/s2e/env/projects/systemtap
docker # stap -a i386 -r 4.9.3-s2e  -e 'probe vfs.read { log("hello world") exit() }' -m simple

Note

It is also possible to build the simple.ko module directly from bootstrap.sh inside the guest instead of using a Docker image on the host. However, doing so is significantly slower (up to several minutes).

At this point, you must have the /home/user/s2e/env/projects/systemtap/simple.ko file. Now it is time to update bootstrap.sh:

${S2ECMD} get simple.ko
sudo staprun simple.ko

Then, run the analysis:

host $ cd /home/user/s2e/env/projects/systemtap
host $ ./launch-s2e.sh

The analysis should finish in a few seconds and serial.txt should contain the following output:

...
Waiting for S2E mode...
... S2E mode detected
... file simple.ko of size 59076 was transferred successfully to /home/s2e/simple.ko
hello world

Creating a simple SystemTap script for symbolic execution

Warning

The following content is under construction. It may or may not work on your setup.

In this section, we show how to intercept the network packets received by the pcnet32 driver and replace the content of the IP header field with symbolic values.

Create (on the host machine) a pcnet32.stp file with the following content:

# We use the embedded C support of SystemTap to access the S2E
# custom instructions. A comprehensive set of such instructions can
# be found in s2e.h. You can adapt them to SystemTap, in case
# you need them.

# Terminate current state.
# This is a SystemTap function that can be called from SystemTap code.
function s2e_kill_state(status:long, message: string) %{
 __asm__ __volatile__(
   ".byte 0x0f, 0x3f\n"
   ".byte 0x00, 0x06, 0x00, 0x00\n"
   ".byte 0x00, 0x00, 0x00, 0x00\n"
   : : "a" ((uint32_t)THIS->status), "b" (THIS->message)
 );
%}

# Print message to the S2E log.
# This is a SystemTap function that can be called from SystemTap code.
function s2e_message(message:string) %{
 __asm__ __volatile__(
   ".byte 0x0f, 0x3f\n"
   ".byte 0x00, 0x10, 0x00, 0x00\n"
   ".byte 0x00, 0x00, 0x00, 0x00\n"
   : : "a" (THIS->message)
 );
%}

# SystemTap also allows to paste arbitrary C code.
# This is useful when calling other C functions.

%{
// Make the specified buffer symbolic and assign a name to it.
static inline void s2e_make_symbolic(void *buf, int size, const char *name)
{
 __asm__ __volatile__(
   ".byte 0x0f, 0x3f\n"
   ".byte 0x00, 0x03, 0x00, 0x00\n"
   ".byte 0x00, 0x00, 0x00, 0x00\n"
   : : "a" (buf), "b" (size), "c" (name)
 );
}
%}

#### Now comes the real stuff ####

# Take a pointer to the IP header, and make the options length field symbolic.
function s2e_inject_symbolic_ip_optionlength(ipheader: long) %{
 uint8_t *data = (uint8_t*)((uintptr_t)(THIS->ipheader + 0));

 uint8_t len;
 s2e_make_symbolic(&len, 1, "ip_headerlength");
 *data = *data & 0xF0;
 *data = *data | ((len) & 0xF);
%}

# Instruct SystemTap to intercept the netif_receive_skb kernel function.
# NIC drivers call this function when they are ready to give the received packet
# to the kernel.
probe kernel.function("netif_receive_skb") {
 msg = sprintf("%s: len=%d datalen=%d\n", probefunc(), $skb->len, $skb->data_len)
 s2e_message(msg)
 s2e_inject_symbolic_ip_optionlength($skb->data)
}


# Instruct SystemTap to intercept the pcnet32_start_xmit in the pcnet32 driver.
# We also tell S2E to kill the current state.
# Intercepting this function can be useful to analyze the reaction of the kernel
# to the reception of a (symbolic) packet.
probe module("pcnet32").function("pcnet32_start_xmit") {
 msg = sprintf("%s: len=%d datalen=%d\n", probefunc(), $skb->len, $skb->data_len)
 s2e_message(msg)
 s2e_kill_state(0, "pcnet32_start_xmit")
}

Compile the script with SystemTap in the chroot environment, adjusting the kernel version to suit your needs.

docker # stap -a i386 -r 4.9.3-s2e  -g -m pcnet_probe pcnet32.stp

This will result in a module called pcnet_probe.ko that we will upload to the VM as explained earlier in this tutorial.

Running the script in S2E

staprun pcnet_probe.ko &

This will load the probe into the kernel. Symbolic execution will start when the network card receives the first packet. To send a packet, use netcat (in the guest) to send a UDP packet: