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 S2E 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.

Software



Publications

Integration Testing of Protocol Implementations using Symbolic Distributed Execution. The 2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), Oct 30 - Nov 2, 2012, Austin, TX, USA. October 2012.
Scalable Symbolic Execution of Distributed Systems. Proceedings of the 31st IEEE International Conference on Distributed Computing Systems (ICDCS 2011), Jun 20 - Jun 24, 2011, Minneapolis, MN, USA. June 2011.
Demo Abstract: Integrating Symbolic Execution with Sensornet Simulation for Efficient Bug Finding. Proceedings of the 8th ACM Conference on Embedded Networked Sensor Systems (SenSys 2010), Zurich, Switzerland. November 2010.
KleeNet: Discovering Insidious Interaction Bugs in Wireless Sensor Networks Before Deployment. Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN 2010), Stockholm, Sweden. April 2010.
Poster Abstract: KleeNet - Automatic Bug Hunting in Sensor Network Applications. Proceedings of the 6th ACM conference on Embedded network sensor systems (SenSys'08), Raleigh, NC, United States. November 2008.
Bug Hunting in Sensor Network Applications. Proceedings of the 7th GI/ITG Fachgespraech Wireless Sensor Networks, Berlin, Germany. September 2008.