Slede: A Domain-specific Verification Framework for Sensor Network Security Protocol Implementations

By: Youssef Hanna, Hridesh Rajan, and Wensheng Zhang

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.

ACM Reference

Hanna, Y. et al. 2008. Slede: A Domain-specific Verification Framework for Sensor Network Security Protocol Implementations. Proceedings of the First ACM Conference on Wireless Network Security, WISEC, Alexandria, USA (2008), 109–118.

BibTeX Reference

@inproceedings{HannaRajanZhang2008a,
  author = {Youssef Hanna and Hridesh Rajan and Wensheng Zhang},
  title = {Slede: A Domain-specific Verification Framework for Sensor Network Security Protocol Implementations},
  booktitle = {Proceedings of the First ACM Conference on Wireless Network Security, WISEC, Alexandria, USA},
  pages = {109--118},
  year = {2008},
  publisher = {{ACM}},
  editor = {Virgil D. Gligor and Jean{-}Pierre Hubaux and Radha Poovendran},
  doi = {10.1145/1352533.1352551},
  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.},
}