Operating System Verification — An Overview
---
paper_title: Report on a conference sponsored by the NATO Science Committee

paper_content:

A fluid energy mill having an inlet chamber, a classification chamber, and an upstack and downstack connecting opposite ends of the inlet chamber to the classification chamber. The inlet chamber, which is positioned angularly to the upstack and downstack, has a Venturi portion between the upstack and downstack. A feed inlet is also positioned angularly to the upstack as well as to the inlet chamber. This feed inlet also has a Venturi portion. A feed hopper is provided above the feed inlet and is in connection therewith. A pressure fluid nozzle is provided below the hopper to project the fluid and particles from the hopper through the Venturi in the feed inlet. A similar but opposed nozzle is provided below the downstack to project fluid through the Venturi in the inlet chamber toward the upstack. The fluid and particles propelled by each nozzle meet and impact below the upstack and the resultant fluid and particles pass upwardly through the upstack and centrifugally move through the mill where the lighter particles are centrifugally separated from the heavier particles and exhausted from the mill.
---
paper_title: Mechanizing Proof: Computing, Risk, and Trust

paper_content:

Most aspects of our private and social lives---our safety, the integrity of the financial system, the functioning of utilities and other services, and national security---now depend on computing. But how can we know that this computing is trustworthy? In Mechanizing Proof, Donald MacKenzie addresses this key issue by investigating the interrelations of computing, risk, and mathematical proof over the last half century from the perspectives of history and sociology. His discussion draws on the technical literature of computer science and artificial intelligence and on extensive interviews with scientists and engineers.
---
paper_title: Program verification: the very idea

paper_content:

The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.
---
paper_title: Ten commandments revisited: a ten-year perspective on the industrial application of formal methods

paper_content:

Ten years ago, our 1995 paper Ten Commandments of Formal Methods [5] suggested some guidelines to help ensure the success of a formal methods project. It proposed ten important requirements (or "commandments") for formal developers to consider and follow, based on our knowledge of several industrial application success stories, most of which have been reported in more detail in two books [17],[18]. The paper was surprisingly popular, is still widely referenced, and used as required reading in a number of formal methods courses. However, not all have agreed with some of our commandments, feeling that they may not be valid in the long-term. We re-examine the original commandments ten years on, and consider their validity in the light of a further decade of industrial best practice and experiences.
---
paper_title: The B-Book: Assigning Programs to Meanings

paper_content:

Tribute Foreword Introduction Part I. Mathematics: 1. Mathematical reasoning 2. Set notation 3. Mathematical objects Part II. Abstract Machines: 4. Introduction to abstract machines 5. Formal definition of abstract machines 6. Theory of abstract machines 7. Constructing large abstract machines 8. Examples of abstract machines Part III. Programming: 9. Sequencing and loop 10. Programming examples Part IV. Refinement: 11. Refinement 12. Constructing large software systems 13. Examples of refinement Appendixes Index.
---
paper_title: Towards Self-verification of HOL Light

paper_content:

The HOL Light prover is based on a logical kernel consisting of about 400 lines of mostly functional Ocaml. whose complete formal verification seems to be quite feasible. We would like to formally verify (i) that the abstract HOL logic is indeed correct, and (ii) that the OCaml code does correctly implement this logic. We have performed a full verification of an imperfect but quite detailed model of the basic HOL Light core, without definitional mechanisms, and this verification is entirely conducted with respect to a set-theoretic semantics within HOL Light itself. We will duly explain why the obvious logical and pragmatic difficulties do not vitiate this approach, even though it looks impossible or useless at first sight. Extension to include definitional mechanisms seems straightforward enough, and the results so far allay most of our practical worries.
---
paper_title: Computer-Aided Reasoning: An Approach

paper_content:

From the Publisher: ::: An Approach ::: Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, or theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on artificial intelligence or automated reasoning and as a reference for business and industry. ::: Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction. ::: In this book we present: ::: ::: A practical functional programming language closely related to Common Lisp which is used to define functions (which can model computing systems) and to make assertions about defined functions; A formal logic in which defined functions correspond to axioms; the logic is first-order, includes induction, and allows us to prove theorems about the functions; The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process. ::: ::: The ACL2 system hasbeen successfully applied to projects of commercial interest, including microprocessor, modeling, hardware verification, microcode verification, and software verification. This book gives a methodology for modeling computing systems formally and for reasoning about those models with mechanized assistance. The practicality of computer-aided reasoning is further demonstrated in the companion book, Computer-Aided Reasoning: ACL2 Case Studies. ::: Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, http://www.cs.utexas.edu/users/moore/ac12, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation. ::: ::: ACL2 Case Studies ::: Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided reasoning system ACL2 can be used in productive and innovative ways to design, build, and maintain hardware and software systems. Included here are technical papers written by twenty-one contributors that report on self-contained case studies, some of which are sanitized industrial projects. The papers deal with a wide variety of ideas, including floating-point arithmetic, microprocessor simulation, model checking, symbolic trajectory evaluation, compilation, proof checking, real analysis, and several others. ::: Computer-Aided Reasoning: ACL2 Case Studies is meant for two audiences: those looking for innovative ways to design, build, and maintain hardware and software systems faster and more reliably, and those wishing to learn how to do this. The former audience includes project managers and students in survey-oriented courses. The latter audience includes students and professionals pursuing rigorous approaches to hardware and software engineering or formal methods. Computer-Aided Reasoning: ACL2 Case Studies can be used in graduate and upper-division undergraduate courses on Software Engineering, Formal Methods, Hardware Design, Theory of Computation, Artificial Intelligence, and Automated Reasoning. ::: The book is divided into two parts. Part I begins with a discussion of the effort involved in using ACL2. It also contains a brief introduction to the ACL2 logic and its mechanization, which is intended to give the reader sufficient background to read the case studies. A more thorough, textbook introduction to ACL2 may be found in the companion book, Computer-Aided Reasoning: An Approach. ::: The heart of the book is Part II, where the case studies are presented. The case studies contain exercises whose solutions are on the Web. In addition, the complete ACL2 scripts necessary to formalize the models and prove all the properties discussed are on the Web. For example, when we say that one of the case studies formalizes a floating-point multiplier and proves it correct, we mean that not only can you read an English description of the model and how it was proved correct, but you can obtain the entire formal content of the project and replay the proofs, if you wish, with your copy of ACL2. ::: ACL2 may be obtained from its home page, http://www.cs.utexas.edu/users/moore/ac12. The results reported in each case study, as ACL2 input scripts, as well as exercise solutions for both books, are available from this page.
---
paper_title: Programming semantics for multiprogrammed computations

