Efficient memory safety for TinyOS

ABSTRACT

Reliable sensor network software is difficult to create: applications are concurrent and distributed, hardware-based memory protection is unavailable, and severe resource constraints necessitate the use of unsafe, low-level languages. Our work improves this situation by providing efficient memory and type safety for TinyOS 2 applications running on the Mica2, MicaZ, and TelosB platforms. Safe execution ensures that array and pointer errors are caught before they can corrupt RAM. Our contributions include showing that aggressive optimizations can make safe execution practical in terms of resource usage; developing a technique for efficiently enforcing safety under interrupt-driven concurrency; extending the nesC language and compiler to support safety annotations; finding previously unknown bugs in TinyOS; and, finally, showing that safety can be exploited to increase the availability of sensor networks applications even when memory errors are left unfixed.

REFERENCES

• 1: Godmar Back , Wilson Hsieh, Drawing the Red Line in Java, Proceedings of the The Seventh Workshop on Hot Topics in Operating Systems, p.116, March 28-30, 1999
• 2: Gérard Berry, The foundations of Esterel, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 3: Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula. Dependent types for low-level programming. In Proc. 16th European Symp. on Programming (ESOP), Braga, Portugal, March--April 2007.
• 4: Nathan Cooprider , John Regehr, Pluggable abstract domains for analyzing embedded software, Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems, June 14-16, 2006, Ottawa, Ontario, Canada
• 5: David Culler , Deborah Estrin , Mani Srivastava, Guest Editors' Introduction: Overview of Sensor Networks, Computer, v.37 n.8, p.41-49, August 2004 [doi>10.1109/MC.2004.93]
• 6: The Deputy Project, 2007. http://deputy.cs.berkeley.edu.
• 7: Dinakar Dhurjati , Vikram Adve, Backwards-compatible array bounds checking for C with very low overhead, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134309]
• 8: Dinakar Dhurjati , Sumant Kowshik , Vikram Adve , Chris Lattner, Memory safety without garbage collection for embedded applications, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.1, p.73-111, February 2005 [doi>10.1145/1053271.1053275]
• 9: 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
• 10: Lin Gu , John A. Stankovic, t-kernel: providing reliable OS support to wireless sensor networks, Proceedings of the 4th international conference on Embedded networked sensor systems, October 31-November 03, 2006, Boulder, Colorado, USA [doi>10.1145/1182807.1182809]
• 11: Brian Hackett , Manuvir Das , Daniel Wang , Zhe Yang, Modular checking for buffer overflows in the large, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134319]
• 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: J. D. Ichbiah, Preliminary Ada reference manual, ACM SIGPLAN Notices, v.14 n.6a, p.1-145, June 1979 [doi>10.1145/956650.956651]
• 14: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 15: Sumant Kowshik , Dinakar Dhurjati , Vikram Adve, Ensuring code safety without runtime checks for real-time control systems, Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems, October 08-11, 2002, Grenoble, France [doi>10.1145/581630.581678]
• 16: Nancy G. Leveson, Safeware: system safety and computers, ACM, New York, NY, 1995
• 17: Philip Levis. TinyOS Extension Proposal (TEP) 111: message_t, 2006. http://www.tinyos.net/tinyos-2.x/doc/html/tep111.html.
• 18: Philip Levis, David Gay, Vlado Handziski, Jan-Hinrich Hauer, Ben Greenstein, Martin Turon, Jonathan Hui, Kevin Klues, Cory Sharp, Robert Szewczyk, Joe Polastre, Philip Buonadonna, Lama Nachman, Gilman Tolle, David Culler, and Adam Wolisz. T2: A second generation OS for embedded sensor networks. Technical Report TKN-05-007, Telecommunication Networks Group, Technische Universität Berlin, November 2005.
• 19: Michael R. Lyu. Handbook of Software Reliability Engineering. McGraw-Hill, 1995.
• 20: George C. Necula , Jeremy Condit , Matthew Harren , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy software, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.3, p.477-526, May 2005 [doi>10.1145/1065887.1065892]
• 21: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 22: John Regehr , Nathan Cooprider , Will Archer , Eric Eide, Efficient type and memory safety for tiny embedded systems, Proceedings of the 3rd workshop on Programming languages and operating systems: linguistic support for modern operating systems, p.6-es, October 22-22, 2006, San Jose, California [doi>10.1145/1215995.1216001]
• 23: Ram Kumar Rengaswamy, Eddie Kohler, and Mani Srivastava. Software-based memory protection in sensor nodes. In Proc. of the 3rd Workshop on Embedded Networked Sensors (EmNets), Cambridge, MA, May 2006.
• 24: Matthew Simpson , Bhuvan Middha , Rajeev Barua, Segment protection for embedded systems using run-time checks, Proceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems, September 24-27, 2005, San Francisco, California, USA [doi>10.1145/1086297.1086307]
• 25: Sun Microsystems. Sun SPOT system: Turning vision into reality. http://research.sun.com/spotlight/SunSPOTSJune30.pdf, 2005.
• 26: Sun Microsystems. Java Card Specification 2.2.2, March 2006.
• 27: Ben L. Titzer, Virgil: objects on the head of a pin, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 28: Ben L. Titzer , Daniel K. Lee , Jens Palsberg, Avrora: scalable sensor network simulation with precise timing, Proceedings of the 4th international symposium on Information processing in sensor networks, April 24-27, 2005, Los Angeles, California
• 29: Feng Zhou , Jeremy Condit , Zachary Anderson , Ilya Bagrak , Rob Ennals , Matthew Harren , George Necula , Eric Brewer, SafeDrive: safe and recoverable extensions using language-based techniques, Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation, p.4-4, November 06-08, 2006, Seattle, WA

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

Additional Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Performance attributes

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.3 Coding Tools and Techniques
      D.2.5 Testing and Debugging
          Subjects: Error handling and recovery
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability

General Terms:
Languages, Performance, Reliability

Keywords:
TinyOS, cXprop, deputy, memory safety, nesC, safe TinyOS, type safety, wireless sensor networks