Systems programs rely on fine-grain control of data representa-tion and use of state to achieve performance, conformance to hard-ware specification, and temporal predictability. The robustness and checkability of these programs could be greatly improved if mod-ern type systems and programming language ideas, such as poly-morphism and type inference, could be applied to these programs. BitC is a higher-order programming language in the tradition of ML and Haskell, extended to incorporate both state and the expres-sion of unboxed and low-level datatypes. State and unboxed value types interact in subtle ways with polymorphic type-inference. Un-less handled with care in the language design, interactions of these features can lead to unsoundness or results that are counter-intuitive to the programmer. Because instances of value types may have mu-table components, a decision must be made concerning their com-patibility at copy boundaries: should structurally equivalent types that differ only in their mutability be considered compatible. The choice impacts both the amount of polymorphism that the language can preserve and the burden of type annotation imposed on the pro-grammer. This paper presents some of these challenges and our design for how to address these issues.

A key missing link in the creation of secure and robust systems is finding a ost effective way to demonstrate and preserve correspondence between a software design and its implementation. This paper explores the use of software model checking techniques to validate selected design invariants in the EROS operating system kernel. Several global consistency policies in the EROS kernel can be expressed as finite state automata. Using the MOPS static hecker, we have been able to validate the EROS kernel implementation against these automata. In the process, we have confirmed the practical utility of the basic verification technique, identified a number of desirable enhancements in MOPS, and located bugs in the EROS implementation.A key contribution of this paper is establishing that it is practical to integrate software model checking into normal development lifestyle. Model hecking is efficient enough that it does not add noticeably to our build times. This allows us to view it as a tool for error prevention rather than detection. Our work with EROS and MOPS suggests that domain specific application of software model hecking is a practical and powerful technique for software assurance and maintenance.

Recent advances in interprocess communication (IPC) performance have been exclusively based on thread-migrating IPC designs. Thread-migrating designs assume that IPC interactions are synchronous, and that user-level execution will usually resume with the invoked process (modulo preemption). This IPC design approach offers shorter instruction path lengths, requires fewer locks, has smaller instruction and data cache footprints, dramatically reduces TLB overheads, and consequently offers higher performance and lower timing variance than previous IPC designs. With care, it can be performed as an atomic unit of operation. While the performance of thread-migrating IPC has been examined in detail, the vulnerabilities implicit in synchronous IPC designs have not been examined in depth in the archival literature, and their implications for IPC design have been actively misunderstood in at least one recent publication. In addition to performance, a sound IPC design must address concerns of asymmetric trust and reproducibility and provide support for dynamic payload lengths. Previous IPC designs, including those of EROS, Mach, L4, Flask, and Pebble, satisfy only two of these three requirements. In this paper, we show how these three design objectives can be met simultaneously. We identify the conflict of requirements and illustrate how their collision arises in two well-documented IPC architectures: L4 and EROS. We then show how all three design objectives are simultaneously met in the next generation EROS IPC system.

Capability systems can be used to implement higher-level security policies including the *-property if a mechanism exists to ensure confinement. The implementation can be efficient if the "weak" access restriction described in this paper is introduced. In the course of developing EROS, a pure capability system, it became clear that verifying the correctness of the confinement mechanism was necessary in establishing the security of the operating system. We present a verification of the EROS confinement mechanism with respect to a broad class of capability architectures (including EROS). We give a formal statement of the requirements, construct a model of the architecture's security policy and operational semantics, and show that architectures covered by this model enforce the confinement requirements if a small number of initial static checks on the confined subsystem are satisfied. The method used generalizes to any capability system.

EROS is a capability-based operating system for commodity processors which uses a single level storage model. The single level store's persistence is transparent to applications. The performance consequences of support for transparent persistence and capability-based architectures are generally believed to be negative. Surprisingly, the basic operations of EROS (such as IPC) are generally comparable in cost to similar operations in conventional systems. This is demonstrated with a set of microbenchmark measurements of semantically similar operations in Linux.The EROS system achieves its performance by coupling well-chosen abstract objects with caching techniques for those objects. The objects (processes, nodes, and pages) are well-supported by conventional hardware, reducing the overhead of capabilities. Software-managed caching techniques for these objects reduce the cost of persistence. The resulting performance suggests that composing protected subsystems may be less costly than commonly believed.