paper_content:

The semantics are defined for a number of meta-instructions which perform operations essential to the writing of programs in multiprogrammed computer systems. These meta-instructions relate to parallel processing, protecting of separate computations, program debugging, and the sharing among users of memory segments and other computing objects, the names of which are hierarchically structured. The language sophistication contemplated is midway between an assembly language and an advanced algebraic language.
---
paper_title: On the derivation of secure components

paper_content:

The author discusses the problems in deriving a system from its specification when that specification includes simple trace-based information-flow security properties as well as safety properties. He presents two fundamental theorems of information-flow security which describe the inherent difficulties of deriving secure implementations and considers the implications of these results. It is concluded that it is dangerous to extrapolate from success in the case of two to the case of many. Results proved about systems with just low- and high-access users may not extend easily to full lattices. >
---
paper_title: Secure Computer Systems: Mathematical Foundations

paper_content:

This paper reports the first results of an investigation into solutions to problems of security in computer systems; it establishes the basis for rigorous investigation by providing a general descriptive model of a computer system.
---
paper_title: Proving that programs eventually do something good

paper_content:

In recent years we have seen great progress made in the area of automatic source-level static analysis tools. However, most of today's program verification tools are limited to properties that guarantee the absence of bad events (safety properties). Until now no formal software analysis tool has provided fully automatic support for proving properties that ensure that good events eventually happen (liveness properties). In this paper we present such a tool, which handles liveness properties of large systems written in C. Liveness properties are described in an extension of the specification language used in the SDV system. We have used the tool to automatically prove critical liveness properties of Windows device drivers and found several previously unknown liveness bugs.
---
paper_title: Thorough static analysis of device drivers

paper_content:

Bugs in kernel-level device drivers cause 85% of the system crashes in the Windows XP operating system [44]. One of the sources of these errors is the complexity of the Windows driver API itself: programmers must master a complex set of rules about how to use the driver API in order to create drivers that are good clients of the kernel. We have built a static analysis engine that finds API usage errors in C programs. The Static Driver Verifier tool (SDV) uses this engine to find kernel API usage errors in a driver. SDV includes models of the OS and the environment of the device driver, and over sixty API usage rules. SDV is intended to be used by driver developers "out of the box." Thus, it has stringent requirements: (1) complete automation with no input from the user; (2) a low rate of false errors. We discuss the techniques used in SDV to meet these requirements, and empirical results from running SDV on over one hundred Windows device drivers.
---
paper_title: The Flask Security Architecture: System Support for Diverse Security Policies

paper_content:

Operating systems must be flexible in their support for security policies, providing sufficient mechanisms for supporting the wide variety of real-world security policies. Such flexibility requires controlling the propagation of access rights, enforcing fine-grained access rights and supporting the revocation of previously granted access rights. Previous systems are lacking in at least one of these areas. In this paper we present an operating system security architecture that solves these problems. Control over propagation is provided by ensuring that the security policy is consulted for every security decision. This control is achieved without significant performance degradation through the use of a security decision caching mechanism that ensures a consistent view of policy decisions. Both fine-grained access rights and revocation support are provided by mechanisms that are directly integrated into the service-providing components of the system. The architecture is described through its prototype implementation in the Flask microkernel-based operating system, and the policy flexibility of the prototype is evaluated. We present initial evidence that the architecture's impact on both performance and code complexity is modest. Moreover, our architecture is applicable to many other types of operating systems and environments.
---
paper_title: Microkernels Meet Recursive Virtual Machines

paper_content:

This paper describes a novel approach to providingmodular and extensible operating system functionality and encapsulated environments based on a synthesis of microkernel and virtual machine concepts. We have developed a software-based virtualizable architecture called Fluke that allows recursive virtual machines (virtual machines running on other virtual machines) to be implemented efficiently by a microkernel running on generic hardware. A complete virtual machine interface is provided at each level; efficiency derives from needing to implement only new functionality at each level. This infrastructure allows common OS functionality, such as process management, demand paging, fault tolerance, and debugging support, to be provided by cleanly modularized, independent, stackable virtual machine monitors, implemented as user processes. It can also provide uncommon or unique OS features, including the above features specialized for particular applications’ needs, virtual machines transparently distributed cross-node, or security monitors that allow arbitrary untrusted binaries to be executed safely. Our prototype implementation of this model indicates that it is practical to modularize operating systems this way. Some types of virtual machine layers impose almost no overhead at all, while others impose some overhead (typically 0–35%), but only on certain classes of applications.
---
paper_title: TAME: Using PVS strategies for special-purpose theorem proving

paper_content:

TAME (Timed Automata Modeling Environment), an interface to the theorem proving system PVS, is designed for proving properties of three classes of automata: I/O automata, Lynch–Vaandrager timed automata, and SCR automata. TAME provides templates for specifying these automata, a set of auxiliary theories, and a set of specialized PVS strategies that rely on these theories and on the structure of automata defined using the templates. Use of the TAME strategies simplifies the process of proving automaton properties, particularly state and transition invariants. TAME provides two types of strategies: strategies for “automatic” proof and strategies designed to implement “natural” proof steps, i.e., proof steps that mimic the high-level steps in typical natural language proofs. TAME's “natural” proof steps can be used both to mechanically check hand proofs in a straightforward way and to create proof scripts that can be understood without executing them in the PVS proof checker. Several new PVS features can be used to obtain better control and efficiency in user-defined strategies such as those used in TAME. This paper describes the TAME strategies, their use, and how their implementation exploits the structure of specifications and various PVS features. It also describes several features, currently unsupported in PVS, that would either allow additional “natural” proof steps in TAME or allow existing TAME proof steps to be improved. Lessons learned from TAME relevant to the development of similar specialized interfaces to PVS or other theorem provers are discussed.
---
paper_title: Running the manual: an approach to high-assurance microkernel development

paper_content:

