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.

News

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

News Archive

About Slede

Flaws 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

  • Ultra-lightweight protocol specification
  • Completely automatic generation of verifiable model from NesC code of the sensor application
  • Automatic generation of protocol-specific intrusion model and its composition with the verification model of the protocol
  • Automated verification of the composed model
  • User-friendly output, in case of protocol faults, and last but not least,
  • Tight-integration with existing tool-set for NesC developers.


Recent Publications/Presentations

  • Youssef Hanna, Samik Basu, and Hridesh Rajan, "Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems", The 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 09), August 2009, Amsterdam, The Netherlands. [PDF Format]
  • Youssef Hanna and Hridesh Rajan, "Slede: Framework for Automatic Verification of Sensor Network Security Protocol Implementations", informal demo in the Proceedings of the 31st International Conference on Software Engineering (ICSE 2009), May 16-24 2009, Vancouver, Canada. [PDF Format] [Poster]
  • Youssef Hanna, Hridesh Rajan, and Wensheng Zhang, "Slede: A Domain-Specific Verification Framework for Sensor Network Security Protocol Implementations", in the Proceedings of the First ACM Conference on Wireless Network Security (WiSec 2008), March 31 - April 2, 2008. Alexandria, VA. [PDF Format]
  • Youssef Hanna, "SLEDE: lightweight verification of sensor network security protocol implementations", in the Proceedings of the doctoral symposium of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007), Dubrovnik, Croatia, September 2007, pp. 591-594. [PDF Fromat]
  • See more ...