Paper Discussion - Fall 2008 - CS 736

Singularity: Rethinking the Software Stack describes a Microsoft software architecture used to construct a robust and dependable research operating system by leveraging a variety of "recent" advances in both programming languages and approaches to specifying/verifying program behavior.

The most prominent feature within Singularity is the notion of a "software isolated process", or SIP. SIP's are processes that run in kernel space and do not share data structures. Instead, they communicate via high-level communication "channels" using message-passing primitives. Messages sent along channels are always delivered in-order by the kernel.

The message-passing primitives are provided by a new programming language, Sing#, an extended version of Microsoft's C# language. C# brings a variety of technologies to the scene: most notably strong {type/array-bound}-checking and automagical garbage collection. Sing# adds support for statically-verifiable "contracts" between software components: essentially protocol specifications for the communication channels between drivers in Singularity.

It sounds like the Singularity project is on the right track to building an operating system of manageable complexity capable of supporting a plethora of interacting, user-written (i.e. poorly-written) drivers. Requiring a specification for how drivers talk to each other should help aid testing and ultimately improve system stability (provided the specifications are properly defined by driver authors, instead of circumvented for the sake of convenience). Garbage collection in both SIP's and the kernel should help prevent memory-leaks reducing system stability WRT time, though likely at a performance cost compared to a correctly-written driven that explicitly manages its memory.

Perhaps more serious concerns for the Singularity project are verifying the correctness of the (presumably complex) routines used to enforce driver isolation and accomplish garbage collection. Also, if the driver isolation routine has to be run against every existing driver for every new driver installed on the system, can the routine be run in a reasonable amount of time? Finally, big restrictions were placed on message-passing (no complex objects, fixed length queues). Will operating within these restrictions result in unnecessarily complex driver code?

Singularity: Rethinking the Software Stack

This paper from Microsoft Research introduces a new operating system that incorporates three key architecture features: software-isolated processes, contract-based channels and manifest-based programs. Singularity was implemented in Sing#, a new programming language developed for this purpose that provides support for OS communication primitives. Also new software verification tools were developed to early detect programming errors.

The main goal of this research is to overcome the shortcomings that the most popular OS present today; these problems have its reason in the fact that current OS were design in the 70's and computers and programming languages back then presented very different characteristics. The main problems that they consider are: security vulnerabilities, unsafe interprocess interaction, failures due software extensions. With the solutions proposed they claim to implement a more dependable OS than the currently existing ones.

1-Software-isolated processes (SIP) are closed objects that may not be accessed or modified by other processes. The isolation and protection is provided by software.

2-Contract-based channels are the only way of communication between two SIPs. Contract channels consist on different possible message types and a set of possible states. A channel endpoints belong to only two particular threads. Contract channels are described in the Sing# language.

3-Manifest-based programs (MBP) are programs described by manifests. Manifests specify the resources required by the program, the capabilities and the interactions with other programs. All the programs in Singularity need to be MBP. Manifests allow static and dynamic verification of the program behavior, this makes the execution of applications safer.

4-The kernel of Singularity is a micro-kernel. It provides support to the previously mentioned abstractions. SIPs access kernel primitives through the Application Binary Interface (ABI), it implements the state isolation invariant: a SIP can not modify another SIP through an ABI function. The memory management divides the address space and assigns it to the SIPS and the exchange heap is used for communication; it implements the memory independence invariant: pointers can not point to other SIPs memory. Because SIPs are closed objects, each one has its own garbage collector, avoiding common deallocation errors.

The goal of this research was to implement a dependable and clear system, paying less attention to other important considerations such as compatibility and performance. Not providing application and driver compatibility is an important drawback nowadays. Some of the communication and process creation is more efficient than in other OS, but in general Singularity does not present special higher performance.

The idea of offering more protection through software instead of just relying on hardware protection makes Singularity more dependable but requires the implementation of new software verification mechanisms that have to be very reliable.

Summary
The Singularity paper reflects on the prevailing design choices in operating systems in the context of advances in programming languages and verification tools and proposes a design that is built around three architectural features - software isolated processes, contract based communication channels and manifest based programs

Problem attempted
The objective of this paper is to exploit the advantages in languages and verification tools, to design and build an operating system that is much more dependable than the contemporary operating systems.

Contributions

1. The paper introduces the concept of Software Isolated Processes (SIP) which is markedly different from the processes that are currently used. The most important difference is that SIPs are isolated by software verification instead of hardware protection. Thus SIPs rely on programming language type and memory safety for isolation. This means that multiple SIPs and the kernel can share a single kernel-mode address space.

2. SIPs do not share writable memory and consequently all communication between SIPs happen through contract based channels. The key advantage in a channel based communication system is that the compiler can statically verify that the send and receive operations over channels conform to the state machine described in contract's protocol.

3. Manifest Based Programs (MBP) is the third important architectural feature introduced by this paper. To begin execution, a user invokes a manifest. A manifest is a machine-checkable expression of an MBP's expected behaviour. Thus static as well as dynamic verification of properties of a MBP is possible with the help of information provided by the manifest.

4. In operating systems that depend on hardware protection, functions with privileged instructions must always execute in kernel. But Singularity systems offer the flexibility of placing privileged instructions in trusted functions that run inside SIPs, thus improving performance by minimizing channel communication.