We propose a development methodology for designing and prototyping high assurance microkernels, and describe our application of it. The methodology is based on rapid prototyping and iterative refinement of the microkernel in a functional programming language. The prototype provides a precise semi-formal model, which is also combined with a machine simulator to form a reference implementation capable of executing real user-level software, to obtain accurate feedback on the suitability of the kernel API during development phases. We extract from the prototype a machine-checkable formal specification in higher-order logic, which may be used to verify properties of the design, and also results in corrections to the design without the need for full verification. We found the approach leads to productive, highly iterative development where formal modelling, semi-formal design and prototyping, and end use all contribute to a more mature final design in a shorter period of time.
---
paper_title: Basing a Modeling Environment on a General Purpose Theorem Prover

paper_content:

Abstract : A general purpose theorem prover can be thought of as an extremely flexible modeling environment in which one can define and analyze almost any kind of model. A disadvantage to the full flexibility of a general purpose theorem prover is the lack of any guidance on how to construct a model and how then to apply the theorem prover to analyzing the model. In the general environment supplied by the prover, much time can be consumed in deciding how to specify a model and in interacting with and understanding feedback from the prover. However, specification templates, together with proof strategies whose design follows certain principles, can be used in many general purpose provers to create specialized modeling environments that address these difficulties. A specialized modeling environment created in this way can be further extended and/or further specialized by drawing on the underlying theorem prover for additional capabilities, and provides a means of integrating powerful theorem proving capabilities into existing software development environments by way of appropriate translation schemes. This paper will use TAME (Timed Automata Modeling Environment) to illustrate the creation, extension, and specialization of a modeling environment based on PVS, and its integration into several software development environments.
---
paper_title: Certifying low-level programs with hardware interrupts and preemptive threads

paper_content:

Hardware interrupts are widely used in the world's critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system programming. Unfortunately, interrupts are also extremely hard to reason about: they dramatically alter the program control flow and complicate the invariants in low-level concurrent code (e.g., implementation of synchronization primitives). Existing formal verification techniques---including Hoare logic, typed assembly language, concurrent separation logic, and the assume-guarantee method---have consistently ignored the issues of interrupts; this severely limits the applicability and power of today's program verification systems. In this paper we present a novel Hoare-logic-like framework for certifying low-level system programs involving both hardware interrupts and preemptive threads. We show that enabling and disabling interrupts can be formalized precisely using simple ownership-transfer semantics, and the same technique also extends to the concurrent setting. By carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we are able to---for the first time---successfully certify a preemptive thread implementation and a large number of common synchronization primitives. Our work provides a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified operating system kernels and hypervisors.
---
paper_title: An Open Framework for Certified System Software

paper_content:

Certified software consists of a machine executable program plus a machine checkable proof showing that the software is free of bugs with respect to a particular specification. Constructing certified system software is an important step toward building a reliable and secure computing platform for future critical applications. In addition to the benefits from provably safe components, architectures of certified systems may also be simplified to achieve better efficiency. However, because system software consists of program modules that use many different computation features and span different abstraction levels, it is difficult to design a single type system or program logic to certify the whole system. As a result, significant amount of kernel code of today's operating systems has to be implemented in unsafe languages, despite recent progress on type-safe languages. ::: In this thesis, I develop a new methodology to solve this problem, which applies different verification systems to certify different program modules, and then links the certified modules in an open framework to compose the whole certified software package. Specifically, this thesis makes contributions in the following two aspects. ::: First, I develop new Hoare-style program logics to certify low-level programs with different features, such as sequential programs with stack-based control abstractions and multi-threaded programs with unbounded thread creations. A common scheme in the design of these logics is modularity. They all support modular verification in the sense that program modules, such as functions and threads, can be certified separately without looking into implementation details of others. ::: Second, I propose an open verification framework that enables interoperation between different verification systems (a.k.a. foreign systems). The framework is open in that it is not designed with a priori knowledge of foreign systems. It is general enough to incorporate both existing verification systems and new program logics presented in this thesis. It also supports modularity and proof reuse. Modules can be certified separately without knowing about implementation details of other modules and about the verification systems in which other modules are certified. Soundness of the framework guarantees that specifications of modules are respected after linking.
---
paper_title: Formal specification and verification of data separation in a separation kernel for an embedded system

paper_content:

Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to rea-son about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded soft-ware system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of dataseparation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS.
---
paper_title: The existence of refinement mappings

paper_content:

Abstract Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. We consider specifications consisting of a state machine (which may be infinite- state) that specifies safety requirements, and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S 1 to a higher-level one S 2 is a mapping from S 1 's state space to S 2 's state space. It maps steps of S 1 's state machine to steps of S 2 's state machine and maps behaviors allowed by S 1 to behaviors allowed by S 2 . We show that, under reasonable assumptions about the specification, if S 1 implements S 2 , then by adding auxiliary variables to S 1 we can guarantee the existence of a refinement mapping. This provides a completeness result for a practical, hierarchical specification method.
---
paper_title: Applying Formal Methods to a Certifiably Secure Software System

paper_content:

A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This paper describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, a compact security model containing only information needed to reason about the security properties of interest is constructed and the security properties are represented formally in terms of the model. To reduce the cost of verification, the code to be verified is partitioned into three categories and only the first category, which is less than 10 percent of the code in our application, requires formal verification. The proof of the other two categories is relatively trivial. Our approach was developed to support a common criteria evaluation of the separation kernel of an embedded software system. This paper describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced, that is, a top-level specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. This paper also presents the formal basis for the argument that the kernel code conforms to the TLS and consequently satisfies the security property.
---
paper_title: Computer-Aided Reasoning: An Approach

paper_content:

