SLEDE: lightweight verification of sensor network security protocol implementations

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 ease the task of verifying sensor network security protocol implementations for the sensor network community by definin...

• Type: Conference
• Year: 2007
• Where: SIGSOFT
• Authors: Youssef Hanna
• Keywords: NesC Security Protocol, Security Protocol Implementations, Sensor Network Security, SIGSOFT 2007, Software Engineering