Singularity: rethinking the software stack

ABSTRACT

Every operating system embodies a collection of design decisions. Many of the decisions behind today's most popular operating systems have remained unchanged, even as hardware and software have evolved. Operating systems form the foundation of almost every software stack, so inadequacies in present systems have a pervasive impact. This paper describes the efforts of the Singularity project to re-examine these design choices in light of advances in programming languages and verification tools. Singularity systems incorporate three key architectural features: software-isolated processes for protection of programs and system services, contract-based channels for communication, and manifest-based programs for verification of system properties. We describe this foundation in detail and sketch the ongoing research in experimental systems that build upon it.

REFERENCES

• 1: Mark Aiken , Manuel Fähndrich , Chris Hawblitzel , Galen Hunt , James Larus, Deconstructing process isolation, Proceedings of the 2006 workshop on Memory system performance and correctness, October 22-22, 2006, San Jose, California [doi>10.1145/1178597.1178599]
• 2: Allen, D. H., Dhong, S. H., Hofstee, H. P., Leenstra, J., Nowka, K. J., Stasiak, D. L. and Wendel, D. F. Custom Circuit Design as a Driver of Microprocessor Performance. IBM Journal of Research and Development, 44 (6).
• 3: Thomas E. Anderson , Henry M. Levy , Brian N. Bershad , Edward D. Lazowska, The interaction of architecture and operating system design, Proceedings of the fourth international conference on Architectural support for programming languages and operating systems, p.108-120, April 08-11, 1991, Santa Clara, California, United States
• 4: 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
• 5: Koushik Chakraborty , Philip M. Wells , Gurindar S. Sohi, Computation spreading: employing hardware migration to specialize CMP cores on-the-fly, Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, October 21-25, 2006, San Jose, California, USA
• 6: Juan Chen , David Tarditi, A simple typed intermediate language for object-oriented languages, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-49, January 12-14, 2005, Long Beach, California, USA
• 7: ECMA International, ECMA-335 Common Language Infrastructure (CLI), 4th Edition. Technical Report Geneva, Switzerland, 2006.
• 8: 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 ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
• 9: Manuel Fähndrich , Michael Carbin , James R. Larus, Reflective program generation with patterns, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1173706.1173748]
• 10: Robert Fitzgerald , David Tarditi, The case for profile-directed selection of garbage collectors, Proceedings of the 2nd international symposium on Memory management, p.111-120, October 15-16, 2000, Minneapolis, Minnesota, United States
• 11: Chris Hawblitzel , Heng Huang , Lea Wittie , Juan Chen, A garbage-collecting typed assembly language, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190323]
• 12: Jorrit N. Herder , Herbert Bos , Ben Gras , Philip Homburg , Andrew S. Tanenbaum, MINIX 3: a highly reliable, self-repairing operating system, ACM SIGOPS Operating Systems Review, v.40 n.3, July 2006 [doi>10.1145/1151374.1151391]
• 13: Hunt, G., Larus, J., Abadi, M., Aiken, M., Barham, P., Fähndrich, M., Hawblitzel, C., Hodson, O., Levi, S., Murphy, N., Steensgaard, B., Tarditi, D., Wobber, T. and Zill, B., An Overview of the Singularity Project. Technical Report MSR-TR-2005-135, Microsoft Research, 2005.
• 14: Galen Hunt , Mark Aiken , Manuel Fähndrich , Chris Hawblitzel , Orion Hodson , James Larus , Steven Levi , Bjarne Steensgaard , David Tarditi , Ted Wobber, Sealing OS processes to improve dependability and safety, Proceedings of the ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, March 21-23, 2007, Lisbon, Portugal
• 15: Poonacha Kongetira , Kathirgamar Aingaran , Kunle Olukotun, Niagara: A 32-Way Multithreaded Sparc Processor, IEEE Micro, v.25 n.2, p.21-29, March 2005 [doi>10.1109/MM.2005.35]
• 16: Butler Lampson , Martín Abadi , Michael Burrows , Edward Wobber, Authentication in distributed systems: theory and practice, ACM Transactions on Computer Systems (TOCS), v.10 n.4, p.265-310, Nov. 1992 [doi>10.1145/138873.138874]
• 17: James R. Larus , Michael Parkes, Using Cohort-Scheduling to Enhance Server Performance, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.103-114, June 10-15, 2002
• 18: League, C. A Type-Preserving Compiler Infrastructure, Yale University, New Haven, CT, 2002.
• 19: Henry M. Levy, Capability-Based Computer Systems, Butterworth-Heinemann, Newton, MA, 1984
• 20: Microsoft Corporation, Scalable Networking: Network Protocol Offload - Introducing TCP Chimney. Technical Report Redmond, WA, 2004.
• 21: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 22: 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
• 23: Saltzer, J. H. and Schroeder, M. D. The protection of information in computer systems. Proceedings of the IEEE, 63 (9). 1268--1308.
• 24: Jonathan S. Shapiro , Jonathan M. Smith , David J. Farber, EROS: a fast capability system, Proceedings of the seventeenth ACM symposium on Operating systems principles, p.170-185, December 12-15, 1999, Charleston, South Carolina, United States
• 25: Michael F. Spear , Tom Roeder , Orion Hodson , Galen C. Hunt , Steven Levi, Solving the starting problem: device drivers as self-describing artifacts, Proceedings of the ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
• 26: Daniel C. Swinehart , Polle T. Zellweger , Richard J. Beach , Robert B. Hagmann, A structural view of the Cedar programming environment, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.4, p.419-490, Oct. 1986 [doi>10.1145/6465.6466]
• 27: Vangal, S., Howard, J., Ruhl, G., Dighe, S., Wilson, H., Tschanz, J., Finan, D., Iyer, P., Singh, A., Jacob, T., Jain, S., Venkataraman, S., Hoskote, Y. and Borkar, N., An 80-Tile 1.28TFLPOPS Network-on-Chip in 65nm CMOS. In 2007 IEEE International Solid-State Circuits Conference, San Francisco, CA, February 2007.
• 28: Rob von Behren , Jeremy Condit , Feng Zhou , George C. Necula , Eric Brewer, Capriccio: scalable threads for internet services, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 29: Edward Wobber , Martín Abadi , Michael Burrows , Butler Lampson, Authentication in the Taos operating system, ACM Transactions on Computer Systems (TOCS), v.12 n.1, p.3-32, Feb. 1994 [doi>10.1145/174613.174614]
• 30: Ted Wobber , Aydan Yumerefendi , Martín Abadi , Andrew Birrell , Daniel R. Simon, Authorizing applications in singularity, Proceedings of the ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, March 21-23, 2007, Lisbon, Portugal

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General
          Subjects: Protection mechanisms
      D.2.4 Software/Program Verification
      D.2.5 Testing and Debugging

General Terms:
Design, Management, Security, Verification

Keywords:
hardware protection domains, manifest-based programs (MBPs), operating systems, program specification, program verification, safe programming languages, sealed kernel, sealed process architecture, software-isolated processes (SIPs), unsafe code tax