From the Publisher: ::: An Approach ::: Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, or theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on artificial intelligence or automated reasoning and as a reference for business and industry. ::: Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction. ::: In this book we present: ::: ::: A practical functional programming language closely related to Common Lisp which is used to define functions (which can model computing systems) and to make assertions about defined functions; A formal logic in which defined functions correspond to axioms; the logic is first-order, includes induction, and allows us to prove theorems about the functions; The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process. ::: ::: The ACL2 system hasbeen successfully applied to projects of commercial interest, including microprocessor, modeling, hardware verification, microcode verification, and software verification. This book gives a methodology for modeling computing systems formally and for reasoning about those models with mechanized assistance. The practicality of computer-aided reasoning is further demonstrated in the companion book, Computer-Aided Reasoning: ACL2 Case Studies. ::: Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, http://www.cs.utexas.edu/users/moore/ac12, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation. ::: ::: ACL2 Case Studies ::: Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided reasoning system ACL2 can be used in productive and innovative ways to design, build, and maintain hardware and software systems. Included here are technical papers written by twenty-one contributors that report on self-contained case studies, some of which are sanitized industrial projects. The papers deal with a wide variety of ideas, including floating-point arithmetic, microprocessor simulation, model checking, symbolic trajectory evaluation, compilation, proof checking, real analysis, and several others. ::: Computer-Aided Reasoning: ACL2 Case Studies is meant for two audiences: those looking for innovative ways to design, build, and maintain hardware and software systems faster and more reliably, and those wishing to learn how to do this. The former audience includes project managers and students in survey-oriented courses. The latter audience includes students and professionals pursuing rigorous approaches to hardware and software engineering or formal methods. Computer-Aided Reasoning: ACL2 Case Studies can be used in graduate and upper-division undergraduate courses on Software Engineering, Formal Methods, Hardware Design, Theory of Computation, Artificial Intelligence, and Automated Reasoning. ::: The book is divided into two parts. Part I begins with a discussion of the effort involved in using ACL2. It also contains a brief introduction to the ACL2 logic and its mechanization, which is intended to give the reader sufficient background to read the case studies. A more thorough, textbook introduction to ACL2 may be found in the companion book, Computer-Aided Reasoning: An Approach. ::: The heart of the book is Part II, where the case studies are presented. The case studies contain exercises whose solutions are on the Web. In addition, the complete ACL2 scripts necessary to formalize the models and prove all the properties discussed are on the Web. For example, when we say that one of the case studies formalizes a floating-point multiplier and proves it correct, we mean that not only can you read an English description of the model and how it was proved correct, but you can obtain the entire formal content of the project and replay the proofs, if you wish, with your copy of ACL2. ::: ACL2 may be obtained from its home page, http://www.cs.utexas.edu/users/moore/ac12. The results reported in each case study, as ACL2 input scripts, as well as exercise solutions for both books, are available from this page.
---
paper_title: A robust machine code proof framework for highly secure applications

paper_content:

Security-critical applications at the highest Evaluation Assurance Levels (EAL) require formal proofs of correctness in order to achieve certification. To support secure application development at the highest EALs, we have developed techniques to largely automate the process of producing proofs of correctness of machine code. As part of the Secure, High-Assurance Development Environment program, we have produced in ACL2 an executable formal model of the Rockwell Collins AAMP7G microprocessor at the instruction set level, in order to facilitate proofs of correctness about that processor's machine code. The AAMP7G, currently in use in Rockwell Collins secure system products, supports strict time and space partitioning in hardware, and has received a U.S. National Security Agency (NSA) Multiple Independent Levels of Security (MILS) certificate based in part on a formal proof of correctness of its separation kernel microcode. Proofs of correctness of AAMP7G machine code are accomplished using the method of "compositional cutpoints", which requires neither traditional clock functions nor a Verification Condition Generator (VCG). In this paper, we will summarize the AAMP7G architecture, detail our ACL2 model of the processor, and describe our development of the compositional cutpoint method into a robust machine code proof framework.
---
paper_title: UCLA data secure unix

paper_content:

Monochlorotoluene that contains at least 45 percent of para-chlorotoluene is prepared by contacting toluene with chlorine in the presence of a catalyst system that contains a ferrocene compound and a sulfur compound.
---
paper_title: A Technique for Proving Specifications are Multilevel Secure

paper_content:

Abstract : This document describe a technique for verifying that a design for an operating system or subsystem expressed in terms of a formal specification is consistent with a particular model of multilevel security. The technique to be described is mathematically rigorous and, if applied properly, gives assurance that the given design is multilevel secure by this particular model. The technique is supported by a collection of automated tools. These tools assist the user in the performance of a large amount of detailed routine tasks that must be performed to apply the technique. In general, contemporary formal verification techniques such as the one described here involve a great deal of repetitive, detailed, uninteresting steps that are necessary to maintain the rigor of the proof process. The proof are usually larger and more complex than the system being proved. Keywords: Critical technology.
---
paper_title: A model for verification of data security in operating systems

paper_content:

Program verification applied to kernel architectures forms a promising method for providing uncircumventably secure, shared computer systems. A precise definition of data security is developed here in terms of a general model for operating systems. This model is suitable as a basis for verifying many of those properties of an operating system which are necessary to assure reliable enforcement of security. The application of this approach to the UCLA secure operating system is also discussed.
---
paper_title: Programming from specifications

paper_content:

Providing a thorough treatment of most elementary programme development techniques, this revised edition covers topics such as procedures, parameters, recursion and data refinement, with the integration of specification, development and coding, based on ordinary (classical) logic. This second edition features: substantial restructuring of earlier material, streamlining the introduction of programming language features; simplified presentation of procedures, parameters and recursion; an expanded chapter on data refinement, giving the much simpler laws that specialize to functional abstractions; a new chapter on recursive types (trees etc) and appropriate control structures; and, following the original concluding case study, two completely new ones: "the recursive treatment of the largest rectangle under a histogram", and a specification and extended developnent of an electronic mail system (including limited concurrency).
---
paper_title: The foundations of a provably secure operating system (PSOS)

paper_content:

PSOS has been designed according to a set of formal techniques embodying the SRI Hierarchical Development Methodology (HDM). HDM has been described elsewhere, 1 – 3 and thus is only summarized here. The influence of HDM on the security of PSOS is also discussed elsewhere. 4 In addition, Linden 5 gives a general discussion of the impact of structured design techniques on the security of operating systems (including capability systems).
---
paper_title: Proof techniques for hierarchically structured programs

paper_content:

A method for describing and structuring programs that simplifies proofs of their correctness is presented. The method formally represents a program in terms of levels of abstraction, each level of which can be described by a self-contained nonprocedural specification. The proofs, like the programs, are structured by levels. Although only manual proofs are described in the paper, the method is also applicable to semi-automatic and automatic proofs. Preliminary results are encouraging, indicating that the method can be applied to large programs, such as operating systems.
---
paper_title: Extending the Noninterference Version of MLS for SAT

paper_content:

A noninterference formulation of MLS applicable to the Secure Ada® Target (SAT) Abstract Model is developed. An analogous formulation is developed to handle the SAT type enforcement policy. Unwinding theorems are presented for both MLS and Multidomain Security (MDS) and the SAT Abstract Model is shown to satisfy both MLS and MDS. Generalizations and extensions are also considered.
---
paper_title: Kit and the short stack

paper_content:

