Finding Software Bugs Using Symbolic Execution

The idea of dynamic symbolic execution is to execute a piece of software on any input. All possible execution paths are explored simultaneously without specifying concrete values. Consider the following example where the input x is unknown, i.e., symbolic:

if (x < 0) {
    // ...
} else if (x > 100) {
    // ...
} else {
    assert("should not reach this!")
}

Symbolic execution runs this code on all three execution paths (x<0, x>100, 0<=x<=100) and generates three concrete test cases: x=-1, x=101 and x=23 after hitting the assertion.

You don’t need to write test cases manually anymore. You catch assertion failures and memory safety errors along the execution paths. Ok, that is all in theory, but can this approach work for real-world programs in practice?

KLEE

KLEE is a symbolic execution engine that executes unmodified, real-world programs on any input. You compile your program to LLVM bitcode, mark some inputs as symbolic, and start KLEE. KLEE explores possible execution paths using constraint solving and generates concrete test cases for each of them. In case of a bug, you can replay your program with the input that triggered it.

In November 2019, the seminal OSDI 2008 paper on KLEE has been elected to ACM SIGOPS Hall of Fame. Over the past decade, the research and application of KLEE resulted in over 150 scientific publications, dozens of Ph.D. theses, research grants, tools, and security startups. On my behalf, I spent more than five years of my life with KLEE as well and learned a lot along the way.

Testing Network Protocols Using KLEE

In 2007, I struggled to find my research thesis until I came across Cristian Cadar’s paper “EXE: Automatically Generating Inputs of Death”. Inspired by the idea of symbolic execution, I asked myself the following question: Can I mark the protocol header of an incoming network packet symbolic before passing it to the network stack? If so, can I find protocol specification and implementation bugs with this technique?

I wrote an e-mail to Cristian Cadar and promptly received an answer. Moreover, Cristian and Daniel Dunbar generously sent me the source code of KLEE, a new tool they were working on, even before its official release to the public.

In the following five years of my Ph.D. journey, I extended KLEE to execute several protocol stacks that talk to each other. I applied this technique to test sensor networks and found a couple of interesting bugs in the Contiki OS described in my IPSN 2010 paper. One of them caused a dead-lock of a sensor node inside the TCP/IP stack requiring a hardware reset. It was a real bug observed in sensor network deployments.

I have not used KLEE actively since 2015 and was curious to give it a try (again). Meanwhile, Contiki OS has been forked to Contiki-NG. I cloned the repo and compiled the test case called 20-packet-parsing to LLVM bitcode. Inside the test case, I marked the test packet buffer (~1KB) symbolic using KLEE’s klee_make_symbolic function.

After running for a couple of minutes on my old Mac, KLEE discovered two memory errors (out of bound pointers) while parsing certain protocols’ headers. I reported these findings with the concrete test cases to the security team of Contiki-NG for further analysis. To me, this small test is yet another evidence that KLEE remains to be a useful research and test case generation tool.

Open Challenges and Opportunities

Applying symbolic execution to arbitrary real-world programs is hard. You often have to model the execution environment and find effective ways to cope with non-determinism and path explosion. Moreover, many of the path constraints are difficult yet intractable to be solved in time with today’s solvers.

Nevertheless, studying and applying symbolic execution (using KLEE) opens many opportunities. You will learn about program structure, compilers, SAT/SMT solvers, and how to write other kinds of testing tools. Given this bag of knowledge, I wrote tools to fuzz Android apps, superoptimize LLVM IR, and more recently at work, a tool to fuzz satellite control procedures written in SPELL.

Consider giving symbolic execution a try. If you are a Ph.D. student and struggling to find a thesis topic in this area, don’t forget the bigger picture and keep pushing.

Subscribe via RSS or follow @rsasnauskas on Twitter for more.