Slede: Lightweight Specification and Formal Verification of Sensor Networks Protocols
These pages describe work carried out under the NSF grant CNS-0627354 on Specification and Verification Challenges for Security Protocols in Sensor Networks. The PI is Hridesh Rajan and much of the work is carried out by Youssef Hanna.
NewsMar 2009: Youssef's submission to ESEC/FSE 2009 accepted. Jan 2009: Youssef's submission to the ICSE 2009 Research Demonstrations track accepted as informal demo. Nov 2008: Eclipse plugin for Slede is available for download. July 2008: Slede is available for download. Dec 2007: Youssef's submission to the ACM Conference on Wireless Network Security (WiSec 08) accepted. Sep 2007: Youssef's submission to the ESEC/FSE 2007 doctoral symposium accepted. |
About SledeFlaws in security protocols are subtle and hard to find. Finding flaws in the security protocols for sensor networks is even harder because they operate under fundamentally different system design assumptions such as event-driven vs. imperative or message passing, resource and bandwidth constraints, hostile deployment scenarios, trivial physical capturing due to the lack of tamper resistance, group-oriented behavior, ad hoc and dynamic topologies, open-ended nature, etc. These assumptions lead to complex security protocols, which in turn makes them much harder to verify. Sensor networks are increasingly becoming an integral part of the nation's cyber infrastructure, making it vital to protect them against cryptographic errors in security protocols. Verifying sensor network security protocol implementations using testing/simulation might leave some flaws undetected. Formal verification techniques have been very successful in detecting faults in security protocol specifications; however, they generally require building a formal description (model) of the protocol. Building accurate models is hard, thus hindering the application of formal verification. Slede aims to solve this problem. It is a framework for automatic verification of sensor network security protocol implementations. Given an implementation of a security protocol in nesC, Slede extracts verifiable PROMELA models, generates protocol specific intruder models, composes them with the generated model and verifies the satisfaction of security properties against the composition of the models. In case of a propery violation, Slede translates the counterexample back to domain language (nesC). Key components of Slede are shown in the following figure: 
Key Features of Slede
Recent Publications/Presentations
|
Department of Computer Science, hridesh@cs.iastate.edu.
Copyright © 2010, Iowa State University of Science and Technology. All rights reserved.
This material is based upon work supported by the National Science Foundation under Grant No. 06-27354. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.