Kit is a small multi-tasking operating system kernel written in the machine language of a uni-processor von Neumann computer. The kernel is proved to implement on this shared computer a fixed number of conceptually distributed communicating processes. In addition to implementing processes, the kernel provides the following verified services: process scheduling, error handling, message passing, and an interface to asynchronous devices. We summarize the Kit project in order to discuss the place Kit could occupy in the verified stack of system components containing Micro-Gypsy, Piton and FM8502.
---
paper_title: Kit : A Study in Operating System Verification

paper_content:

The author reviews Kit, a small multitasking operating system kernel written in the machine language of a uniprocessor von Neumann computer. The kernel is proved to implement on this shared computer a fixed number of conceptually distributed communicating processes. In addition to implementing processes, the kernel provides the following verified services: process scheduling, error handling, message passing, and an interface to asynchronous devices. As a by-product of the correctness proof, security-related results such as the protection of the kernel from tasks and the inability of tasks to enter supervisor mode are proved. The problem is stated in the Boyer-Moore logic, and the proof is mechanically checked with the Boyer-Moore theorem prover. >
---
paper_title: A Verified Operating System Kernel

paper_content:

We present a multitasking operating system kernel, called KIT, written in the machine language of a uni-processor von Neumann computer. The kernel is proved to implement, on this shared computer, a fixed number of conceptually distributed communicating processes. In addition to implementing processes, the kernel provides the following verified services: process scheduling, error handling, message passing, and an interface to asynchronous devices. The problem is stated in the Boyer-Moore logic, and the proof is mechanically checked with the Boyer-Moore theorem prover.
---
paper_title: KSOS—The design of a secure operating system*

paper_content:

This paper discusses the design of the Department of Defense (DoD) Kemelized Secure Operating System (KSOS, formerly called Secure UNIX). ** KSOS is intended to provide a provably secure operating system for larger minicomputers. KSOS will provide a system call interface closely compatible with the UNIX operating system. The initial implementation of KSOS will be on a Digital Equipment Corporation PDP-11/70 computer system. A group from Honeywell is also proceeding with an implementation for a modified version of the Honeywell Level 6 computer system.
---
paper_title: Some Techniques for Proving Correctness of Programs which Alter Data Structures

paper_content:

A metal oxide varistor has a high thermal conductivity potting material encapsulating completely the metal oxide varistor and a portion of the leads therefrom, a pair of metal plates spaced in a generally parallel reslationship to the opposite major surfaces of the varistor and bonded thereto by the potting material, and one of the plates having at least a pair of mounting holes therein or other suitable means.
---
paper_title: Pragmatic nonblocking synchronization for real-time systems

paper_content:

We present a pragmatic methodology for designing nonblocking real-time systems. Our methodology uses a combination of lock-free and wait-free synchronization techniques and clearly states which technique should be applied in which situation. This paper reports novel results in various respects: We restrict the usage of lock-free mechanisms to cases where the widely available atomic singleword compare-and-swap operation suffices. We show how Brinch Hansen’s monitors (alias Java’s synchronized methods) can be implemented on top of our mechanisms, thereby demonstrating their versatility. We describe in detail how we used the mechanisms for a full reimplementation of a popular microkernel interface (L4). Our kernel— in contrast to the original implementation—bounds execution time of all operations. We report on a previous implementation of our mechanisms in which we used Massalin’s and Pu’s single-server approach, and on the resulting performance, which lead us to abandon this well-known scheme. Our microkernel implementation is in daily use with a user-level Linux server running a large variety of applications. Hence, our system can be considered as more than just an academic prototype. Still, and despite its implementation in C++, it compares favorably with the original, highly optimized, non-real-time, assembly-language implementation.
---
paper_title: The semantics of C++ data types: Towards verifying low-level system components

paper_content:

In order to formally reason about low-level system programs one needs a semantics (for the programming language in question) that can deal with programs that are not statically type-correct. For system-level programs, the semantics must deal with such heretical constructs like casting integers to pointers and converting pointers between incompatible base types. In this paper we describe a formal semantics for the data types of the C++ programming language that is suitable for low-level programs in the above sense. This work is part of a semantics for a large subset of the C++ programming language developed in the VFiasco project. In the VFiasco project we aim at the verification of substantial properties of the Fiasco microkernel, which is written in C++.
---
paper_title: The Formal Semantics of Programming Languages

paper_content:

A shutter mechanism alternates between an exposure phase and a reflex phase. In the reflex phase it reflects incident scene light onto a light-sensitive stage which generates a light-indicating signal. A first control pulse is generated at the start of the reflex phase, and a second control pulse at the end of the reflex phase. An integrating circuit receives the first pulse and during the reflex phase generates an integral signal dependent upon the time integral of the light-indicating signal. A signal-transmission switch is operative in response to the second pulse for transmitting the integral signal to a signal-storing stage. The signal from the signal-storing stage is used as the feedback signal to a negative-feedback control arrangement for the camera diaphragm. This feedback signal is dependent not only upon scene light but also the duration of the reflex phase. Accordingly, if the scene light remains constant but the speed of the motor driving the shutter is below or above rated speed, that is automatically compensated by a change in the feedback signal, so that the diaphragm setting takes into account the longer or shorter exposure times resulting from the shutter-motor speed deviation.
---
paper_title: A formal model of memory peculiarities for the verification of low-level operating-system code

paper_content:

This paper presents our solutions to some problems we encountered in an ongoing attempt to verify the micro-hypervisor currently developed within the Robin project. The problems that we discuss are (1) efficient automatic reasoning for type-correct programs in virtual memory, and (2) modeling memory-mapped devices with alignment requirements. The discussed solutions are integrated in our verification environment for operating-system kernels in the interactive theorem prover PVS. This verification environment will ultimately be used for the verification of the Robin micro-hypervisor. As a proof of concept we include an example verification of a very simple piece of code in our environment.
---
paper_title: Applying source-code verification to a microkernel: the VFiasco project

paper_content:

We present the VFiasco project, in which we apply source-code verification to a complete operating-system kernel written in C++. The aim of the VFiasco project is to establish security-relevant properties of the Fiasco microkernel.Source-code verification works by reasoning about the semantics of the full source code of a program. Traditionally it is limited to small programs written in an academic programming language. The project's main challenges are to enable high-level reasoning about typed data starting from only low-level knowledge about the hardware, and to develop a clean semantics for the subset of C++ used by the kernel. In this extended abstract we present our ideas for tackling these challenges. We focus on a type-safe object store that is based on a hardware model that closely resembles the IA32 virtual-memory architecture and on guarantees provided by the kernel itself. We also briefly touch on the semantics for C++.Please find the full version of this paper at http://www.vfiasco.org/objstore.pdf.
---
paper_title: A Linear Time Algorithm for Deciding Subject Security

