KleeNet - Symbolic Execution of Distributed Systems

High-coverage testing of distributed systems, such as sensornets, is vital for pre-deployment bug cleansing, but has previously 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 failures, packet losses, 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 our project, we designed and implemented KleeNet, a debugging environment based on KLEE that aims to effectively discover such situations before deployment. By running unmodified communication protocols on symbolic input and automatically injecting non-deterministic failures, KleeNet automatically generates distributed execution paths at high-coverage. Moreover, we integrated KleeNet with the COOJA sensor network simulator to allow for straight-forward and intuitive testing initiated from a simulation environment. A tight coupling of simulation and testing helps detect, narrow down, and fix complex interaction bugs in an early development phase.

In our recent research efforts we test protocols of communicating virtual machines which are symbolically executed using the S²E framework. Hence, we are able to generate test cases for unmodified distributed software running in diverse networked systems.

The main challenge in this project remains to be the scalability and the pruning of redundant execution states.