5. By implementing process protection in software, SIPs have eliminated the necessity of I/O processors having separate memory management units. Additionally, since MBPs are in abstract Microsoft Intermediate Language (MSIL), they can be converted to the ISA of any I/O processor. This eliminates the trouble of processors having to keep up backwards compatibility.

Flaws

1. SIPs are protected by software verification instead of memory management hardware. But there could always be some vulnerabilities in the way protection is implemented in software leading to potential failures as against the foolproof protection implemented by hardware. Besides, protection implemented in hardware is faster than software protection, in spite of additional costs such as page table maintenance.

What it makes easier

1. The overhead involved in creating an SIP is much lesser than that involved in creating a conventional process. This is because SIP can be created without creating page tables or flushing TLBs. Context siwthes between SIPs have very low overhead because TLBs need not be flushed now.

2. In Singularity, since all processes share a single address space, we need only one security architecture, recovery model and program model in comparison to many levels of redundant mechanisms in current systems.

3. The device drivers and file systems are now user replacable services that execute in SIPs outisde the kernel. Taking away the device drivers from the kernel makes the kernel a lot lighter.

4. By restricting the SIP to not having pointers pointing to other SIP's objects, garbage collection of a SIP can be done without the cooperation of other SIPs.

What it makes harder

1. Driver compatibility has been abandoned to gain freedom in exploring many design options. But this means that code for drivers have to be written from scratch.

2. Message based communication has almost always been much slower than shared-memory based communication.

summary
the paper introduces singularity which employs safe programming languages and program verification to build a failsafe and reliable operating operating system

problem addressed
The authors adress the problems of perceived lack of robustness, vulnerabilites, unexpected interactions among applications and failures due to extensions and plugins, as faced by contemporary operating systems. The claim is that these flaws prevail due to design decisions made in the 1960s-70s which failed to see further revision thereafter. Singularity aims to re-examine these design choices and develop an operating system which addresses the resultant issues. Primary focus is observed to be on security through type safe languages and verifiability.

system organization
Three central aspects to the singularity system are (1) Software isolated processes (2) contract-based channels for communication and (3) manifest based programs. SIPs are anologous to processes in present day systems but are isolated through software verification rather than hardware protection. Limits on dynamic behaviour of SIPs are argued to guarantee their isolation and hence the reliability of the system. The contract based channels provide a verifiable communication mechanism for the SIPs. Given the static verifiability, the system can be proved to be free of unexpected/errant states. Manifests form a sort of metadata to programs in Singularity. They describe the code resources, required system resources, capabilities, dependencies etc, thereby again allowing for verifiability (majorly static, with a few runtime checks).

what it makes easier
- security is built into the system and hence catering to secure applications could be easier
- zero copy exchange of large amounts of data allows for ease of use for IPC in some situations
- given the design of SIPs as more statically verified and with little runtime overhead, creation of SIPs, context switches etc are easier

what it makes harder
- porting existing applications would require going back to square one.
- the virtual memory support seems limited and may be a cause of concern when writing hugely memory consuming applications

contribution
- type safety and verifiability: This is the crux of the paper. Albiet the lack of full fledged evaluation on how successful these mechanism are in improving reliability, the focus on them is particularly strong and seminal. SIPs, contract-based channels and MBPs are other noteworthy contributions, but have already been explained above.
- the idea of processors specializing to tasks dynamically is another interesting contribution and could hold value for the future.
- typed assembly languages allowing some extend of safety checking in assembly code is another interesting contribution

flaws
- What you can do with the system seems highly limited given the numerous restrictions/invariants on it.
- Performance has been officially declared a non-goal by the paper ;)
- From what I gather from the paper, I would compare the whole system to a freestanding sing# virtual machine rather than an operating system.

In this paper, the authors present Singularity, an experimental operating system built by Microsoft research. They first describe the philosophy behind its design and then give details about its basic features.

The authors are trying to build a reliable and secure system which will overcome problems that are present in the existing operating systems. Their primary goal is to experiment with novel ideas and to examine new opportunities in the design of operating systems. For this reason, they build the entire system from scratch.

Singularity is a highly dependable OS. Its basic architecture features are SIPs, the contract-based channels and the manifest-based programs. Execution of each user program occurs within the context of a SIP. SIPs are isolated processes which execute autonomously and communicate with each other through contract-based channels. SIPs can’t share memory with other SIPs. They can exchange data by using an area of memory, known as exchange heap. All processes share the same address space. SIPs start execution only if a manifest is invoked. The manifest describes the properties of the SIP.

The authors have introduced many interesting ideas .In my opinion, the main contribution of the system is the software isolation of processes, instead of hardware isolation. This feature combined with the code verification makes the system more efficient and simultaneously ensures that the code is safe. Another interesting feature of the system is the communication among SIPs. SIPs can communicate through channels or via the kernel. This type of communication is very safe and helps preventing mistakes that may occur. Some other contributions are the scheduling which is very fast, the flexibility that each process has to choose its own garbage collector policy and the use of manifests instead of executable files.

The different design of the system combined with the use of Sing# language make it difficult to port existing applications to the system. In my opinion, this constitutes the main flaw of the system.