paper_content:

A particular protection mechanism from the protection hterature-the take and grant system--is presented For this particular mechanism, it is shown that the safety problem can be solved in linear time Moreover the security policies that this mechanism can enforce are characterized The theoretical analysis of systems for protectmg the security of reformation should be of interest to the practmoner as well as the theorehctan. The practitioner must convince users that the integrity of their programs and files is maintained; Le. he must convince them that the operating system and its mechanisms will correctly protect these programs and files Vague or informal arguments are unacceptable since they are often wrong. Indeed the folklore is replete with stones of "secure" systems being compromised m a matter of hours. A primary reason for the abundance of these incidents is that even a small set of apparently simple protection pnmmves can often lead to complex systems that can be exploited, and therefore compromised, by some adversary. But it is preosely this fact, simple primitives with complex behavior, that lures the theoretician. Our purpose here is to present a concrete example of a protection system and then to completely analyze its behavior. Our motivation for doing this analysis ~s twofold. The protection system that we study ~s not one we invented, rather it appears, for example, in Cohen (1) Moreover it is closely related to systems studied m Denning and Graham (2) and Jones (4). This point is most important, for the space of possible protection systems is exceedingly nch and it is trivial to think up arbitrary systems to study. We are interested not in arbitrary systems, but in systems that have practical apphcahon The above motivation is necessary but not sufficient for us to establish that these questions should interest the theoreticmn. Our second reason for studying these prob- lems is that m a natural way they can be viewed as "generahzat~ons of transitive closure." Informally, our model is:
---
paper_title: Verifying the EROS confinement mechanism

paper_content:

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.
---
paper_title: An axiomatic basis for computer programming

paper_content:

In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantages, both theoretical and practical, may follow from a pursuance of these topics.
---
paper_title: Formal verification of a C compiler front-end

paper_content:

This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the specification language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.
---
paper_title: Formal pervasive verification of a paging mechanism

paper_content:

Memory virtualization by means of demand paging is a crucial component of every modern operating system. The formal verification is challenging since reasoning about the page fault handler has to cover two concurrent computational sources: the processor and the hard disk. We accurately model the interleaved executions of devices and the page fault handler, which is written in a high-level programming language with inline assembler portions. We describe how to combine results from sequential Hoare logic style reasoning about the page fault handler on the low-level concurrent machine model. To the best of our knowledge this is the first example of pervasive formal verification of software communicating with devices.
---
paper_title: Computer Architecture: A Quantitative Approach

paper_content:

This best-selling title, considered for over a decade to be essential reading for every serious student and practitioner of computer design, has been updated throughout to address the most important trends facing computer designers today. In this edition, the authors bring their trademark method of quantitative analysis not only to high-performance desktop machine design, but also to the design of embedded and server systems. They have illustrated their principles with designs from all three of these domains, including examples from consumer electronics, multimedia and Web technologies, and high-performance computing.
---
paper_title: On the Architecture of System Verification Environments

paper_content:

Implementations of computer systems comprise many layers and employ a variety of programming languages. Building such systems requires support of an often complex, accompanying tool chain. ::: ::: The Verisoft project deals with the formal pervasive verification of computer systems. Making use of appropriate formal specification and proof tools, this task requires (i) specifying the layers and languages used in the implementation, (ii) specifying and verifying the algorithms employed by the tool chain (or, alternatively, validating their actual output), and (iii) proving simulation statements between layers, arguing about the programs residing at the different layers. Combining the simulation statements for all layers should allow to transfer correctness results for top-layer programs to their bottom-layer representation; in this manner, a verified stack can be built. ::: ::: Maintaining all formal artifacts, the actual system implementation, and the (verification) tool chain is a challenging task. We call sets of tools that help addressing this task system verification environments. In this paper, we describe the structure, contents, and architecture of the system verification environment used in the Verisoft project.
---
paper_title: Formal certification of a compiler back-end or: programming a compiler with a proof assistant

paper_content:

This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
---
paper_title: Correct Microkernel Primitives

paper_content:

Primitives are basic means provided by a microkernel to implementors of operating system services. Intensively used within every OS and commonly implemented in a mixture of high-level and assembly programming languages, primitives are meaningful and challenging candidates for formal verification. We report on the accomplished correctness proof of academic microkernel primitives. We describe how a novel approach to verification of programs written in C with inline assembler is successfully applied to a piece of realistic system software. Necessary and sufficient criteria covering functional correctness and requirements for the integration into a formal model of memory virtualization are determined and formally proven. The presented results are important milestones on the way to a pervasively verified operating system.
---
paper_title: Pervasive Compiler Verification -- From Verified Programs to Verified Systems

paper_content:

