Symbolic Execution of Distributed Systems

High-coverage testing of distributed systems, such as sensornets, is vital for pre-deployment bug cleansing, but has notoriously been difficult due to the limited set of available tools. The main challenge is to detect bugs that occur due to low-probability events, such as node/network failures and unforeseen input. These events, due to their non-deterministic nature, have the potential to drive the distributed execution into corner-case situations hard to detect using existing testing and debugging techniques.

In this talk, I will first introduce the concept of symbolic distributed execution (SDE) that targets the discovery of such bugs before deployment. Second, I will present KleeNet – a testing environment for networked systems that executes applications on symbolic input and automatically injects non-deterministic failures. We integrated KleeNet with the COOJA network simulator for Contiki OS and detected a number bugs in the widely-deployed μIP TCP/IP protocol stack. Next to KleeNet, I will shortly present our initial prototype of SDE implementation for the analyses of communicating virtual machines running unmodified, even closed-source binaries.

Raimondas Sasnauskas is a sixth-year PhD student at the RWTH Aachen University, working at the chair of Communication and Distributed Systems (ComSys) lead by Prof. Klaus Wehrle. His research interests lie in the area of systems dependability, with particular focus on high-coverage protocol testing before deployment using symbolic execution techniques.