Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols
File
Date
Authors
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Journal Issue
Is Version Of
Versions
Series
Department
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.