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.
- 1.M. Abadi, and L. Cardelli. A Theory of Objects. Monographs in Computer Science, D. Gries, and F. B. Schneider (Ed.). Springer- Verlag New York. (1996).]] Google ScholarDigital Library
- 2.B. Bershad, S. Savage, P. Pardyak, E. G. Sirer, M. Fiucynski, D. Becker, S. Eggers, and C. Chambers. Extensibility, Safety, and Performance in the SPIN Operating System, 15th Symposium on Operating System Principles. Copper Mountain, CO. (December 1995).]] Google ScholarDigital Library
- 3.B. Alpern, and F. B. Schneider. Recognizing Safety and Liveness. Distributed Computing 2 3. (1987).]]Google Scholar
- 4.R. Bodik, R. Gupta, and V. Sarkar. ABCD: Eliminating Array Bounds Checks on Demand. SIGPLAN Conference on Programming Language Design and Implementation. Vancouver B.C., Canada. (June 2000).]] Google ScholarDigital Library
- 5.D.R. Chase, M. Wegman, and F. Zadeck. Analysis of Pointers and Structures. SIGPLAN Conference on Programming Language Design and Implementation. New York, NY. (1990).]] Google ScholarDigital Library
- 6.T. Chiueh, G. Venkitachalam, P. Pradhan. Integrating Segmentation and Paging Protection for Safe, Efficient and Transparent Software Extensions. 17th ACM Symposium on Operating Systems Principles. Charleston, SC. (December 1999).]] Google ScholarDigital Library
- 7.P. Cousot, and N. Halbwachs. Automatic Discovery of Linear Restraints Among Variables of a Program. Fifth Annual ACM Symposium on Principles of Programming Languages. Tucson, AZ. (January 1978).]] Google ScholarDigital Library
- 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).]]Google Scholar
- 9.E.W. Dijkstra. A Discipline of Programming. Prentice-Hall. Englewood Cliffs, NJ. (1976).]] Google ScholarDigital Library
- 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).]]Google Scholar
- 11.D. Engler, M. F. Kaashoek, and J. O'Toole. Exokernel: An Operating System Architecture for Application-Level Resource Management. 15th Symposium on Operating System Principles. Copper Mountain, CO. (December 1995).]] Google ScholarDigital Library
- 12.C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM 12 10. (October 1969).]] Google ScholarDigital Library
- 13.Illustra Information Technologies. Illustra DataBlade Developer's Kit Architecture Manual, Release 1.1. (1994).]]Google Scholar
- 14.JavaSoft. Java Native Interface Specification. Release 1.1 (May 1997).]]Google Scholar
- 15.jPVM: A Native Methods Interface to PVM for the Java Platform. http://www.chmsr.gatech.edu/jPVM. (2000).]]Google Scholar
- 16.S. Katz, and Z. Manna. A Heuristic Approach to Program Verification. 3rd International Conference on Artificial Intelligence. (August 1973).]]Google ScholarDigital Library
- 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).]]Google Scholar
- 18.X. Leroy, and F. Rouaix. Security Properties of Typed Applets. 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. San Diego, CA. (January 1998).]] Google ScholarDigital Library
- 19.Lindholm T., and F. Yellin. The Java (TM) Virtual Machine Specification. Second Edition. http://java.sun.com/docs/books/vmspec/2ndedition/html/VMSpec ToC.doc.html. (1999).]] Google ScholarDigital Library
- 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).]] Google ScholarDigital Library
- 21.Misrosoft. Microsoft COM Technologies-Information and Resources for the Component Object Model-Based Technologies. http://www.microsoft.com/com. (March 2000)]]Google Scholar
- 22.B.P. Miller, M. D. Callaghan, J. M. Cargille, J. K. Hollingsworth, R. B. Irvin, K. L. Karavanic, K. Kunchithapadam, and T. Newhall.The Paradyn Parallel Performance Measurement Tools. IEEE Computer 28 11. (November 1995).]] Google ScholarDigital Library
- 23.J.C. Mogul, R. F. Rashid, and M. J. Accetta. The Packet Filter: An Efficient Mechanism for User-Level Network Code. ACM Symposium on Operating Systems Principles. Austin, TX. (November 1987).]] Google ScholarDigital Library
- 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).]]Google Scholar
- 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).]]Google Scholar
- 26.G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to Typed Assembly Language. 25th Annual ACM Symposium on Principles of Programming Languages. San Diego, CA. (January 1998).]] Google ScholarDigital Library
- 27.G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-Based Typed Assembly Language. 1998 Workshop on Types in Compilation. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, 1473. Springer- Verlag 1998.]] Google ScholarDigital Library
- 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).]]Google Scholar
- 29.S. S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers, Inc. (1997).]] Google ScholarDigital Library
- 30.G. Necula. Compiling with Proofs. Ph.D. Dissertation, Carnegie Mellon University. (September 1998).]] Google ScholarDigital Library
- 31.G. Necula, and P. Lee. The Design and Implementation of a Certifying Compiler. ACM SIGPLAN Conference on Programming Language Design and Implementation. Montreal, Canada. (June 1998).]] Google ScholarDigital Library
- 32.G. Necula. Proof-Carrying Code. 24th Annual ACM Symposium on Principles of Programming Languages. Paris, France. (January 1997).]] Google ScholarDigital Library
- 33.Netscape. Browser Plug-ins, 1999. http://h~me'netscape'c~m/plugins/index'html']]Google Scholar
- 34.C. Pu, T. Audrey, A. Black, C. Consel, C. Cowan, J. Inouye, L. Kethana, J. Walpole, and K. Zhang. Optimistic Incremental Specialization: Streamlining a Commercial Operating System. 15th ACM Symposium on Operating Systems Principles. Copper Mountain, CO. (December 1995).]] Google ScholarDigital Library
- 35.W. Pugh. The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. Supercomputing. Albuquerque, NM. (November 1991).]] Google ScholarDigital Library
- 36.W. Pugh, and D. Wonnacott. Eliminating False Data Dependences Using the Omega Test. ACM SIGPLAN Conference on Programming Language Design and Implementation. San Francisco, CA. (June 1992).]] Google ScholarDigital Library
- 37.W. Pugh, and D. Wonnacott. Experience with Constraint-Based Array Dependence Analysis. Technical Report CS-TR-3371. University of Maryland. (1994).]] Google ScholarDigital Library
- 38.D.D. Redell, Y. K. Dalal, T. R. Horsley, H. C. Lauer, W. C. Lynch, P. R. McJones, H. G. Murray, and S. C. Purcell. Pilot: An Operating System for a Personal Computer. Communications of the ACM 23 2. (February 1980).]] Google ScholarDigital Library
- 39.R. Rivest. The MD5 Message-Digest Algorithm. Request for Comments: 1321. MIT Laboratory for Computer Science and RSA Data Security, Inc. (April 1992).]] Google ScholarDigital Library
- 40.F.B. Schneider. Towards Fault-Tolerant and Secure Agentry. llth International Workshop on Distributed Algorithms. Saarbrticken, Germany. (September 1997).]] Google ScholarDigital Library
- 41.M.I. Seltzer, Y. Endo, C. Small, and K. A. Smith. Dealing With Disaster: Surviving Misbehaved Kernel Extensions. 2nd USENIX Symposium on Operating Systems Design and Implementation. Seattle, WA. (October 1996).]] Google ScholarDigital Library
- 42.M. Sift, S. Chandra, T. Ball, K. Kunchithapadam, and T. Reps. Coping with type casts in C. Seventh European Software Engineering Conference and Seventh ACM SIGSOFT Symposium on the Foundations of Software Engineering. Toulouse, France. (September 1999).]] Google ScholarDigital Library
- 43.N.P. Smith. Stack Smashing Vulnerabilities in the UNIX Operating System. http://www'destr~y'net/machines/security' (2000).]]Google Scholar
- 44.R. Strom, and D. M. Yellin. Extending Typestate Checking Using Conditional Liveness Analysis. IEEE Transactions on Software Engineering 19 5. (May 1993).]] Google ScholarDigital Library
- 45.R. Strom, and S. Yemini. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering 12 1. (January 1986).]] Google ScholarDigital Library
- 46.C. Small, and M. A. Seltzer. Comparison of OS Extension Technologies. USENIX 1996 Annual Technical Conference. San Diego, CA. (January 1996).]] Google ScholarDigital Library
- 47.M. Stonebraker. Inclusion of New Types in Relational Data Base Systems. Readings in Database Systems. Second Edition. Michael Stonebraker (Ed.). (1994).]] Google ScholarDigital Library
- 48.Sun Microsystems, Inc. Java (TM) Plug-in Overview. http://java.sun.com/products/1.1.1/index- 1.1.1.html. (October 1999).]]Google Scholar
- 49.N. Susuki, and K. Ishihata. Implementation of an Array Bound Checker. 4th ACM Symposium on Principles of Programming Languages. Los Angeles, CA. (January 1977).]] Google ScholarDigital Library
- 50.A. Tamches, and B. P. Miller. Fine-Grained Dynamic Instrumentation of Commodity Operating System Kernels. Third Symposium on Operating System Design and Implementation. New Orleans, LA. (February 1999).]] Google ScholarDigital Library
- 51.M. Tamir. ADI: Automatic Derivation of Invariants. IEEE Transactions on Software Engineering SE-6 1. (January 1980).]]Google Scholar
- 52.D. Tennenhouse, and D. Wetherall. Towards an Active Network Architecture. Computer Communication Review 26 2. (April 1996).]] Google ScholarDigital Library
- 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).]]Google Scholar
- 54.B. Wegbreit. The Synthesis of Loop Predicates. Communications ofthe ACM 17 2. (February 1974).]] Google ScholarDigital Library
- 55.R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient Software-Based Fault Isolation. 14th Symposium on Operating System Principles. Asheville, NC. (December 1993).]] Google ScholarDigital Library
Index Terms
- Safety checking of machine code
Recommendations
Safety checking of machine code
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 ...
Checking memory safety with blast
FASE'05: Proceedings of the 8th international conference, held as part of the joint European Conference on Theory and Practice of Software conference on Fundamental Approaches to Software EngineeringBlast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast statically proves that either the program satisfies the safety property or the program has an ...
Comments