Summary:
This paper describes an experimental operating system which is built in the singularity project by using a new programming language, Sing# which is the extension of C#. The Singularity system consists of three key architectural features which are software-isolated processes, contract-based channels, and manifest-based programs which significantly bring up improvements in dependability of system when compared with the previous operating systems.
The problem the paper was trying to deal with:
By knowing the inadequacies existing in the present operating systems, the authors aim to develop techniques and technologies that result in significant improvements in dependability and reliability of the operating system by using the advanced languages, tools developed recently.
Contributions
1． Three key architectural features of the Singularity system including software-isolated processes, contract-based channels and manifest-based programs provide a high protection, fast communication and high dependability to the system.
2． The singularity system provides a foundational feature which is Software-Isolated process (SIP). When compared with hardware protected resources, a SIP can just cause very low overhead, which makes it practical to use SIPs as a fine-grain isolation and extension mechanism to replace the conventional mechanisms of hardware protected processes and unprotected dynamic code loading.
3． The singularity system provides contract-based channels providing an efficient way of inter process communication by allowing zero-copy exchange of large amounts of data through them.
4． The singularity system also provides Manifest-Based Programs (MBP) requiring no code is allowed to run on a singularity system without a manifest and highly-probably significantly reducing the costs of system administration,
Flaws:
The paper claims that Manifest-Based Programs will play a role in significantly reducing the costs of system administration, but no completed the experimental work provided to validate that claim. And the Singularity operating system design is targeted to a very high level which brings a high complexity to implement it.
What it makes easier:
The highly developed hardware and software makes it easier to implement a complicated operating system like singularity. The existence of Software-Isolated Process makes it easier to cut down overhead because it can be created without creating page tables or flushing TLBs. And the existence of Contract-Based Channels in the singularity system makes it easier to communicate between SIPs.

What it makes harder:
The singularity kernel provides the base abstractions of software-isolated processes, contract-based channels and manifest-based programs, which brings high complexity to the system and make the implementation harder.

Singularity : Rethinking the Software Stack

Summary
The paper discusses "Singularity" - a dependable and trust-worthy operating system built using the Sing# ( a memory safe, typed checked ) language that relies on static analysis & verification of application code to provide software based process isolation for protection rather than using hardware protection mechanisms. It also provides novel contract based communication channels for IPC , Manifest based programs for signed and verified software installation, System Invariants for a protected system.

Description of the problem being solved

The authors are trying to build a highly dependable yet performing operating system based on untraditional ( not constrained by compatibility to existing operating systems ) design choices based on advances in programing languages, static analysis and verification.

Contributions of the paper

a) Protection through software isolated processes that relies on static analysis, program verification, type and memory safety of Sing# is a novel concept.

b) The kernel and all processes sharing the same virtual address space is novel and this allows for performance improvements like cheaper process context switches.

c) Contract based communication channels serve as a safe inter process communication mechanism and also make possible the verification of communication contract and prevention & detection of coding bugs during compilation.

d) Manifest based programs provide a way of identifying and verifying applications. They allow operating system managed software installations making vulnarabilities and malware a theoretical impossibilty.

e) Making the Application Binary Interface between kernel and applications inlineable makes system calls very efficient.

f) Operating System as a managed code written in a memory safe, type checked language called Sing# provides advantages like garbage collection, easier adaptation to many-core processors and dedicated processors in programmable I/O devices.

Flaws in the paper

a) There is too much reliance on the robustness and correctness of the operating system software itself for protection mechanisms. Bugs in complex systems like operating system, garbage collectors are practical and any vulnerability discovered can potentially cause severe damages to the security of all the systems using Singularity. Though hardware based protection mechanisms can coexist for deeper protection, the paper stresses on software based protection as a philosophy.

b) Singularity has a lot of system invariants like "pointers must point to SIP's own memory or pointers owned by the SIP in the exchange heap" and rules like "each cycle in the state transition of a contract contains atleast one receive and send action" - that make the system tight and rigid making software development harder.

What is made easier?

a) Development of a safe , dependable computing environment is made easier. Security Vulnerabilities in applications are theoretically impossible.

b) Debugging and Verification phases of Application development is made easy because of the excellent static analysis , verification tools and garbage collection facilities available.

c) Extendability of the OS to take advantage of "many core" processors or dedicate processors in I/O devices is made easier.

What is made harder?

a) The design and implementation part of the Application development is made harder due to the memory safe and typed language , system invariants of the OS.

b) Porting existing applications to Singularity is made difficult because of the untraditional and new design choices in the OS.

Singularity is an OS built for experiments. With the system's core design principles, including software-only isolation and tightly-bound support for automatic verification, the authors have departed significantly from traditional OS construction. I say this, despite having noticed some remarkable similarities to Pilot.

It is tempting to identify the Software-Isolated Process (SIP) as the most significant contribution of this work. Software-made guarantees over code, however, do not themselves make a new concept, as we observed this from the Pilot operating system. What is actually new here is the reliance of SIPs on static verification and manifest-based execution, tools beyond the scope of compiler errors, to make incorrect programs more difficult to write. Contracts over shared communication channels, and particular their inclusion of state machine-based checking of acceptable properties, are a particularly neat application of static analysis to a difficult problem: communication. That the combination of these components, all having verifiably good behavior, have created an acceptably-performant OS is a significant achievement. Their anecdotal evidence (perhaps more the bulk of their evaluation techniques) supports the power of these tools in creating error-free programs.

As a main-stream OS candidate, however, Singularity does not measure as well. The authors make no bones about their intentions to create an OS that is good for experimentation, while not necessarily fool-proof. In doing so, they make a key decision (exactly as the authors of Pilot) to help prevent erroneous code while more or less ignoring malicious code (which we know is a real problem). SIPs are a demonstration of a compromise made to this end, where pointers (the most open door to a system from a piece of software) are permitted to make system programming possible. I fear that any use of pointers without hardware to prevent indiscriminate access opens the door to malicious behavior, and the authors say nothing that really convinces me otherwise. This is all underlined by the fact that the garbage collector is not implemented with the same restrictions, and so may create even more open doors through erroneous code.