We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties from the C0 layer to the assembler and hardware layers. The compiler verification is split into two parts: the correctness of the compiling specification (which can be translated to executable ML code via Isabelle's code generator) and the correctness of a C0 implementation of this specification. We also sketch a method to solve the boot strap problem, i.e., how to obtain a trustworthy binary of the C0 compiler from its C0 implementation. Ultimately, this allows to prove pervasively the correctness of compiled C0 programs in the real system.
---
paper_title: On the Verification of Memory Management Mechanisms

paper_content:

We report on the design and formal verification of a complex processor supporting address translation by means of a memory management unit (MMU). We give a paper and pencil proof that such a processor together with an appropriate page fault handler simulates virtual machines modeling user computation. These results are crucial steps towards the seamless verification of entire computer systems.
---
paper_title: A verification environment for sequential imperative programs in Isabelle/HOL

paper_content:

We develop a general language model for sequential imperative programs together with a Hoare logic. We instantiate the framework with common programming language constructs and integrate it into Isabelle/HOL, to gain a usable and sound verification environment.
---
paper_title: Formal Device and Programming Model for a Serial Interface

paper_content:

The verification of device drivers is essential for the pervasive verification of an operating system. To show the correctness of device drivers, devices have to be formally modeled. In this paper we present the formal model of the serial interface controller UART 16550A. By combining the device model with a formal model of a processor instruction set architecture we obtain an assembler-level programming model for a serial interface. As a programming and verification example we present a simple UART driver implemented in assembler and prove its correctness. All models presented in this paper have been formally specified in the Isabelle/HOL theorem prover.
---
paper_title: An approach to systems verification

paper_content:

The term systems verification refers to the specification and verification of the components of a computing system, including compilers, assemblers, operating systems and hardware. We outline our approach to systems verification, and summarize the application of this approach to several systems components. These components consist of a code generator for a simple high-level language, an assembler and linking loader, a simple operating system kernel, and a microprocessor design.
---
paper_title: A machine-checked model for a Java-like language, virtual machine, and compiler

paper_content:

We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between the realism of the language and the tractability and clarity of its formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence, a type system and a definite initialisation analysis, a type safety proof of the small step semantics, a virtual machine (JVM), its operational semantics and its type system, a type safety proof for the JVM; a bytecode verifier, that is, a data flow analyser for the JVM, a correctness proof of the bytecode verifier with respect to the type system, and a compiler and a proof that it preserves semantics and well-typedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine, and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.
---
paper_title: Towards the formal verification of a C0 compiler: code generation and implementation correctness

paper_content:

In the spirit of the famous CLI stack project the Verisoft project aims at the pervasive verification of entire computer systems including hardware, system software, compiler, and communicating applications, with a special focus on industrial applications. The main programming language used in the Verisoft project is C0 (a subset of C which is similar to MISRA C). This paper reports on (i) an operational small steps semantics for C0 which is formalized in Isabelle/HOL, (ii) the formal specification of a compiler from C0 to the DLX machine language in Isabelle/HOL, (iii) a paper and pencil correctness proof for this compiler and the status of the formal verification effort for this proof, and (iv) the implementation of the compiler in C0 and a formal proof in Isabelle/HOL that the implementation produces the same code as the specification.
---
paper_title: Putting it all together – Formal verification of the VAMP

paper_content:

In the verified architecture microprocessor (VAMP) project we have designed, functionally verified, and synthesized a processor with full DLX instruction set, delayed branch, Tomasulo scheduler, maskable nested precise interrupts, pipelined fully IEEE compatible dual precision floating point unit with variable latency, and separate instruction and data caches. The verification has been carried out in the theorem proving system PVS. The processor has been implemented on a Xilinx FPGA.
---
paper_title: Integration of a Software Model Checker into Isabelle

paper_content:

The paper presents a combination of interactive and automatic tools in the area of software verification. We have integrated a newly developed software model checker into an interactive verification environment for imperative programming languages. Although the problems in software verification are mostly too hard for full automation, we could increase the level of automated assistance by discharging less interesting side conditions. That allows the verification engineer to focus on the abstract algorithm, safely assuming unbounded arithmetic and unlimited buffers.
---
paper_title: Separation logic: a logic for shared mutable data structures

paper_content:

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.
---
paper_title: Formalising a high-performance microkernel

paper_content:

This paper argues that a pragmatic approach is needed for integrating design and formalisation of complex systems. We report on our approach to designing the seL4 operating system microkernel API and its formalisation in Isabelle/HOL. The formalisation consists of the systematic translation of significant parts of the functional programming language Haskell into Isabelle/HOL, including monadbased code. We give an account of the experience, decisions and outcomes in this translation as well as the technical problems we encountered together with our solutions. The longer-term goal is to demonstrate that formalisation and verification of a large, complex, OS-level code base is feasible with current tools and methods and is in the order of magnitude of traditional development cost.
---
paper_title: A Linear Time Algorithm for Deciding Subject Security

paper_content:

A particular protection mechanism from the protection hterature-the take and grant system--is presented For this particular mechanism, it is shown that the safety problem can be solved in linear time Moreover the security policies that this mechanism can enforce are characterized The theoretical analysis of systems for protectmg the security of reformation should be of interest to the practmoner as well as the theorehctan. The practitioner must convince users that the integrity of their programs and files is maintained; Le. he must convince them that the operating system and its mechanisms will correctly protect these programs and files Vague or informal arguments are unacceptable since they are often wrong. Indeed the folklore is replete with stones of "secure" systems being compromised m a matter of hours. A primary reason for the abundance of these incidents is that even a small set of apparently simple protection pnmmves can often lead to complex systems that can be exploited, and therefore compromised, by some adversary. But it is preosely this fact, simple primitives with complex behavior, that lures the theoretician. Our purpose here is to present a concrete example of a protection system and then to completely analyze its behavior. Our motivation for doing this analysis ~s twofold. The protection system that we study ~s not one we invented, rather it appears, for example, in Cohen (1) Moreover it is closely related to systems studied m Denning and Graham (2) and Jones (4). This point is most important, for the space of possible protection systems is exceedingly nch and it is trivial to think up arbitrary systems to study. We are interested not in arbitrary systems, but in systems that have practical apphcahon The above motivation is necessary but not sufficient for us to establish that these questions should interest the theoreticmn. Our second reason for studying these prob- lems is that m a natural way they can be viewed as "generahzat~ons of transitive closure." Informally, our model is:
---
paper_title: Future Directions in the Evolution of the L4 Microkernel

paper_content:

L4 is a small microkernel that is used as a basis for several operating systems. L4 seems an ideal basis for embedded systems that possess and use memory protection. It could provide a reliable, robust, and secure embedded platform. This paper examines L4’s suitability as a basis for trustworthy embedded systems. It motivates the use of a microkernel, introduces L4 in particular as an example microkernel, overviews selected embedded applications benefiting from memory protection (focusing mostly on security related applications), and then examines L4’s applicability to those application domains and identifies issues with L4’s abstractions and mechanisms.
---
paper_title: A Logic for Virtual Memory

paper_content:

We present an extension to classical separation logic which allows reasoning about virtual memory. Our logic is formalised in the Isabelle/HOL theorem prover in a manner allowing classical separation logic notation to be used at an abstract level. We demonstrate that in the common cases, such as user applications, our logic reduces to classical separation logic. At the same time we can express properties about page tables, direct physical memory access, virtual memory access, and shared memory in detail.
---
paper_title: A memory allocation model for an embedded microkernel

paper_content:

High-end embedded systems featuring millions of lines of code, with varying degrees of assurance, are becoming commonplace. These devices are typically expected to meet diverse application requirements within tight resource budgets. Their growing complexity makes it increasingly difficult to ensure that they are secure and robust. One approach is to provide strong guarantees of isolation between components — thereby ensuring that the effects of any misbehaviour are confined to the misbehaving component. This paper focuses on an aspect of the system’s behaviour that is critical to any such guarantee: management of physical memory resources. In this paper, we present a secure physical memory management model that gives hard guarantees on physical memory consumption. The model dictates the inkernel mechanisms for allocation, however the allocation policy is implemented outside the kernel. We also argue that exporting allocation to user-level provides the flexibility necessary to implement the diverse resource management policies needed in embedded systems, while retaining the high-assurance properties of a formally verified kernel.
---
paper_title: Proving Pointer Programs in Hoare Logic

paper_content:

It is possible, but difficult, to reason in Hoare logic about programs which address and modify data structures defined by pointers. The challenge is to approach the simplicity of Hoare logic’s treatment of variable assignment, where substitution affects only relevant assertion formula. The axiom of assignment to object components treats each component name as a pointer-indexed array. This permits a formal treatment of inductively defined data structures in the heap but tends to produce instances of modified component mappings in arguments to inductively defined assertions. The major weapons against these troublesome mappings are assertions which describe spatial separation of data structures. Three example proofs are sketched.
---
paper_title: Pervasive Compiler Verification -- From Verified Programs to Verified Systems

paper_content:

We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties from the C0 layer to the assembler and hardware layers. The compiler verification is split into two parts: the correctness of the compiling specification (which can be translated to executable ML code via Isabelle's code generator) and the correctness of a C0 implementation of this specification. We also sketch a method to solve the boot strap problem, i.e., how to obtain a trustworthy binary of the C0 compiler from its C0 implementation. Ultimately, this allows to prove pervasively the correctness of compiled C0 programs in the real system.
---
paper_title: Some Techniques for Proving Correctness of Programs which Alter Data Structures

paper_content:

A metal oxide varistor has a high thermal conductivity potting material encapsulating completely the metal oxide varistor and a portion of the leads therefrom, a pair of metal plates spaced in a generally parallel reslationship to the opposite major surfaces of the varistor and bonded thereto by the potting material, and one of the plates having at least a pair of mounting holes therein or other suitable means.
---
paper_title: Types, bytes, and separation logic

paper_content:

We present a formal model of memory that both captures the low-level features of C's pointers and memory, and that forms the basis for an expressive implementation of separation logic. At the low level, we do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap. At the level of separation logic, we are still able to reason abstractly and efficiently. We implement this framework in the theorem prover Isabelle/HOL and demonstrate it on two case studies. We show that the divide between detailed and abstract does not impose undue verification overhead, and that simple programs remain easy to verify. We also show that the framework is applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel.
---
paper_title: Towards a Practical, Verified Kernel

paper_content:

In the paper we examine one of the issues in designing, specifying, implementing and formally verifying a small operating system kernel -- how to provide a productive and iterative developmentmethodology for both operating system developers and formal methods practitioners. ::: ::: We espouse the use of functional programming languages as a medium for prototyping that is readily amenable to formalisation with a low barrier to entry for kernel developers, and report early experience in the process of designing and building seL4: a new, practical, and formally verified microkernel.
---
paper_title: Isabelle theories for machine words

paper_content:

We describe a collection of Isabelle theories which facilitate reasoning about machine words. For each possible word length, the words of that length form a type, and most of our work consists of generic theorems which can be applied to any such type. We develop the relationships between these words and integers (signed and unsigned), lists of booleans and functions from index to value, noting how these relationships are similar to those between an abstract type and its representing set. We discuss how we used Isabelle's bin type, before and after it was changed from a datatype to an abstract type, and the techniques we used to retain, as nearly as possible, the convenience of primitive recursive definitions. We describe other useful techniques, such as encoding the word length in the type.
---

Title: Operating System Verification — An Overview

Section 1: Introduction
Description 1: Introduce the motivation for operating system verification and the historical background of software complexity and the software crisis. Explain briefly the goals of this article including highlighting formal, mathematical proof as a solution for achieving high assurance in software implementation correctness.

Section 2: Software Verification
Description 2: Provide an overview of software verification in general, focusing on formal verification. Discuss how formal verification fits into the broader context of software development, its promises, and the remaining risks.

Section 3: Microkernels
Description 3: Introduce operating system microkernels, their definition, and significance. Include explanations of sample architectures, their advantages, disadvantages, and trade-offs.

Section 4: Architectures
Description 4: Detail the various architectures of microkernels, comparing them with traditional monolithic kernels. Discuss their design philosophy and real-world applications.

Section 5: Services and Policies
Description 5: Discuss the usage scenarios, services, and mechanisms provided by microkernels. Include the emphasis on abstraction, flexibility, real-time capabilities, and security policies.

Section 6: OS Verification - The State of the Art
Description 6: Survey the state of the art in operating system verification. Provide an overview of different projects in the field, their goals, approaches, and outcomes. 

Section 7: Overview
Description 7: Present a high-level, table-style overview of the projects surveyed. Include brief backgrounds, goals, methods, and achievements of these projects.

Section 8: Related Projects
Description 8: Cover a number of smaller, related projects that have made significant contributions to the field of OS verification even if they did not target full microkernel verification.

Section 9: Early Work
Description 9: Dive into early work on OS verification, summarizing key projects such as UCLA Secure Unix, PSOS, and KIT. Discuss their methodologies, outcomes, and impact on later verification efforts.

Section 10: VFiasco
Description 10: Detail the VFiasco project, its goals, approaches, and contributions. Include discussions on its challenges and the modeling of the C++ language for verification.

Section 11: EROS/Coyotos
Description 11: Describe the Coyotos kernel and its predecessor EROS. Explain their security models, the shift towards formal verification in Coyotos, and the efforts involved in developing a suitable programming language for kernel implementation.

Section 12: Verisoft
Description 12: Provide a comprehensive overview of the Verisoft project, emphasizing its approach to pervasive verification from hardware to applications. Discuss the project's significant achievements and ongoing efforts.

Section 13: L4.verified/seL4
Description 13: Detail the L4.verified and seL4 projects, covering their tight integration, methodologies, verification accomplishments, and performance outcomes. Discuss future prospects and the commercial implications of these efforts.

Section 14: Conclusion
Description 14: Summarize the key findings, state of the art, and future directions in operating system verification. Offer insights into the feasibility of achieving comprehensive verification and the technological advancements that have made this possible.