SystemTap and S2E - Cannot fork

[johnathonro...@gmail.com]

I'm using S2E in conjunction with SystemTap to test kernel drivers, similar to the DDT paper but with USB device drivers in the Linux kernel. I have a very simple emulated USB device and Linux driver than upon initialisation calls a function `my_vulnerable_function` as seen below:

my_vulnerable_function(u32 x, char *msg)
{
        printk( KERN_INFO "x is at 0x%p\n", &x);
        if( x == 13 ){
                kfree( msg );
        }
        printk( KERN_INFO "WHY_WOULD_YOU_DO_THIS : %s\n",
                msg);
        return 0;
}

In the system tap script, I have included the entire s2e{,-x86}.h to access s2e functions; and they seem to work s2e_{log,message,make_symbolic} ect. Here is the specific system tap functions that are being intercepted. I have copied the example from the SystemTap docs in that I declare a new variable and make it symbolic, then set it to the value in the kernel module.

function my_vuln_func(data:long) %{
        uint32_t *x = (uint32_t *)STAP_ARG_data;
        uint32_t y;
        s2e_make_symbolic(&y, 4, "y");
        *x = y;
%}

probe module("usb_skeleton").function("my_vulnerable_function") {

           s2e_enable_forking()

        println( "my_vuln_func :: ".$$vars )
        msg = sprintf("%s :: x = %i, %p", probefunc(),  $x, &$x)
        log(msg)
        #_s2e_make_symbolic(&$x, 4, "x")
        my_vuln_func(&$x)
}

Here is my config.lua:

s2e = {
  kleeArgs = {
        "--use-batching-search",
        "--use-random-path"
  }
}

plugins = {
  --This is required for s2e_make_symbolic
  "BaseInstructions",
  "ExecutionTracer",
  "ModuleTracer",
  "RawMonitor",
  "MemoryTracer",
  "TestCaseGenerator",
  "ConsistencyModels"
}
pluginsConfig = {}
pluginsConfig.ConsistencyModels = {
    model="strict"
}

When I execute the stap script and then load the kernel module, my module loads, prints to the kernel log, s2e_message and s2e_make_symbolic is called and printed to the debug output but the state isn't forked. I have printed out the addresses of `x` in the kernel log, stap output and s2e debug; all of which match. Why isn't the state forked?


Here's a snapshot of the debug.txt:

Creating plugin CorePlugin
Creating plugin BaseInstructions
Creating plugin ExecutionTracer
Creating plugin ModuleTracer
Creating plugin RawMonitor
Creating plugin MemoryTracer
Creating plugin TestCaseGenerator
Creating plugin ConsistencyModels
You should specify pluginsConfig['RawMonitor'].kernelStart
MonitorMemory: 0 PageFaults: 0 TlbMisses: 0
0 [State 0] Created initial state
128 [State 0] BaseInstructions: custom instruction (opcode: 0x1000) called.
128 [State 0] Message from guest (0xffffffffa0623256): Enabling forking...
128 [State 0] BaseInstructions: custom instruction (opcode: 0x900) called.
549 [State 0] BaseInstructions: custom instruction (opcode: 0x900) called.
550 [State 0] BaseInstructions: custom instruction (opcode: 0x300) called.
550 [State 0] Inserting symbolic data at 0xffff880021ce7a64 of size 0x4 with name 'y'