Secure virtual architecture: a safe execution environment for commodity operating systems

ABSTRACT

This paper describes an efficient and robust approach to provide a safe execution environment for an entire operating system, such as Linux, and all its applications. The approach, which we call Secure Virtual Architecture (SVA), defines a virtual, low-level, typed instruction set suitable for executing all code on a system, including kernel and application code. SVA code is translated for execution by a virtual machine transparently, offline or online. SVA aims to enforce fine-grained (object level) memory safety, control-flow integrity, type safety for a subset of objects, and sound analysis. A virtual machine implementing SVA achieves these goals by using a novel approach that exploits properties of existing memory pools in the kernel and by preserving the kernel's explicit control over memory, including custom allocators and explicit deallocation. Furthermore, the safety properties can be encoded compactly as extensions to the SVA type system, allowing the (complex) safety checking compiler to be outside the trusted computing base. SVA also defines a set of OS interface operations that abstract all privileged hardware instructions, allowing the virtual machine to monitor all privileged operations and control the physical resources on a given hardware platform. We have ported the Linux kernel to SVA, treating it as a new architecture, and made only minimal code changes (less than 300 lines of code) to the machine-independent parts of the kernel and device drivers. SVA is able to prevent 4 out of 5 memory safety exploits previously reported for the Linux 2.4.22 kernel for which exploit code is available, and would prevent the fifth one simply by compiling an additional kernel library.

REFERENCES

