Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols

Date
2006-11-14
Authors
Hanna, Youssef
Rajan, Hridesh
Rajan, Hridesh
Wensheng, Zhang
Journal Title
Journal ISSN
Volume Title
Publisher
Source URI
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

The contribution of this work is an approach for lightweight specification and verification of nesC implementations of sensor networks security protocols. Our approach provides annotations to specify objectives, network topology, intruder models, and channel fault models. The objectives of the protocols can be specified in terms of user-defined events, which is significantly more expressive compared to earlier approaches such as CAPSL that provide a fixed set of objectives. Moreover, our approach is extensible in that it allows new intruder and channel fault models to be added to the verification process. These models are themselves written in nesC. To show the feasibility of our approach, we describe the implementation of our verification framework. Our verification framework uses the model checker SPIN as the underlying technology. Our approach was able to detect earlier known bugs in protocols and an assumption violation in the protocol implementation.

Description
Keywords
Citation
Collections