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. Technical Report #07-09. Iowa State University, Dept. of Computer Science.

BibTeX Reference

@techreport{hanna2008slede-a,
  author = {Hanna, Youssef and Rajan, Hridesh and Zhang, Wensheng},
  title = {Slede: A Domain-specific Verification Framework for Sensor Network Security Protocol Implementations},
  year = {2008},
  institution = {Iowa State University, Dept. of Computer Science},
  number = {07-09},
  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.
  }
}