Safety checking of machine code

ABSTRACT

We show how to determine statically whether it is safe for untrusted machine code to be loaded into a trusted host system. Our safety-checking technique operates directly on the untrusted machine-code program, requiring only that the initial inputs to the untrusted program be annotated with typestate information and linear constraints. This approach opens up the possibility of being able to certify code produced by any compiler from any source language, which gives the code producers more freedom in choosing the language in which they write their programs. It eliminates the dependence of safety on the correctness of the compiler because the final product of the compiler is checked. It leads to the decoupling of the safety policy from the language in which the untrusted code is written, and consequently, makes it possible for safety checking to be performed with respect to an extensible set of safety properties that are specified on the host side. We have implemented a prototype safety checker for SPARC machine-language programs, and applied the safety checker to several examples. The safety checker was able to either prove that an example met the necessary safety conditions, or identify the places where the safety conditions were violated. The checking times ranged from less than a second to 14 seconds on an UltraSPARC machine.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , S. Eggers, Extensibility safety and performance in the SPIN operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.267-283, December 03-06, 1995, Copper Mountain, Colorado, United States
• 3: B. Alpern, and F. B. Schneider. Recognizing Safety and Liveness. Distributed Computing 2 3. (1987).
• 4: Rastislav Bodík , Rajiv Gupta , Vivek Sarkar, ABCD: eliminating array bounds checks on demand, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.321-333, June 18-21, 2000, Vancouver, British Columbia, Canada
• 5: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 6: Tzi-cker Chiueh , Ganesh Venkitachalam , Prashant Pradhan, Integrating segmentation and paging protection for safe, efficient and transparent software extensions, Proceedings of the seventeenth ACM symposium on Operating systems principles, p.140-153, December 12-15, 1999, Charleston, South Carolina, United States
• 7: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 8: D.K. Detlefs, R. M. Leino, G. Nelson, and J. B. Saxe. Extended Static Checking. Research Report 159, Compaq Systems Research Center. Palo Alto, CA. (December 1998).
• 9: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 10: B. Elspas, M. W. Green, K. N. Levitt, and R. J. Waldinger. Research in Interactive Program-Proving Techniques. SRI, Menlo Park, California. (May 1972).
• 11: D. R. Engler , M. F. Kaashoek , J. O'Toole, Jr., Exokernel: an operating system architecture for application-level resource management, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.251-266, December 03-06, 1995, Copper Mountain, Colorado, United States
• 12: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 13: Illustra Information Technologies. Illustra DataBlade Developer's Kit Architecture Manual, Release 1.1. (1994).
• 14: JavaSoft. Java Native Interface Specification. Release 1.1 (May 1997).
• 15: jPVM: A Native Methods Interface to PVM for the Java Platform. http://www.chmsr.gatech.edu/jPVM. (2000).
• 16: S. Katz, and Z. Manna. A Heuristic Approach to Program Verification. 3rd International Conference on Artificial Intelligence. (August 1973).
• 17: W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnocott. The Omega Library, Version 1.1.0 Interface Guide. omega@ cs.umd.edu, http://www.cs.umd.edu/projects/omega. (November 1996).
• 18: Xavier Leroy , François Rouaix, Security properties of typed applets, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.391-403, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268979]
• 19: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 20: S. McCanne, and V. Jacobson. The BSD Packet Filter: A New Architecture for User-Level Packet Capture. The Winter 1993 USENIX Conference. USENIX Association. San Diego, CA. (January 1993).
• 21: Misrosoft. Microsoft COM Technologies-Information and Resources for the Component Object Model-Based Technologies. http://www.microsoft.com/com. (March 2000)
• 22: Barton P. Miller , Mark D. Callaghan , Jonathan M. Cargille , Jeffrey K. Hollingsworth , R. Bruce Irvin , Karen L. Karavanic , Krishna Kunchithapadam , Tia Newhall, The Paradyn Parallel Performance Measurement Tool, Computer, v.28 n.11, p.37-46, November 1995 [doi>10.1109/2.471178 ]
• 23: J. Mogul , R. Rashid , M. Accetta, The packer filter: an efficient mechanism for user-level network code, Proceedings of the eleventh ACM Symposium on Operating systems principles, p.39-51, November 08-11, 1987, Austin, Texas, United States
• 24: J. Morris. A General Axiom of Assignment. Theoretical Foundations of Programming Methodology, Lecture Notes of an International Summer School, directed by F. L. Bauer, E. W. Dijkstra and C.A.R. Hoare. Manfred Broy and Gunther Schmidt (Ed.). D. Reidel Publishing Company. (1982).
• 25: G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML Compiler: Performance and Safety Through Types. In 1996 Workshop on Compiler Support for Systems Software. Tucson, AZ. (February 1996).
• 26: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 27: J. Gregory Morrisett , Karl Crary , Neal Glew , David Walker, Stack-Based Typed Assembly Language, Proceedings of the Second International Workshop on Types in Compilation, p.28-52, March 25-27, 1998
• 28: G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, S. Zdancewic. TALx86: A Realistic Typed Assembly Language. ACM Workshop on Compiler Support for System Software. Atlanda, GA (May 1999).
• 29: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 30: George Ciprian Necula , Peter Lee, Compiling with proofs, 1998
• 31: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 32: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 33: Netscape. Browser Plug-ins, 1999. http://h~me'netscape'c~m/plugins/index'html'
• 34: C. Pu , T. Autrey , A. Black , C. Consel , C. Cowan , J. Inouye , L. Kethana , J. Walpole , K. Zhang, Optimistic incremental specialization: streamlining a commercial operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.314-321, December 03-06, 1995, Copper Mountain, Colorado, United States
• 35: William Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing, p.4-13, November 18-22, 1991, Albuquerque, New Mexico, United States [doi>10.1145/125826.125848]
• 36: William Pugh , David Wonnacott, Eliminating false data dependences using the Omega test, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.140-151, June 15-19, 1992, San Francisco, California, United States
• 37: William Pugh , David Wonnacott, Experiences with constraint-based array dependence analysis, University of Maryland at College Park, College Park, MD, 1994
• 38: David D. Redell , Yogen K. Dalal , Thomas R. Horsley , Hugh C. Lauer , William C. Lynch , Paul R. McJones , Hal G. Murray , Stephen C. Purcell, Pilot: an operating system for a personal computer, Communications of the ACM, v.23 n.2, p.81-92, Feb. 1980 [doi>10.1145/358818.358822]
• 39: R. Rivest. The MD5 Message-Digest Algorithm. Request for Comments: 1321. MIT Laboratory for Computer Science and RSA Data Security, Inc. (April 1992).
• 40: Fred B. Schneider, Towards Fault-Tolerant and Secure Agentry, Proceedings of the 11th International Workshop on Distributed Algorithms, p.1-14, September 24-26, 1997
• 41: Margo I. Seltzer , Yasuhiro Endo , Christopher Small , Keith A. Smith, Dealing with disaster: surviving misbehaved kernel extensions, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.213-227, October 29-November 01, 1996, Seattle, Washington, United States
• 42: Michael Siff , Satish Chandra , Thomas Ball , Krishna Kunchithapadam , Thomas Reps, Coping with type casts in C, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.180-198, September 06-10, 1999, Toulouse, France
• 43: N.P. Smith. Stack Smashing Vulnerabilities in the UNIX Operating System. http://www'destr~y'net/machines/security' (2000).
• 44: R. E. Strom , D. M. Yellin, Extending Typestate Checking Using Conditional Liveness Analysis, IEEE Transactions on Software Engineering, v.19 n.5, p.478-485, May 1993 [doi>10.1109/32.232013 ]
• 45: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 46: C. Small, and M. A. Seltzer. Comparison of OS Extension Technologies. USENIX 1996 Annual Technical Conference. San Diego, CA. (January 1996).
• 47: Michael Stonebraker, Inclusion of new types in relational data base systems, Readings in database systems (2nd ed.), Morgan Kaufmann Publishers Inc., San Francisco, CA, 1994
• 48: Sun Microsystems, Inc. Java (TM) Plug-in Overview. http://java.sun.com/products/1.1.1/index- 1.1.1.html. (October 1999).
• 49: Norihisa Suzuki , Kiyoshi Ishihata, Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-143, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512963]
• 50: Ariel Tamches , Barton P. Miller, Fine-grained dynamic instrumentation of commodity operating system kernels, Proceedings of the third symposium on Operating systems design and implementation, p.117-130, February 1999, New Orleans, Louisiana, United States
• 51: M. Tamir. ADI: Automatic Derivation of Invariants. IEEE Transactions on Software Engineering SE-6 1. (January 1980).
• 52: David L. Tennenhouse , David J. Wetherall, Towards an active network architecture, ACM SIGCOMM Computer Communication Review, v.26 n.2, p.5-17, April 1996 [doi>10.1145/231699.231701]
• 53: D. Wegner, J. Foster, E. Brewer, and A. Aiken. A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. The 2000 Network and Distributed Systems Security Conference. San Diego, CA. (February 2000).
• 54: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]
• 55: Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.203-216, December 05-08, 1993, Asheville, North Carolina, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Experimentation, Verification