archives

SLEDE: A Domain-Specific Verification Framework for Sensor Network Security Protocol Implementations


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Hanna, Youssef and Rajan, Hridesh (2007) SLEDE: A Domain-Specific Verification Framework for Sensor Network Security Protocol Implementations. Technical Report 07-09, Computer Science, Iowa State University.

Full text available as:Adobe PDF

Abstract

Sensor networks are often deployed in hostile situations. A number of protocols are being developed to secure these networks. Current means to verify these protocols include simulation, manual inspection, and running them on sensor network testbeds. These techniques leave room for subtle errors in protocol implementations that can be exploited by adversaries. The contribution of this work is the design, implementation and early evaluation of a domain-specific verification framework for nesC implementations of sensor network security protocols. We call our verification framework Slede. Technical underpinnings of Slede include support for automatic extraction of PROMELA models from nesC source code, an annotation language to guide the verification process, and an automatic intrusion model generator. Preliminary evaluation shows that Slede was able to discover flaws in a canonical cryptographic protocol by Needham and Schroeder and two security protocols specific to sensor networks. We also demonstrate that a protocol aware intrusion model automatically generated by Slede incurs a small extra cost compared to models handwritten by model checking experts. By automating a significant portion of the verification process, Slede promises to make it easier to apply finite-state model checking to verify nesC protocol implementations.

Keywords:sensor networks, security protocols, model checking, slede, intrusion model generation, SLEDE
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
ID code:00000543
Deposited by:Hridesh Rajan on 13 June 2007



Contact site administrator at: ssg@cs.iastate.edu