Extremely Reliable Operating System
Encyclopedia
EROS is an operating system
developed by The EROS Group, LLC., the Johns Hopkins University
, and the University of Pennsylvania
. Features include automatic data and process persistence, some preliminary real-time
support, and capability-based security
. EROS is purely a research operating system, and was never deployed in real world use. , development has stopped in favor of two successor systems, CapROS
and Coyotos
.
(IPC). By enforcing capability-protected interfaces, the kernel ensures that all communications to a process arrive via an intentionally exported interface. It also ensures that no invocation is possible unless the invoking component holds a valid capability to the invokee. Protection in capability systems is achieved by restricting the propagation of capabilities from one component to another, often through a security policy known as confinement.
Capability systems naturally promote component-based software structure. This organizational approach is similar to the programming language concept of object-oriented programming
, but occurs at larger granularity and does not include the concept of inheritance
. When software is restructured in this way, several benefits emerge:
Collectively, these benefits lead to measurably more robust and secure systems. The SDS Sigma 7
was a hardware-based capability system originally designed for use in telephony switches. A capability-based design was chosen specifically for reasons of robustness.
In contrast to many earlier systems, capabilities are the only mechanism for naming and using resources in EROS. Such a system is sometimes referred to as a pure capability system. The IBM AS/400 is an example of a commercially successful capability system, but it is not a pure capability system.
Pure capability architectures are supported by well-tested and mature mathematical security models. These have been used to formally demonstrate that capability-based systems can be made secure if implemented correctly. The so-called "safety property" has been shown to be decidable for pure capability systems (see Lipton). Confinement, which is the fundamental building block of isolation, has been formally verified to be enforceable by pure capability systems, and is reduced to practical implementation by the EROS "constructor" and the KeyKOS "factory". No comparable verification exists for any other primitive protection mechanism. There is a fundamental result in the literature showing that "safety" is mathematically undecidable in the general case (see HRU
, but note that it is of course provable for an unbounded set of restricted cases). Of greater practical importance, safety has been shown to be false for all of the primitive protection mechanisms shipping in current commodity operating systems (see HRU
). Safety is a necessary precondition to successful enforcement of any security policy. In practical terms, this result means that it is not possible in principle to secure current commodity systems, but it is potentially possible to secure capability-based systems provided they are implemented with sufficient care. Neither system has ever been successfully penetrated, and their isolation mechanisms have never been successfully defeated by any inside attacker, but it is not known whether the EROS or KeyKOS implementations was careful enough. One goal of the Coyotos
project is to demonstrate that component isolation and security has been definitively achieved by apply software verification techniques.
The L4.sec system, which is a successor to the L4 microkernel family
, is a capability-based system, and has been significantly influenced by the results of the EROS project. The influence is mutual, since the EROS work on high-performance invocation was motivated strongly by Jochen Liedtke
's successes with the L4 microkernel family
.
, which is an "evolutionary step" beyond the EROS operating system.
The EROS project started in 1991 as a clean-room reconstruction of an earlier system, KeyKOS
. KeyKOS was an operating system developed by Key Logic, Inc., and was a direct continuation of work on the earlier GNOSIS
(Great New Operating System In the Sky) system created by Tymshare, Inc. The KeyKOS system offered a degree of security and reliability that remains unduplicated today (2006). The circumstances surrounding Key Logic's unfortunate demise in 1991 made licensing KeyKOS impractical. Since KeyKOS did not run on popular commodity processors in any case, the decision was made to reconstruct it from the publicly available documentation.
By late 1992, it had become clear that processor architecture had changed significantly since the introduction of the capability idea, and it was no longer obvious that component-structured systems were practical. Microkernel
-based systems, which similarly favor large numbers of processes and IPC, were facing severe performance challenges, and it was uncertain if these could be successfully resolved. The x86 architecture
was clearly emerging as the dominant architecture but the expensive user/supervisor transition latency on the 386
and 486
presented serious challenges for process-based isolation. The EROS project was turning into a research effort, and moved to the University of Pennsylvania
to become the focus of Shapiro's dissertation research. By 1999, a high performance implementation for the Pentium processor had been demonstrated that was directly performance competitive with the L4 microkernel family
, which is known for its exceptional speed in IPC. The EROS confinement mechanism had been formally verified, in the process creating a general formal model for secure capability systems.
In 2000, Shapiro joined the faculty of Computer Science at Johns Hopkins University. At Hopkins, the goal was to show how to use the facilities provided by the EROS kernel to construct secure and defensible servers at application level. Funded by the Defense Advanced Research Projects Agency
and the Air Force Research Laboratory
, EROS was used as the basis for a trusted window system, a high-performance, defensible network stack, and the beginnings of a secure web browser. It was also used to explore the effectiveness of lightweight static checking. In 2003, some very challenging security issues were discovered that are intrinsic to any system architecture based on synchronous IPC primitives (notably including EROS and L4). Work on EROS halted in favor of Coyotos, which resolves these issues.
, EROS and its successors are the only widely available capability systems that run on commodity hardware.
system is building directly from the EROS code base, while the Coyotos
system is a successor system that addresses some of the architectural deficiencies of EROS, and is exploring (as research) the possibility of a fully verified operating system. Both CapROS and Coyotos are expected to be released in various commercial deployments.
Operating system
An operating system is a set of programs that manage computer hardware resources and provide common services for application software. The operating system is the most important type of system software in a computer system...
developed by The EROS Group, LLC., the Johns Hopkins University
Johns Hopkins University
The Johns Hopkins University, commonly referred to as Johns Hopkins, JHU, or simply Hopkins, is a private research university based in Baltimore, Maryland, United States...
, and the University of Pennsylvania
University of Pennsylvania
The University of Pennsylvania is a private, Ivy League university located in Philadelphia, Pennsylvania, United States. Penn is the fourth-oldest institution of higher education in the United States,Penn is the fourth-oldest using the founding dates claimed by each institution...
. Features include automatic data and process persistence, some preliminary real-time
Real-time operating system
A real-time operating system is an operating system intended to serve real-time application requests.A key characteristic of a RTOS is the level of its consistency concerning the amount of time it takes to accept and complete an application's task; the variability is jitter...
support, and capability-based security
Capability-based security
Capability-based security is a concept in the design of secure computing systems, one of the existing security models. A capability is a communicable, unforgeable token of authority. It refers to a value that references an object along with an associated set of access rights...
. EROS is purely a research operating system, and was never deployed in real world use. , development has stopped in favor of two successor systems, CapROS
CapROS
CapROS is an open source operating system. It is a pure capability-based system that features automatic persistence of data and processes, even across system reboots. Capability systems naturally support the principle of least authority, which improves security and fault tolerance.CapROS is an...
and Coyotos
Coyotos
Coyotos is a capability-based security-focused microkernel operating system developed by The EROS Group, LLC. It is a successor to the EROS system that was created at the University of Pennsylvania and Johns Hopkins University.- History :...
.
Key concepts
The overriding goal of the EROS system (and its relatives) is to provide strong support at the operating system level for the efficient restructuring of critical applications into small communicating components. Each component can communicate with the others only through protected interfaces, and is isolated from the rest of the system. A "protected interface", in this context, is one that is enforced by the lowest level part of the operating system (the kernel). The kernel is the only portion of the system that can move information from one process to another. It also has complete control of the machine and (if properly constructed) cannot be bypassed. In EROS, the kernel-provided mechanism by which one component names and invokes the services of another is capabilities using inter-process communicationInter-process communication
In computing, Inter-process communication is a set of methods for the exchange of data among multiple threads in one or more processes. Processes may be running on one or more computers connected by a network. IPC methods are divided into methods for message passing, synchronization, shared...
(IPC). By enforcing capability-protected interfaces, the kernel ensures that all communications to a process arrive via an intentionally exported interface. It also ensures that no invocation is possible unless the invoking component holds a valid capability to the invokee. Protection in capability systems is achieved by restricting the propagation of capabilities from one component to another, often through a security policy known as confinement.
Capability systems naturally promote component-based software structure. This organizational approach is similar to the programming language concept of object-oriented programming
Object-oriented programming
Object-oriented programming is a programming paradigm using "objects" – data structures consisting of data fields and methods together with their interactions – to design applications and computer programs. Programming techniques may include features such as data abstraction,...
, but occurs at larger granularity and does not include the concept of inheritance
Inheritance (computer science)
In object-oriented programming , inheritance is a way to reuse code of existing objects, establish a subtype from an existing object, or both, depending upon programming language support...
. When software is restructured in this way, several benefits emerge:
- The individual components are most naturally structured as event loopsEvent-driven programmingIn computer programming, event-driven programming or event-based programming is a programming paradigm in which the flow of the program is determined by events—i.e., sensor outputs or user actions or messages from other programs or threads.Event-driven programming can also be defined as an...
. Examples of systems that are commonly structured this way include flight control systems (see also DO-178B Software Considerations in Airborne Systems and Equipment CertificationDO-178BDO-178B, Software Considerations in Airborne Systems and Equipment Certification is a document dealing with the safety of software used in airborne systems....
), and telephone switching systems (see 5ESS switch5ESS SwitchThe 5ESS Switch is a Class 5 telephone electronic switching system sold by Alcatel-Lucent. This digital central office telephone circuit switching system is used by many telecommunications service providers.-History:...
). Event-driven programming is chosen for these systems primarily because of simplicity and robustness, which are essential attributes in life-critical and mission-critical systems. - Components become smaller and individually testable, which helps the implementor to more readily identify flaws and bugs.
- The isolation of each component from the others limits the scope of the damage that may occur when something goes wrong or the software misbehaves.
Collectively, these benefits lead to measurably more robust and secure systems. The SDS Sigma 7
Scientific Data Systems
Scientific Data Systems, or SDS, was an American computer company founded in September 1961 by Max Palevsky, a veteran of Packard Bell and Bendix, along with eleven other computer scientists. SDS was an early adopter of integrated circuits in computer design and the first to employ silicon...
was a hardware-based capability system originally designed for use in telephony switches. A capability-based design was chosen specifically for reasons of robustness.
In contrast to many earlier systems, capabilities are the only mechanism for naming and using resources in EROS. Such a system is sometimes referred to as a pure capability system. The IBM AS/400 is an example of a commercially successful capability system, but it is not a pure capability system.
Pure capability architectures are supported by well-tested and mature mathematical security models. These have been used to formally demonstrate that capability-based systems can be made secure if implemented correctly. The so-called "safety property" has been shown to be decidable for pure capability systems (see Lipton). Confinement, which is the fundamental building block of isolation, has been formally verified to be enforceable by pure capability systems, and is reduced to practical implementation by the EROS "constructor" and the KeyKOS "factory". No comparable verification exists for any other primitive protection mechanism. There is a fundamental result in the literature showing that "safety" is mathematically undecidable in the general case (see HRU
HRU (security)
The HRU security model is an operating system level computer security model which deals with the integrity of access rights in the system. It is an extension of the Graham-Denning model, based around the idea of a finite set of procedures being available to edit the access rights of a subject s on...
, but note that it is of course provable for an unbounded set of restricted cases). Of greater practical importance, safety has been shown to be false for all of the primitive protection mechanisms shipping in current commodity operating systems (see HRU
HRU (security)
The HRU security model is an operating system level computer security model which deals with the integrity of access rights in the system. It is an extension of the Graham-Denning model, based around the idea of a finite set of procedures being available to edit the access rights of a subject s on...
). Safety is a necessary precondition to successful enforcement of any security policy. In practical terms, this result means that it is not possible in principle to secure current commodity systems, but it is potentially possible to secure capability-based systems provided they are implemented with sufficient care. Neither system has ever been successfully penetrated, and their isolation mechanisms have never been successfully defeated by any inside attacker, but it is not known whether the EROS or KeyKOS implementations was careful enough. One goal of the Coyotos
Coyotos
Coyotos is a capability-based security-focused microkernel operating system developed by The EROS Group, LLC. It is a successor to the EROS system that was created at the University of Pennsylvania and Johns Hopkins University.- History :...
project is to demonstrate that component isolation and security has been definitively achieved by apply software verification techniques.
The L4.sec system, which is a successor to the L4 microkernel family
L4 microkernel family
L4 is a family of second-generation microkernels, generally used to implement Unix-like operating systems, but also used in a variety of other systems.L4 was a response to the poor performance of earlier microkernel-base operating systems...
, is a capability-based system, and has been significantly influenced by the results of the EROS project. The influence is mutual, since the EROS work on high-performance invocation was motivated strongly by Jochen Liedtke
Jochen Liedtke
Jochen Liedtke was a German computer scientist, noted for his work on microkernels, especially the creation of the L4 microkernel family....
's successes with the L4 microkernel family
L4 microkernel family
L4 is a family of second-generation microkernels, generally used to implement Unix-like operating systems, but also used in a variety of other systems.L4 was a response to the poor performance of earlier microkernel-base operating systems...
.
History
The primary developer of EROS was Jonathan S. Shapiro. He is also the driving force behind CoyotosCoyotos
Coyotos is a capability-based security-focused microkernel operating system developed by The EROS Group, LLC. It is a successor to the EROS system that was created at the University of Pennsylvania and Johns Hopkins University.- History :...
, which is an "evolutionary step" beyond the EROS operating system.
The EROS project started in 1991 as a clean-room reconstruction of an earlier system, KeyKOS
KeyKOS
KeyKOS is a persistent, pure capability-based operating system for the IBM S/370 mainframe computers. It allows emulating the VM, MVS, and POSIX environments. It is a predecessor of the Extremely Reliable Operating System , and its successors, the CapROS and Coyotos operating systems...
. KeyKOS was an operating system developed by Key Logic, Inc., and was a direct continuation of work on the earlier GNOSIS
GNOSIS
GNOSIS is a capability-based operating system that was researched during the 1970s in Tymshare, Inc. It was based on the research of Norman Hardy, Dale E. Jordan, Bill Frantz, Charlie Landau, Jay Jonekait, et al. It provided a foundation for the development of future operating systems such as...
(Great New Operating System In the Sky) system created by Tymshare, Inc. The KeyKOS system offered a degree of security and reliability that remains unduplicated today (2006). The circumstances surrounding Key Logic's unfortunate demise in 1991 made licensing KeyKOS impractical. Since KeyKOS did not run on popular commodity processors in any case, the decision was made to reconstruct it from the publicly available documentation.
By late 1992, it had become clear that processor architecture had changed significantly since the introduction of the capability idea, and it was no longer obvious that component-structured systems were practical. Microkernel
Microkernel
In computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system . These mechanisms include low-level address space management, thread management, and inter-process communication...
-based systems, which similarly favor large numbers of processes and IPC, were facing severe performance challenges, and it was uncertain if these could be successfully resolved. The x86 architecture
X86 architecture
The term x86 refers to a family of instruction set architectures based on the Intel 8086 CPU. The 8086 was launched in 1978 as a fully 16-bit extension of Intel's 8-bit based 8080 microprocessor and also introduced segmentation to overcome the 16-bit addressing barrier of such designs...
was clearly emerging as the dominant architecture but the expensive user/supervisor transition latency on the 386
386
Year 386 was a common year starting on Thursday of the Julian calendar. At the time, it was known as the Year of the Consulship of Honorius and Euodius...
and 486
486
Year 486 was a common year starting on Wednesday of the Julian calendar. At the time, it was known as the Year of the Consulship of Basilius and Longinus...
presented serious challenges for process-based isolation. The EROS project was turning into a research effort, and moved to the University of Pennsylvania
University of Pennsylvania
The University of Pennsylvania is a private, Ivy League university located in Philadelphia, Pennsylvania, United States. Penn is the fourth-oldest institution of higher education in the United States,Penn is the fourth-oldest using the founding dates claimed by each institution...
to become the focus of Shapiro's dissertation research. By 1999, a high performance implementation for the Pentium processor had been demonstrated that was directly performance competitive with the L4 microkernel family
L4 microkernel family
L4 is a family of second-generation microkernels, generally used to implement Unix-like operating systems, but also used in a variety of other systems.L4 was a response to the poor performance of earlier microkernel-base operating systems...
, which is known for its exceptional speed in IPC. The EROS confinement mechanism had been formally verified, in the process creating a general formal model for secure capability systems.
In 2000, Shapiro joined the faculty of Computer Science at Johns Hopkins University. At Hopkins, the goal was to show how to use the facilities provided by the EROS kernel to construct secure and defensible servers at application level. Funded by the Defense Advanced Research Projects Agency
Defense Advanced Research Projects Agency
The Defense Advanced Research Projects Agency is an agency of the United States Department of Defense responsible for the development of new technology for use by the military...
and the Air Force Research Laboratory
Air Force Research Laboratory
The Air Force Research Laboratory is a scientific research organization operated by the United States Air Force Materiel Command dedicated to leading the discovery, development, and integration of affordable aerospace warfighting technologies; planning and executing the Air Force science and...
, EROS was used as the basis for a trusted window system, a high-performance, defensible network stack, and the beginnings of a secure web browser. It was also used to explore the effectiveness of lightweight static checking. In 2003, some very challenging security issues were discovered that are intrinsic to any system architecture based on synchronous IPC primitives (notably including EROS and L4). Work on EROS halted in favor of Coyotos, which resolves these issues.
, EROS and its successors are the only widely available capability systems that run on commodity hardware.
Status
Work on EROS by the original group has halted, but there are two successor systems. The CapROSCapROS
CapROS is an open source operating system. It is a pure capability-based system that features automatic persistence of data and processes, even across system reboots. Capability systems naturally support the principle of least authority, which improves security and fault tolerance.CapROS is an...
system is building directly from the EROS code base, while the Coyotos
Coyotos
Coyotos is a capability-based security-focused microkernel operating system developed by The EROS Group, LLC. It is a successor to the EROS system that was created at the University of Pennsylvania and Johns Hopkins University.- History :...
system is a successor system that addresses some of the architectural deficiencies of EROS, and is exploring (as research) the possibility of a fully verified operating system. Both CapROS and Coyotos are expected to be released in various commercial deployments.
Journals
- R. J. Lipton and L. Snyder. "A Linear Time Algorithm for Deciding Subject Security." Journal of the ACM, 24(3):455—464, 1977.
- M. A. Harrison, W. L. Ruzzo and J. D. Ullman. "Protection in Operating Systems". Communications of ACM. 19(8):461—471, August 1976.