Slede: Lightweight Specification and Formal Verification of Sensor Networks Protocols

Motivation

Flaws in security protocols are subtle and hard to find. Finding flaws in the security protocols for sensor networks is even harder because they operate under fundamentally different system design assumptions such as event-driven vs. imperative or message passing, resource and bandwidth constraints, hostile deployment scenarios, trivial physical capturing due to the lack of tamper resistance, group-oriented behavior, ad hoc and dynamic topologies, open-ended nature, etc. These assumptions lead to complex security protocols, which in turn makes them much harder to verify. Sensor networks are increasingly becoming an integral part of the nation's cyber infrastructure, making it vital to protect them against cryptographic errors in security protocols. There are several existing techniques for specifying and verifying cryptographic protocols; however, none accommodates all the system design assumptions mentioned above.

The Slede project is advancing the state of the art in specification and verification of cryptographic protocols for sensor networks. Applications of sensor networks are numerous from military to environmental research. By providing mechanisms to find cryptographic errors in the security protocols for sensor networks this research program is improving the reliability of these networks, making a direct impact on all areas where these networks are utilized. The activities in this research project are collectively contributing to the development of innovative specification and verification mechanisms for security protocols in sensor networks, and training of a diverse cadre of young scientists in programming languages, software engineering, computer networks, and most importantly enhanced computer security.