• 1: Vikram Adve , Chris Lattner , Michael Brukman , Anand Shukla , Brian Gaeke, LLVA: A Low-level Virtual Instruction Set Architecture, Proceedings of the 36th annual IEEE/ACM International Symposium on Microarchitecture, p.205, December 03-05, 2003
• 2: Z. Amsden. Transparent paravirtualization for linux. In Linux Symposium, Ottawa, Canada, Jul 2006.
• 3: Todd M. Austin , Scott E. Breach , Gurindar S. Sohi, Efficient detection of all pointer and array access errors, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.290-301, June 20-24, 1994, Orlando, Florida, United States
• 4: Godmar Back , Wilson C. Hsieh, The KaffeOS Java runtime system, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.583-630, July 2005 [doi>10.1145/1075382.1075383]
• 5: 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
• 6: H. Bos and B. Samwel. Safe kernel programming in the oke. In Proceedings of IEEE OPENARCH, 2002.
• 7: A. Brown. A Decompositional Approach to Computer System Performance. PhD thesis, Harvard College, April 1997.
• 8: J. Criswell, B. Monroe, and V. Adve. A virtual instruction set interface for operating system kernels. In Workshop on the Interaction between Operating Systems and Computer Architecture, Boston, June 2006.
• 9: Grzegorz Czajkowski , Thorsten von Eicken, JRes: a resource accounting interface for Java, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.21-35, October 18-22, 1998, Vancouver, British Columbia, Canada
• 10: 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]
• 11: Dinakar Dhurjati , Sumant Kowshik , Vikram Adve, SAFECode: enforcing alias analysis for weakly typed languages, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 12: 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]
• 13: Paul Barham , Boris Dragovic , Keir Fraser , Steven Hand , Tim Harris , Alex Ho , Rolf Neugebauer , Ian Pratt , Andrew Warfield, Xen and the art of virtualization, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 14: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 15: Ulfar Erlingsson , Fred B. Schneider, The inlined reference monitor approach to security policy enforcement, Cornell University, Ithaca, NY, 2004
• 16: Manuel Fähndrich , Mark Aiken , Chris Hawblitzel , Orion Hodson , Galen Hunt , James R. Larus , Steven Levi, Language support for fast and reliable message-based communication in singularity OS, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
• 17: Bryan Ford , Godmar Back , Greg Benson , Jay Lepreau , Albert Lin , Olin Shivers, The Flux OSKit: a substrate for kernel and language research, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.38-51, October 05-08, 1997, Saint Malo, France
• 18: Rakesh Ghiya , Daniel Lavery , David Sehr, On the importance of points-to analysis and other memory disambiguation methods for C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.47-58, June 2001, Snowbird, Utah, United States
• 19: Michael Golm , Meik Felser , Christian Wawersich , Jürgen Kleinöder, The JX Operating System, Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, p.45-58, June 10-15, 2002
• 20: 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
• 21: G. Guninski. Linux kernel multiple local vulnerabilities, 2005. http://www.securityfocus.com/bid/11956.
• 22: Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, A principled approach to operating system construction in Haskell, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 23: Chris Hawblitzel , Chi-Chao Chang , Grzegorz Czajkowski , Deyu Hu , Thorsten von Eicken, Implementing multiple protection domains in java, Proceedings of the annual conference on USENIX Annual Technical Conference, p.22-22, June 15-19, 1998, New Orleans, Louisiana
• 24: G. C. Hunt and J. R. Larus. Singularity Design Motivation (Singularity Technical Report 1). Technical Report MSR-TR-2004-105, Microsoft Research, Dec 2004.
• 25: 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
• 26: R. W. M. Jones and P. H. J. Kelly. Backwards-compatible bounds checking for arrays and pointers in c programs. In Automated and Algorithmic Debugging, pages 13--26, 1997.
• 27: Chris Lattner , Vikram Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation, Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, p.75, March 20-24, 2004, Palo Alto, California
• 28: Chris Lattner , Vikram Adve, Automatic pool allocation: improving performance by controlling data structure layout in the heap, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 29: Chris Lattner , Andrew Lenharth , Vikram Adve, Making context-sensitive points-to analysis with heap cloning practical for the real world, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 30: Steven McCanne , Van Jacobson, The BSD packet filter: a new architecture for user-level packet capture, Proceedings of the USENIX Winter 1993 Conference Proceedings on USENIX Winter 1993 Conference Proceedings, p.2-2, January 25-29, 1993, San Diego, California
• 31: 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]
• 32: 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]
• 33: George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
• 34: 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
• 35: A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Comm., 2003.
• 36: T. Saulpaugh and C. Mirho. Inside the JavaOS Operating System. Addison-Wesley, Reading, MA, USA, 1999.
• 37: 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
• 38: P. Starzetz. Linux kernel elf core dump local buffer overflow vulnerability. http://www.securityfocus.com/bid/13589.
• 39: P. Starzetz. Linux kernel IGMP multiple vulnerabilities, 2004. http://www.securityfocus.com/bid/11917.
• 40: P. Starzetz and W. Purczynski. Linux kernel setsockopt MCAST\_MSFILTER integer overflow vulnerability, 2004. http://www.securityfocus.com/bid/10179.
• 41: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 42: Michael M. Swift , Muthukaruppan Annamalai , Brian N. Bershad , Henry M. Levy, Recovering device drivers, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.1-1, December 06-08, 2004, San Francisco, CA
• 43: Michael M. Swift , Brian N. Bershad , Henry M. Levy, Improving the reliability of commodity operating systems, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 44: Michael M. Swift , Brian N. Bershad , Henry M. Levy, Improving the reliability of commodity operating systems, ACM Transactions on Computer Systems (TOCS), v.23 n.1, p.77-110, February 2005 [doi>10.1145/1047915.1047919]
• 45: Úlfar Erlingsson , Martín Abadi , Michael Vrable , Mihai Budiu , George C. Necula, XFI: software guards for system address spaces, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
• 46: Ivan Sprundel. Linux kernel bluetooth signed buffer index vulnerability. http://www.securityfocus.com/bid/12911.
• 47: Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, ACM SIGOPS Operating Systems Review, v.27 n.5, p.203-216, Dec. 1993
• 48: 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]
• 49: Nicholas Weaver , Vern Paxson , Stuart Staniford , Robert Cunningham, A taxonomy of computer worms, Proceedings of the 2003 ACM workshop on Rapid malcode, October 27-27, 2003, Washington, DC, USA [doi>10.1145/948187.948190]
• 50: 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 symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
      D.4.7 Organization and Design

General Terms:
Design, Reliability, Security

Keywords:
compiler, memory safety, operating systems, security, type safety, typed assembly language, virtual machine