In spite of my fears for the security of this system, I think it presents several really good ideas that deserve the attention of the community. Static verification, integrated with an environment as it is in Singularity, could bring tremendous benefits to software in almost all other contexts. I wish, in fact, that I had access to such tools for my own work.

Summary

Paper talk about experimental operating system Singularity , which is developed using functionality of advance programming language. Paper talks about three architecture feature Software Isolated Processes (SIP) ,Contract based channel and Manifest based program (MBP).

Problem Trying to solve

Most of the current operating system are designed and developed in 1960’s and 1970’s. Their design decision were influenced by architecture and programming language of earlier time.As computing environment have evolved drastically so most of the operating system face problem such as security vulnerabilities and unexpected interaction among applications. Paper proposes a new operating system from scratch using advance programming language of today for current computing environment.

Work Summary/Contribution

1. Most operating systems enforce process isolation through hardware protection mechanisms such as memory segmentation, page mapping, and differentiated user and kernel instructions. Singularity is a new operating system that uses software mechanisms to enforce process isolation.
2. Contract based channel enable fast , verifiable message based communication between process. As exchange data is kept in external heap memory and transferring data from one process to another just require passing pointer. Which is called zero-copy exchange
3. zero-copy exchange communication allows copying of data across multiple application without any overhead as data is not required to be copied from one application to another
4. Manifesto Based Program enable static and dynamic verification of program property.
5. Linked stack is used to reduce thread memory overhead. Linked stack allows thread to grow on demand.

Flaws

One flaw I can find in paper is constraint on number of pointer that can refer to a block. In current programming scenario multiple pointer to a block of data enable easier transfer of data between function stacks. Different pointer can work on different part of block. one pointer to block will limit all such approach to a block.

What it makes easier

Garbage collection is really easy in Singularity . As atmost one thread can point to a block. So in case SIP termicate block can be collected without worrying about other SIP pointing so same block.

What it makes Harder

If SIP want to pass some data which is local to its data space then it needs to copy this data to exchange heap first and then pass pointer to exchange heap block. This put overhead on data exchange.

Summary
Galen and James in this paper present a new operating system,Singularity that relies on type safe languages and verification tools for building a robust yet efficient system. The operating system is designed using Sing# and currently allows programs only in that language. It also uses system constructs such as Software Isolated Processes(SIP), Manifest based Programs(MBP) and Contract based channels(CBC) to ensure the verifiability and robustness of the system.

Problem
The authors feel that the current operating systems have been built based on state of affairs in 1960-70's. The design decisions made in this period, though sensible for the constraints for that era, no more have any value. These systems should be redesigned without being restricted by backward compatibility with existing systems.

Contributions
- The entire system is built in such a way that all the programs can be statically verified using software(that is during the installation or compilation) as a result, they don't cause any surprises during runtime. Software verification also seems to get rid of many of the hardware bottlenecks on context switches such as TLB flush.
- They propose the idea of each process being completely isolated from each other.(SIP) This isolation ensures program verification, garbage collection, fault isolation of each process. It also allows each SIP to run on separate processor which ensures code/data locality.Since no memory is shared, they provide an exchange heap managed by the kernel.
- For any interprocess communication, the program provides a finite state automaton(contract) to ensure static verifiability of the system. This also ensures that no process can send too many messages or miss a particular state.
- Each program provides a manifesto(MBP) regarding its requirements, capabilities, communication channels, which enables further static verification of the system.
- It also uses software verification to prevent invalid memory accesses and buffer overflow exploits. Also, by just the virtue of only allowing type safe language implementations, many of the exploits are rendered impossible.
- The OS micro-kernel provides an interface for system calls, ABI that allows versioned system calls instead of bothering about backward capability of each system call. This may increase the ABI code bloat but also provides more flexibility for future developments.

Flaws
- The design is very restrictive as it currently allows only implementations in Sing# or type safe C# for applications.
- Since all applications share the address space with a 32 bit addressing, this would limit the available space for each application(if no hardware protection is used).
- Building any application on this system has too many extra requirements apart from just the code. Writing manifests and contracts for each application, is something that developers are not used to.
- Since there is no hardware protection at all, any flaw in the verification system or any other entry point can leave the system vulnerable.

Design
The entire OS is designed as a micro-kernel with each SIP being separate processes communicating through channels and an exchange heap. The system level calls are performed through a strongly versioned ABI interface. Each program is compiled and verified during its installation for possible bugs.

Easier
- Since it has many verification tools, it can help in ensuring fewer bugs such as invalid memory accesses or unhandled states. This along with the isolated processes concept can prevent many BSOD's caused in the Windows system.

Harder
- As mentioned before, writing/maintaining any application for this rigid system would involve a lot more effort than just writing the code.

Summary
The paper describes Singularity, a microkernel operating system, designed from scratch and based upon the use of type and memory safety mechanisms built into programming languages, such as C#.

Problem
This system is trying to address the problem that operating systems are undependable and untrustworthy and that applications and drivers often have unexpected interactions and exploit security vulnerabilities.

