Finding Bugs in Wireless Sensor Networks with Symbolic Execution

Abstract

Sensor networks are composed of many sensor nodes which have limitations such as memory and CPU. It is difficult to access them physically, since they are usually distributed in a hard-toreach environment such as high mountains and far deserts. They are also connected to each other by unreliable wireless links. These factors make debugging of sensor network, a challenging activity. As a matter of fact, it may be common for a deployed sensor network to encounter periodic faults. Locating and fixing these bugs are difficult after deployment. A main challenge is to find bugs that are related to non-deterministic events, such as node failure and packet loss. Since these non-deterministic events often cause complex bugs and errors in sensor applications. Most of available debugging approaches and tools have been unsuccessful in detecting such bugs. In sensor network applications, a high coverage testing before deployment is vital to clean bugs. However, there are limited numbers of such tools available; hence comprehensive testing has been difficult so far. In this thesis work, we integrate KLEE symbolic execution tool with TinyOS to provide high coverage and effective testing before deployment. KLEE executes sensor network applications on a wide variety of symbolic inputs. In addition, by using such symbolic execution tool, we can automatically inject non-deterministic failures to applications. Consequently, KLEE highly covers application and provides numerous distributed execution paths. These paths may include low-probability situations. As a case study, we integrate KLEE into Distance Information Protocol (DIP) and TinyOS MANET On demand (TYMO) protocols available in TinyOS package. We show that KLEE effectively detects two out-of-bound bugs in DIP protocol and three serious bugs in TYMO. Bugs in TYMO are critical and result in packet transmission failure.