SLEDE: lightweight verification of sensor network security protocol implementations

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 ease the task of verifying sensor network security protocol implementations for the sensor network community by defining 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 security protocol implementations. By significantly decreasing the cost of verification, we believe our approach will improve the overall quality of the nesC security protocol implementations.

REFERENCES

• 1: Karthikeyan Bhargavan , Cedric Fournet , Andrew D. Gordon , Stephen Tse, Verified Interoperable Implementations of Security Protocols, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.139-152, July 05-07, 2006 [doi>10.1109/CSFW.2006.32]
• 2: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 3: Edmund Clarke, Muralidhar Talupur, Tayssir Touili, and Helmut Veith. Verification by network decomposition. In Fifteenth International Conference on Concurrency Theory (CONCUR 04), pages 276--291. Springer-Verlag, 2004.
• 4: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: Laurent Eschenauer , Virgil D. Gligor, A key-management scheme for distributed sensor networks, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586117]
• 7: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 8: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 9: Jean Goubault-Larrecq and Fabrice Parrennes. Cryptographic protocol analysis on real C code. In Radhia Cousot, editor, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 363--379, Paris, France, January 2005. Springer.
• 10: Youssef Hanna and Hridesh Rajan. Slede: A domain specific verification framework for sensor network security protocol implementations. Technical Report 07--09, Computer Science, Iowa State University, 2007.
• 11: Klaus Havelund, Java PathFinder, A Translator from Java to Promela, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.152, September 21-24, 1999
• 12: Jason Hill , Robert Szewczyk , Alec Woo , Seth Hollar , David Culler , Kristofer Pister, System architecture directions for networked sensors, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.93-104, November 2000, Cambridge, Massachusetts, United States
• 13: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 14: Gerard J. Holzmann , Margaret H. Smith, A practical method for verifying event-driven software, Proceedings of the 21st international conference on Software engineering, p.597-607, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302710]
• 15: Chin-Liang Chang , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
• 16: Catherine Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):113--131, 1996.
• 17: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 18: nesC Compiler. http://sourceforge.net/projects/nescc.
• 19: Adrian Perrig , Robert Szewczyk , Victor Wen , David Culler , J. D. Tygar, SPINS: security protocols for sensor networks, Proceedings of the 7th annual international conference on Mobile computing and networking, p.189-199, July 2001, Rome, Italy [doi>10.1145/381677.381696]
• 20: Amir Pnueli. The temporal logic of programs. In The 18th Annual Symposium on the Foundations of Computer Science, pages 46--57, New York, 1977. IEEE.
• 21: Bastian Schlich and Stefan Kowalewski. Model checking c source code for embedded systems. In IEEE/NASA Workshop Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2005), sep 2005.
• 22: Gustavus J. Simmons. How to (selectively) broadcast a secret. In Proceedings of the IEEE Symposium on Security and Privacy, page 108, 1985.
• 23: Hao Yang , Fan Ye , Yuan Yuan , Songwu Lu , William Arbaugh, Toward resilient security in wireless sensor networks, Proceedings of the 6th ACM international symposium on Mobile ad hoc networking and computing, May 25-27, 2005, Urbana-Champaign, IL, USA [doi>10.1145/1062689.1062696]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Security, Verification

Keywords:
Slede, model checking, security protocols, sensor networks