Proposed Organization
The proposed system provides Software-Isolated Processes (SIPs). SIPs share no data and can communicate with each other only through contract-based channels. Code is sealed and separate from a process’s object space, and only one process can have a pointer to data at a time. As such, SIPs are sort of a security primitive that rely on the type and memory safety of the language compiler rather than hardware isolation. Channels provide a lossless in-order bi-directional queue and are described by a contract, which consists of message declarations and a specification of states and transitions. As well, each program has a manifest that describes a program’s required resources and dependencies and allows for Singularity to verify type and memory safety, correct usage of channel contracts, absence of privileged instructions, etc.

Contributions
SIPs have certain speed advantages that are described in the paper, and also provide a good deal of control to the process over various aspects including garbage collection. This alone is nothing new, but Singularity is trying to address problems with problematic software interactions and is providing a mechanism of isolation that just isn’t present in and doesn’t seem to have been much of concern for the designers of similar systems such as Pilot. A number of their “explorations” deserve further exploration and are interesting in their own right, aside from their use in this particular operating system. One such exploration, typed assembly language, attempts to deal with the very real issue that verified intermediate code may have bugs after it is optimized and compiled into assembly language. The ability to verify typed assembly code would close this potential hole in the system.

Flaws
To say the least, this was not a light read.

Summary:
This paper presents Singularity, a clean-slate design for building a software system which overcomes the shortcomings of the state-of-the-art operating systems, such as wide-spread security vulnerabilities and unexpected interactions among applications, etc. Singularity uses safe programming language (Sing#) to eliminate preventable defects, soung program verificatin tools to remove programmer errors and finally an improved system architecture to stop propoagation of run-time errors (SIP).

Problem:
With the aim to build a dependable and trustworthy system, Singularity presents three novel features: software isolated processes fr protection, contract-based channels for communication and manifest-based programs for system verification. Notable feature of Singularity is the run-time mapping of SIPs to different protection domain, which allow analogies to hardware-protected microkernel systems \cite{MINIX}, to monolithic OS and hybrid combinations.

Contribution:
- Idea of software isolated processes: Instead of hardware-based protection, in Singularity, one can create a SIP without creating page tables or flushin TLBs. Instead a process is sealed at execution time and isolated by software verification. This enables stronger security - a process can be identified by its code content even at runtime.
- Contract-based channels: They enable efficient and analyzable communication between SIPs. They are efficient as they provide zero-copy exchange of large amounts of data. Sing# compiler can statically verify their protocol states, hence verifying the contracts established between the receiver and sender.
- Manifest-based programs: A manifest describes the program's static state - its required system resources, desired capabilities and dependencies. Additionally, it is machine-checkable and allows static and deynamic verification of MBP properties, eg. a manifest of a driver ensures install-time verification that it will not access hardware usesd by a previously installed driver.
- Software protection domains: Multiple SIPs can be hosted within a protection domain. The different kinds of SIP to protection-domain mappings matches Singularity to a microkernel, a monolithic kernel or a hybrid kernel design. Thus allowing to suit the requirements.

Flaws:
- SIPs heavily rely on Sing# programming language type and memory safety instead of hardware memory management. However, this restricts Singularity to be a research system only due to its dependence on C# (or Sing#) features such as garbage collection, policy verification, etc.
- Protection is provided by a set of rules (invariants) verified by static analysis. Invariants are checked during the installation of the application statically. And the installation is only carried out by the operating system. This restricts the protection decisions to a static analysis, unlike commodity operating systems which provide hardware-based protection mechanisms such as TLB, page protection, etc.

What it makes harder?
- Generating an exhaustive list of invariants for verification for an application at install time is definitely not possible. An application itself may be self-evolving, eg. its behavior dependent on runtime or input vectors.
- Distributed applications are never thought of in Singularity. Using the concept of bidirectional channels, it may not be possible to support techniques like remote DMA, etc.

What it makes easier?
- Context switches between SIPs have very low overhead as compared to hardware protected processes because TLBs and virtually-addressed caches need not be flushed. This is also shown in Table 1 and compared with commodity OS.
- Zero-copy exchange of large amounts of data through the contract-based channels between SIPs greatly reduce copy overheads.

Summary: Singularity is an experimental project investigating how the software stack (OS + applications) would be redesigned from scratch using today's hardware and software advances. It's main goal is improved reliability/security and it is more than just a microkernel OS: it is an architecture based on provable properties enforced by type safe languages and contracts between components.

Problem: The weak reliability for many of today's large systems can be traced back to design decisions made in a different era (limited hardware and software tools). Such systems are hard to reason about and are composed of parts that can interact in unexpected or unsafe ways. For years, fixing just parts of such systems has failed to solve the reliability problem. Singularity looks at a radical approach: redesign the entire system.

Contributions: The main contribution of Singularity is its emphasis on provable properties. Software isolation of processes is such a property, which offers the ability to run arbitrary SIPs in the same address space as the kernel. Traditional OS techniques alone could not have achieved this and Singularity is new in its reliance on a custom designed programming language, runtime checks and on software verification tools. Components interact with each other using verifiable contracts (contract based channels and manifests).

Organization: Singularity's microkernel provides only the basic, safe sharing of system resources (CPU/scheduling, memory, SIP creation/destruction). Other OS services (file system, etc) are offered by SPIs outside the kernel. A Software Isolated Processe (SIP) is obtained by compiling with a Sing#. All programs must have a manifest which describes the interaction between that program and the environment. Relevant properties can be verified by a verification tool. SIPs don't share memory, they communicate only through contract based channels. Channel endpoints are capabilities which are present at SIP creation time or obtained through channels. These channels are implemented using an Exchange Heap. Zero-allocation communication is ensured by finite queue sizes. SIPs can have threads. Each thread has its own link stack and runtime checks insure that this stack is adjusted as needed. All processes (including the kernel) have garbage collection and can select among several algorithms. Access control is imposed to applications viewed as principals which reflect the identity of the current SIP.

Software isolation allows SIPs to share the address space with the kernel, which decreases the context switch time. Isolation also can facilitate dynamic specialization or direct programming of peripheral devices. Hardware based protection between various security domains is also possible.

Weaknesses: Singularity sometimes on enforcing cumbersome restrictions (such as Linearity for pointers to blocks), in order to be able to prove invariants. It's conceptual simplicity relies on moving part of the complexity to the tools it uses. The verifiers must be small in order to be trusted.
Lack of support for shared memory may be a problem for some applications. The programming style it requires may be challenging.

Singularity: Rethinking the Software Stack

Summary
This paper talks about Singularity Operating system. The hardware and software has evolved with time but the design decisions behind Operating System haven’t. This paper describes the effort made by team of people to re-examine those designs choices in light of new programming languages and verification tools and presents new architectural features.

Problems they are trying to solve
They are trying to target the current shortcomings of all Operating System environments that includes wide spread security vulnerabilities; unexpected interactions among applications; failures caused by errant extensions, plug-ins, and drivers, and a perceived lack of robustness. The current operating system architecture dates back to 1960’s, and there hasn’t been much advancements in the design, though the computers and related hardware has evolved with time. So they are trying to overcome the shortcoming by designing a new architecture using the abilities of these new highly efficient machines.

Contributions
1. The Singularity system is divided in to three key architectural features: Software Isolated Processes, contract-based channels, and manifest-based programs.

2. Software Isolated Processes are just like processes in other OS with different implementation. It is a holder of processing resources and provides context for program execution and associated with it is the set of memory pages containing code and data. SIPs do not share data, and all communication is over a channel called exchange heap. They are separated from other SIPs by software isolation and not by hardware protection. Creation and Destruction of SIPs are inexpensive, as compared to hardware protected resources as in other Operating Systems. Context switches between SIPs is low, as the TLBs and caches don’t need to be flushed.

3. Contract Based Channels are used for all communications between different SIPs. A channel is bidirectional message conduit with exactly two end points. Communication is described by channel contract. Singularity allows zero-copy exchange of data. The rule adopted here is, in each cycle of state transition, there has to be a one send and one receives action.

4. Manifest Based Programs: A manifest describes Manifest Based Programs code resources, its required system resources, its desired capabilities, and its dependencies on other programs. Every component in Singularity is described by a Manifest including kernel, device drivers, and user applications.

5. Sing# Language Compiler provides with static contract verifier that checks what contracts are used in the program and if the code conforms to state machine of the contract. A program can’t run without a Manifest. Programming Language provides static verification and runtime checks.

6. Singularity Kernel: The kernel provides base abstractions of all SIPs, Contract Based channels and manifest based programs. The kernel does a basic job of providing system resources to competing processes and abstracting hardware components.

7. Application Binary Interface (ABI) provides an interface from SIP to kernel.ABI can distinguish between process level operations and high-level operations. ABI constraints an entry of new endpoint to a channel. Static Analysis tool can verify the contract accessibility of code.

8. In Singularity, the kernel and all SIPs reside in a single address space with software isolation. And this address space is logically partitioned in to kernel object space, SIP object space and exchange heap. SIPs cannot access any pointer outside its own SIP address apace and memory owned in exchange heap. Thus each has SIP has its own garbage collector.

9. Manifest Based Configuration by CTR allows programmers to write inspection and generate code. This allows them to statically verify it’s well formed and type safe.

Flaws:
The paper doesn’t say about its ease of use. The Operating System success hugely depends upon the ease of use or how user interfaces with it. The Implementation isn’t enough to have good idea, how it works.
What’s the guarantee that static checking does everything required correctly?

What it makes easier
1. The safe programming language used makes system highly secure. The programmer doesn’t have to worry about buffer overflows and null pointers.
2. Singularity makes system highly resilient. The concept of SIPs, totally isolated processes from each other, thus they don’t depend on each other and prevents system crashes.
3. The sound verification tools detect programmer error early in development cycle. The contract verifier tool appears to be very efficient in the long run. The errors that could easily be missed by user are easily caught by the contract verifier.
4. The SIPs and kernel are software separated but they can occupy same hardware space. They incur low overhead cost while communication and SIPs are inexpensive to create and destroy as compared to hardware protected processes. Context switch is low, as context switch between them doesn’t require flushing TLB or cache.
5. This system would have no unexpected interaction amongst processes as the scope has been left to NIL. All the SIPs have different logical address space and they have no way to accessing other SIPs object. The concept of shared written space is eradicated which simplifies system a lot.
6. Singularity offers dynamic specialization of processors making the perfect use of multi core functionality.
7. SIP allows greater flexibility of placing privilege instructions. Because of available type and memory safety functions, singularity can place privilege instructions inside trusted function of SIP. This flexibility is not at all possible in current OS designs as they might screw the resource.

What it makes tougher
1. Singularity dint consider the application and driver compatibility while exploring new design options. This requires rewriting or to port every line of code again.
2. All the communication can occur only on exchange heap. There might arise a situation where this could act as a bottleneck especially zero allocation mechanism.

Summary:
The authors of this paper present, Singularity, an operating system built in the type safe language, Sing#. The design of the OS is based on three key architectural components, which addresses the shortcomings of previous operating systems by emphasizing system dependability and trustworthiness of processes.
Problem to Solve: The authors are trying to solve several problems that occur in operating systems today because of the changing nature of how operating systems are used now compared to the 1960s and 1970s when many of these systems were originally developed. Namely, some of the items they would like to address are increasing security and robustness while preventing applications from unexpectedly interacting and checking the correctness of applications before use.
Contributions: The authors had several main contributions in this paper:

The development of a new language Sing# based on C#.
The idea of using software-isolated processes (SIP) to help isolate programs from each other in a way that still allowed for message passing, memory safety and memory management.
A communication channel that allows for general information to be passed between nodes on an isolated channel.
The creation of Manifest-Based programs (MBP) allows for the system to know all of a programs needed resources and privileges before execution.
Flaws: One flaw of this paper is that it never truly discusses machine dependence/independence. Cost in CPU cycles is presented table 2 and later I/O device compatibility in SIPs is discussed, but this information doesn’t clarify for the user that this OS is highly machine independent. Another flaw in the paper is that it states that application compatibility was given up for the sake of design, but what types of software fall under applications is not clearly defined. Users would probably accept the loss of common application if there was another application that could take its place (e.g. Word vs. OpenOffice), but if none of the applications a user is fond of today could be used that is a more serious downfall.
Advantages of Proposed OS: One major advantage of this system is its communication channel. Like capabilities, the passing of pointers to data in the exchange heap allows other processes the ability to access and take control over data in memory. Another advantage is that the “unsafe code tax” is only imposed on unsafe programs leading to lower overhead in the system overall compared to other systems with code taxes. Protection domains provide an additional level of protection for programs from each other through static analysis which helps increase system robustness.
Disadvantages: One disadvantage of this system is lack of support for existing applications. Another disadvantage with the system is its dependence on MSIL. Changes to the MSIL language would then need to be reflected in the Singularity system code.

Summary
The Singularity project is experimental operating system that considers the use of a high level programming language, while adding the features of static verification tools. Singularity brings the power of a high level language and static verification tools into the operating system to reduce the hardware protection burden on the kernel.

Problem
Contemporary operating systems are burdened with the backwards compatibility, tools and designs from the 1960’s and 1970’s. The evolution of operating systems has been very gradual in time even though the processing capabilities of operating systems have grown.

Contributions
This paper contributes the idea of combining static verification tools and high level syntax checking into the operating system and applications. Static verification tools are very helpful in detecting flaws and security issues during development rather than at real time and combining these features into OS development is a good direction to examine for possibilities.
The Singularity also brings about the idea of total process memory isolation. No memory is shared between processes except for the heap memory for message passing which simplifies the kernel model.

Flaws
The Singularity design is targeting a very high level design. The security has been pushed to the programming language and static analysis tools, however the high level programming language and static analysis tools can be very complex and can lead to many security issues once discovered. Although static verification tools can improve the protection and run time behavior, it cannot perform all the tasks of dynamic run-time checking. Along with this, static checking takes high level of tuning to analyze programs behavior.

Proposed Organization
The Singularity project is organized with a microkernel at the base with 90% of the software written in Sing#, and all devices, systems and protocols implemented in SIPS. SIPS are software isolated processes that can only communicate with other SIPS through the kernel message passing objects. Individual garbage collection tools clean up memory. Applications are manifest-based programs that have or contain capabilities of which the program will need access to. The Sing# syntax and type checking and static verification tools ensure applications operate properly and reduce protection requirements.
Singularity makes it easier to write applications and debug flaws or security vulnerabilities early in development; however, singularity makes it difficult to get strong performance through the operating system because of the message passing limitations and high level confinements of the Singularity system.

Introduction:
This paper describes the philosophy and design of the Singularity Operating System, an experimental OS built from the ground up at Microsoft Research.

What were they trying to solve:
Most "real" operating systems running today have their designs based on architectural principles set in the 1970s. Many of the design decisions made in those days are not suitable in modern day systems, since both hardware and software has evolved a lot since then. This has lead to modern systems being bulky, redundant, inefficient and unreliable. The authors also feel that operating systems are not making use of modern software verification methods.

Contributions:
The central theme of this paper is Static Verification. The idea is, if you have a set of tools which verify the software before it runs, you can make the runtime environment much simpler, and guarantee that the software works without major problems.
All processes and the kernel share the same address space. This is more efficient that hardware-protected multiple virtual address spaces since it prevents unnecessary cache misses etc.
Communication between processes are highly structured. There is no direct sharing of data between processes. Communication has be through the kernel or via Channels. This makes accidental contamination of external resources unlikely.
Per Process Garbage collection: Each process can implement a different garbage collection policy as per it's requirements.
Contract-based Channels: Explicit, verifiable information of the communication protocol needs to be explicitly specified at compile time. This allows static checks to be made to ensure that the process doesn't bring down the system(eg: If a process does a SEND, it has to RECEIVE before it can SEND again, which prevents unbounded message creation.)
Manifest based programs: The manifest of a program is a complete description of the process in terms of what channels it creates, whether it had unsafe code etc. The binary code is loaded into memory only when the manifest satisfies all the constraints. This prevents malicious code to be injected into the system.
Versioned ABI is an elegant and controlled approach to binary compatibility. This is important since modern systems need to change rapidly, without endangering existing applications.
The Two-List scheduling mechanism is a fast and efficient way to schedule processes. It specifically is good for processes which wake up just to handle and then go back to sleep, which is what a lot of daemon processes do.

Flaws:
Not having a separate address space per process decreases the address range each process can play with. This is especially true of 32-bit systems where the address space is not too large.
The assumption here is that the set of static verification tools is complete in preventing any potentially malicious code from executing. This is difficult to guarantee in practice. And once this security is breached, the access over the system is complete.
The compile time reflection mechanism is not powerful enough to replace true dynamic reflection. If a program verifier is built into the kernel, then the program verification can be done dynamically as well.
In practice, writing comprehensive contracts for complex processes would be very hard.

OS Organization:
The system consists of the kernel and multiple independent Software Isolated Processes. SIP's communicate via Channels, and share data through an exchange heap managed by the kernel. All processes share the same address space. All code that executes is statically verified for correctness.
Advantages:
Process creation, context switching, message passing is very fast.
Provable guarantees can be given for proper working of the code. The system is (in theory) highly reliable.
Disadvantages:
Porting existing applications to this is very hard since the model is so different.
Rigid framework for building programs. Would probably be complex to code and change the program since most of the checks are static.

Summary
In “Singularity: Rethinking the Software Stack”, Hunt and Larus describe the operating system Singularity—an OS designed for research purposes which sports safe programming languages, use of verification, and improved system architecture to provide correct system behavior.

Problem
Singularity as a whole is designed as a system upon which new ideas can be evaluated. It provides a variety of facilities for building a safe system which earlier operating systems did not have due to the fact that they were developed when speed and memory were far more limited. This lack of safe systems has brought about a variety of issues in today’s systems that stem from corruption of resources because programs access and modify information which they should not.

Contributions
• Isolating processes at a software level—this prevents the need for costly hardware level isolation and thus improves the system’s efficiency. This promotion of a trust-based system requires full checking of any software which is to be run upon the system, but once checking is complete and the program becomes trusted, additional protection is not necessary.
• Contract-based channels provide an efficient and reliable method of inter process communication. This abstraction requires all processes to cooperate in communication and provides a uniform method of communication.
• Allowing processes to be tied to a particular processor/core. By so doing, cache effects (if each core has an independent cache) can be better taken advantage of. This yields itself well to possible future specialization of cores and also to making use of current specialization of various processing devices (CPU and GPU).

Flaws
• The system addresses safety well with SIPs, but does little in terms of preventing maliciousness. For example, code could be altered after checking and then could gain access to the entire memory space in which everything else (including the microkernel) resides.
• Applying the techniques described in this paper would require porting or replacing any existing software which was needed on this system. With the wealth of software in existence, this would be a major undertaking.

Organization
Singularity consists of code in SIPs which (barring maliciousness) are fully isolated from each other. The software isolated processes communicate with each other through contract-based channels, with large transfers of information done with an exchange heap, which allows for cheap data transfer by transferring a reference to data in a location accessible to multiple processes. Processes are started via manifests, which detail the processes’ resources and define everything upon which the process depends. The manifest is used by the system to prepare everything the process will use and to start it.

Singularity is a research project on new design ideas in operating systems. Hunt and Larus attribute lots of the design decisions in existing systems in the computing environment of the 1970s. Singularity tries to shed light on new design ideas for creating modern reliable operating systems.

Singularity primarily attacks the reliability problem in modern operating systems. The widespread adoption of some operating systems has resulted in a pressing need for flexibility. The operating system architects have responded with modular designs, where everyone can insert extensions into the kernel to support some specific need (eg. a new device). The authors argue that the design principles of operating systems today cannot keep up in a modern environment. This leads to security vulnerabilities and system failures, which in turn degrade the overall reliability.

The memory protection mechanism of the paper is interesting as it relies on memory independence: all pointers are either to SIP-local data or the exchange heap, a special place for storing shared data. In the exchange heap, SIPs can put data and then transfer ownership of the data to the destination SIP. This effectively insures that each SIP is isolated from the effects of the other SIPs running on the system. This way context switches become a lot cheaper as no protection mode transitions are required. Finally, there is a very nice integration of operating system functions and model-based checking and verification.

It is not clear if the stated problems affect all operating systems: implicitly the authors refer to Windows being the one and only operating system. Of course, Windows has driven the concept of extensibility to a completely new level, so it could be argued that they just hit the problem first. Also, the option of requiring a high-level language reminds me of Pilot, as both systems could implement some nice features because of the type safety. The question that is still not answered is how reasonable this would be for a system that is not destined to be a research vehicle but a stable production operating system, in 2007: How would applications in C be ported on an operating system that relies upon type safety and memory safety? (The authors argue about introducing protection domains, but they seem to defeat the purpose of providing this new memory protection mechanism in the first place.) Finally, I have serious doubts if an operating system kernel should require garbage collection on itself to function efficiently.

The strong separation makes it easier to build the system as a set of interconnected SIPs. The disadvantage is that you have to copy all data into the exchange heap before passing it to someone else, aka. this means two copies of the whole data instead of a copy of a memory pointer. Moreover, this design decision means that some basic hardware techniques (like DMA) are not so simple to use in the new architecture and even if they are used, they will not work nearly as fast.