Laboratory for Software Design

Got a question?

Got a question or comment? Contact us at (515) 294-6168 or hridesh@cs.iastate.edu.

SLEDE: Lightweight Verification of Sensor Network Security Protocol Implementations

By Youssef Hanna

Abstract

Finding flaws in security protocol implementations is hard. Finding flaws in the implementations of sensor network security protocols is even harder because they are designed to protect against more system failures compared to traditional protocols. Formal verification techniques such as model checking, theorem proving, etc, have been very successful in the past in detecting faults in security protocol specifications; however, they generally require a model. Developing these models is a non-trivial task for an average developer. This task is further complicated by the impedance mismatch between the implementation language and the modeling language. For example, while the dominant implementation language for sensor network applications (nesC)} uses an event-based paradigm, the modeling language (Promela) uses message-driven paradigm. The key goal of this research is to define an approach for automatically extracting a model from the nesC implementations of a security protocol. We contribute the design and implementation of a verification framework that we call slede which emulates our approach to extract a PROMELA model from nesC implementation. By significantly decreasing the cost of verification, we believe our approach will improve the overall quality of the nesC security protocol implementations.

Bibliographic Information

@InProceedings{Hanna-07,
author = {Youssef Hanna},
title = {SLEDE: Lightweight Verification of Sensor Network Security Protocol Implementations},
booktitle = {ESEC/FSE '07: 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering},
year = {2007},
month = {September},
location = {Dubrovnik, Croatia},
}

Paper:[PDF].