About Slede

Slede 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).

Motivation

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. Slede is a framework for automating formal verification of sensor network security protocols. It extracts models from protocol implementations and verifies them against generated intruder models.

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