Finding Bugs in Wireless Sensor Networks with Symbolic Execution

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/176657
Download file(s):
File Description SizeFormat 
176657.pdfFulltext2.66 MBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Finding Bugs in Wireless Sensor Networks with Symbolic Execution
Authors: Sadat Mahdieh, Mirhashemi
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.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2013
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/176657
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.