Mutatis Mutandis: Safe and predictable dynamic software updating

ABSTRACT

This article presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program's type structure to change dynamically but guarantees the updated program remains type-correct by ensuring a property we call con-freeness. We show how con-freeness can be enforced dynamically, and how it can be approximated via a novel static analysis. This analysis can be used to assess the implications of a program's structure on future updates in order to make update success more predictable. We have implemented Proteus for C, and briefly discuss our implementation which we have tested on several well-known programs.

REFERENCES

• 1: Sameer Ajmani , Barbara H. Liskov, Automatic software upgrades for distributed systems, Massachusetts Institute of Technology, Cambridge, MA, 2004
• 2: Ajmani, S., Liskov, B., and Shrira, L. 2006. Modular software upgrades for distributed systems. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP).
• 3: Gautam Altekar , Ilya Bagrak , Paul Burstein , Andrew Schultz, OPUS: online patches and updates for security, Proceedings of the 14th conference on USENIX Security Symposium, p.19-19, July 31-August 05, 2005, Baltimore, MD
• 4: Appel, A. 1994. Hot-Sliding in ML. Unpublished manuscript.
• 5: Armstrong, J. L. and Virding, R. 1991. Erlang---An experimental telephony switching language. In the 13th International Switching Symposium. Stockholm, Sweden.
• 6: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 7: Andrew Baumann , Gernot Heiser , Jonathan Appavoo , Dilma Da Silva , Orran Krieger , Robert W. Wisniewski , Jeremy Kerr, Providing dynamic update in an operating system, Proceedings of the annual conference on USENIX Annual Technical Conference, p.32-32, April 10-15, 2005, Anaheim, CA
• 8: Bierman, G., Hicks, M., Sewell, P., and Stoyle, G. 2003a. Formalizing dynamic software updating. In Proceedings of (USE03) the 2nd International Workshop on Unanticipated Software Evolution Warsaw, Poland.
• 9: Gavin Bierman , Michael Hicks , Peter Sewell , Gareth Stoyle , Keith Wansbrough, Dynamic rebinding for marshalling and update, with destruct-time ?, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.99-110, August 25-29, 2003, Uppsala, Sweden
• 10: Bloom, T. 1983. Dynamic module replacement in a distributed programming system. Ph.D. thesis, Laboratory for Computer Science, The Massachussets Institute of Technology.
• 11: Bloom, T. and Day, M. 1993. Reconfiguration and module replacement in Argus: Theory and practice. Soft. Engin. J. 8, 2 (March), 102--108.
• 12: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira , Chuang-Hue Moh , Steven Richman, Lazy modular upgrades in persistent object stores, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 13: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• 14: Bryan Buck , Jeffrey K. Hollingsworth, An API for Runtime Code Patching, International Journal of High Performance Computing Applications, v.14 n.4, p.317-329, November 2000 [doi>10.1177/109434200001400404]
• 15: Drossopoulou, S. and Eisenbach, S. 2003. Flexible, source level dynamic linking and re-linking. In Proceedings of the ECOOP 2003 Workshop on Formal Techniques for Java Programs.
• 16: Dominic Duggan, Type-based hot swapping of running modules (extended abstract), Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 17: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: Ophir Frieder , Mark E. Segal, On dynamically updating a computer program: from concept to prototype, Journal of Systems and Software, v.14 n.2, p.111-128, Feb. 1991 [doi>10.1016/0164-1212(91)90096-O]
• 19: Vladimir Gapeyev , Michael Y. Levin , Benjamin C. Pierce, Recursive subtyping revealed: (functional pearl), Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.221-231, September 2000
• 20: Gilmore, S., Kirli, D., and Walton, C. 1997. Dynamic ML without dynamic types. Tech. rep. ECS-LFCS-97-378, LFCS, University of Edinburgh.
• 21: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 22: Gupta, D. 1994. Online software version change. Ph.D. thesis, Department of Computer Science and Engineering, Indian Institute of Technology, Kanpur, India.
• 23: Nevin Charles Heintze, Set based program analysis, Carnegie Mellon University, Pittsburgh, PA, 1992
• 24: Michael Hicks , Scott Nettles, Dynamic software updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1049-1096, November 2005 [doi>10.1145/1108970.1108971]
• 25: Hicks, M., Tse, S., Hicks, B., and Zdancewic, S. 2005. Dynamic updating of information-flow policies. In Proceedings of the International Workshop on Foundations of Computer Security (FCS).
• 26: Michael W. Hicks , Stephanie Weirich , Karl Crary, Safe and Flexible Dynamic Linking of Native Code, Selected papers from the Third International Workshop on Types in Compilation, p.147-176, September 21, 2000
• 27: Michael William Hicks , Scott M. Nettles, Dynamic software updating, University of Pennsylvania, Philadelphia, PA, 2001
• 28: Gísli Hjálmtýsson , Robert Gray, Dynamic C++ classes: a lightweight mechanism to update code in a running program, Proceedings of the annual conference on USENIX Annual Technical Conference, p.6-6, June 15-19, 1998, New Orleans, Louisiana
• 29: John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• 30: Iulian Neamtiu , Jeffrey S. Foster , Michael Hicks, Understanding source code evolution using abstract syntax tree matching, Proceedings of the 2005 international workshop on Mining software repositories, p.1-5, May 17-17, 2005, St. Louis, Missouri
• 31: Iulian Neamtiu , Michael Hicks , Gareth Stoyle , Manuel Oriol, Practical dynamic software updating for C, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 32: 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
• 33: David Oppenheimer , Aaron Brown , James Beck , Daniel Hettena , Jon Kuroda , Noah Treuhaft , David A. Patterson , Katherine Yelick, ROC-1: Hardware Support for Recovery-Oriented Computing, IEEE Transactions on Computers, v.51 n.2, p.100-107, February 2002 [doi>10.1109/12.980002]
• 34: A Technique for Dynamic Updating of Java Software, Proceedings of the International Conference on Software Maintenance (ICSM'02), p.649, October 03-06, 2002
• 35: Peterson, J., Hudak, P., and Ling, G. S. 1997. Principled dynamic code improvement. Tech. rep. YALEU/DCS/RR-1135, Department of Computer Science, Yale University.
• 36: Soules, C., Appavoo, J., Hui, K., Wisniewski, R. W., Silva, D. D., Ganger, G. R., Krieger, O., Stumm, M., Auslander, M., Ostrowski, M., Rosenburg, B., and Xenidis, J. 2003. System support for online reconfiguration. In Proceedings of the USENIX Annual Technical Conference.
• 37: Gareth Stoyle , Michael Hicks , Gavin Bierman , Peter Sewell , Iulian Neamtiu, Mutatis mutandis: safe and predictable dynamic software updating, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.183-194, January 12-14, 2005, Long Beach, California, USA
• 38: David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]
• 39: David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]
• 40: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA
• 41: Zorn, B. 2005. Personal communication, based on experience with Microsoft Windows customers.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics; Syntax

General Terms:
Design, Languages, Reliability, Theory, Verification

Keywords:
Dynamic software updating, Proteus, capability, type inference, updateability analysis