Singularity: Rethinking the Software StackGalen C. Hunt and James R. Larus Microsoft Research [email protected] operating system embodies a collection of design decisions. Many of the decisions behind WRGD\¶V PRVW SRSXODU RSHUDWLQJ 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. KeywordsOperating systems, safe programming languages, program verification, program specification, sealed process architecture, sealed kernel, software-isolated processes (SIPs), hardware protection domains, manifest-based programs (MBPs), unsafe code tax. 1. INTRODUCTIONEvery operating system embodies a collection of design decisions²some explicit, some implicit. These decisions include the choice of implementation language, the program protection model, the security model, the system abstractions, and many others. Contemporary operating systems²Windows, Linux, Mac OS X, and BSD²share a large number of design decisions. This commonality is not entirely accidental, as these systems are all rooted in OS architectures and development tools of the late ¶V DQG early ¶V. Given the common operating environments, the same programming language, and similar user expectations, it is not surprising that designers of these systems made similar decisions. While some design decisions have withstood the test of time, others have aged less gracefully. The Singularity project started in 2003 to re-examine the design decisions and increasingly obvious shortcomings of existing systems and software stacks. These shortcomings include: wide-spread security vulnerabilities; unexpected interactions among applications; failures caused by errant extensions, plug-ins, and drivers, and a perceived lack of robustness. We believe that many of these problems are attributable to systems that have not evolved far beyond the computer architectures DQG SURJUDPPLQJ ODQJXDJHV RI WKH ¶V DQG ¶V 7KH FRPSXWLQJ HQYLURQPHQW RI WKDW SHULRG ZDV YHU\ different from today. Computers were extremely limited in speed and memory capacity. They were used only by a small group of benign technical literati and were rarely networked or connected to physical devices. None of these requirements still hold, but modern operating systems have not evolved to accommodate the enormous shift in how computers are used. 1.1 A Journey, not a Destination In the Singularity project, we have built a new operating system, a new programming language, and new software verification tools. The Singularity operating system incorporates a new software architecture based on software isolation of processes. Our programming language, Sing# [8], is an extension of C# that provides verifiable, first-class support for OS communication primitives as well as strong support for systems programming and code factoring. The sound verification tools detect programmer errors early in the development cycle. From the beginning, Singularity has been driven by the following question: what would a software platform look like if it was designed from scratch, with the primary goal of improved dependability and trustworthiness? To this end, we have championed three strategies. First, the pervasive use of safe programming languages eliminates many preventable defects, such as buffer overruns. Second, the use of sound program verification tools further guarantees that entire classes of programmer errors are removed from the system early in the development cycle. Third, an improved system architecture stops the propagation of runtime errors at well-defined boundaries, making it easier to achieve robust and correct system behavior. Although dependability is difficult to measure in a research prototype, our experience has convinced us of the practicality of new technologies and design decisions, which we believe will lead to more robust and dependable systems in the future. Singularity is a laboratory for experimentation in new design ideas, not a design solution. While we like to think our current code base represents a significant step forward from prior work, we do not VHH LW DV DQ ³LGHDO´ V\VWHP or an end in itself. A research prototype such as Singularity is intentionally a work in progress; it is a laboratory in which we continue to explore implementations and trade-offs. In the remainder of this paper, we describe the common architectural foundation shared by all Singularity systems. Section 3 describes the implementation of the Singularity kernel which provides the base implementation of that foundation. Section 4 surveys our work over the last three years within the Singularity project to explore new opportunities in the OS and system design space. Finally, in Section 5, we summarize our work to date and discuss areas of future work. 2. ARCHITECTURAL FOUNDATION The Singularity system consists of three key architectural features: software-isolated processes, contract-based channels, and manifest-based programs. Software-isolated processes provide an environment for program execution protected from external interference. Contract-based channels enable fast, verifiable message-based communication between processes. Manifest-37based programs define the code that runs within software-isolated processes and specify its verifiable behavioral properties. A guiding philosophy behind Singularity is one of simplicity over richness. The foundational features respectively provide basic support for execution, communication, and system verification and are a bedrock design upon which dependable, verifiable systems can be built. 2.1 Software-Isolated Processes The first foundational feature common to Singularity systems is the Software-Isolated Process (SIP). Like