We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.

We have developed a verified application proved to be both effective and efficient. The application generates moves in the puzzle-game Nim and is coded in Piton, a language with a formal semantics and a compiler verified to preserve its semantics on the underlying machine. The Piton compiler is targeted to the FM9001, a recently fabricated verified microprocessor. The Nim program correctness proof makes use of the language semantics that the compiler is proved to implement. Like the Piton compiler proof and FM9001 design proof, the Nim correctness proof is generated using Nqthm, a proof system sometimes known as the Boyer-Moore theorem prover.

The “Common Criteria” is an international standard for evaluating secure computer systems. The Common Criteria defines seven distinct Evaluation Assurance Levels (EALs). The three highest EALs, the so-called highassurance levels, require some degree of formalism in development. This paper discusses requirements for formalism in the high-assurance levels and our initial experiences in satisfying these requirements using ACL2.

Successful formal methods applications have four characteristics: intrinsically important applications, concise correctness theorems, validated models, and proof automation. We describe a recentlycompleted verification of a microprocessor's intrinsic partitioning mechanism in those terms. What Makes for a Good Application of Formal Methods? Formal methods is the application of mathematical reasoning to establish properties about digital systems. Formal methods can be applied in many different ways with many different notations and tools. They can deal with system models that describe the lowest level of implementation or the most abstract requirements, with properties to be proved that may be comprehensive descriptions of “correctness” or minor aspects that indicate good system development. Despite the wide range of formal methods applications, we observe that successful formal methods projects share four characteristics. 1. The target being analyzed is intrinsically important. Formal methods can provide a high level of certainty about a target, but the extra assurance must be worth the effort that formal verification usually entails. Three applications of formal methods that we consider successful are Microsoft’s SLAM project [Ball2004], AMD’s floating-point verification [Russinoff2000], and Rockwell Collins’ requirements validation [Miller2004]. The SLAM project aims to reduce crashes of Microsoft’s Windows OS by proving important device driver behaviors. AMD’s floating-point work seeks to eliminate errors in the floating-point units on AMD's x86 microprocessors. Rockwell Collins is applying model-checking to help validate requirements for safety-critical systems. Each of these applications of formal methods is solving a problem that is important enough to justify an extra effort. 2. The target’s desired behavior has a concise and understandable formalization. An important indicator of successful formal methods application is the degree to which the description of the needed property is compelling. A proved theorem only increases assurance about a target of evaluation if we trust in the formalization of the desired

The experimental feature MBE (for \must be equal") allows ACL2 users to introduce two versions of the body for a function, one for reasoning and one for execution [2]. The user must show that the two function bodies are equal when the function arguments satisfy the function guards. We demonstrate that MBE allows us to overcome an ACL2 logic weakness identi ed in an example presented at the 2nd ACL2 Workshop [4].

Formal verification can be used to establish important properties of critical systems. However, applying formal methods to a low-level implementation of a complex system is a daunting challenge, in part because extracting abstract functionality from a specific implementation is tedious. Automating such efforts by placing them under computer control helps free the user to focus on the essence of the verification problem. vFaat is a tool suite to assist in the formal verification of imperative code executing on von Neumann computing architectures. Building on our experience developing proofs about high-assurance microcoded processors, this work codifies several ad hoc techniques to simplify the process of reasoning about software-based systems. 1. The Promise and Challenge of Code Proofs 1.1 Formal Methods and the Code Verification Challenge Formal methods allow precise descriptions of systems and requirements and enable them to be related in a mathematically meaningful way. Formal verification can demonstrate that, under all conditions of interest, a particular design behaves as specified. A formal proof of correctness can account for every condition that the design might experience regardless of the size of the design’s state space. Formal methods therefore provide both the high assurance and the vital scaling property that are necessary for verifying complex designs. A crucial consideration in formal methods work is the level of abstraction that is appropriate for models. The use of high-level, abstract models as the basis for formal methods verification allows for simpler reasoning when the properties of interest can be conveniently addressed at the algorithmic level. An excellent example of reasoning about such an abstract system is the work at Rockwell Collins analyzing mode awareness in flight guidance systems that formally demonstrates that the design of modern flight automation software does not lead to dangerous ambiguities [Butler98, Miller01]. There are, however, several reasons for adopting a more detailed model of computation in some applications of formal methods. To guarantee the model’s fidelity In order for the evaluation of the system to take advantage of the formal methods, it must be certain that the formal model used to support the proofs actually reflects the behavior of the system being scrutinized. When the model is a low-level model based on the actual code it is easier to demonstrate this connection [Greve00c]. To reason about low-level primitives Assembly code and compiler directives are commonly used in low-level software implementations. Such constructs are most common in code of high criticality; code such as operating system kernels and math libraries. Unfortunately, the semantics of these primitives are often difficult to express at the source code level, making formal analysis nearly impossible. To avoid reasoning about compilers and other software tools By reasoning directly about low-level machine code or microcode, one bypasses tools such as compilers and linkers that could impact the correctness of an application.[Greve00b]. The disadvantage of reasoning about code directly, rather than at a more abstract level, is complexity. Code proofs involve many implementation details that would be ignored when reasoning about a more abstract model. Some work has been done on techniques for solving this problem. One notable project is the CLI short stack [Bevier89, Wilding93]. A family of implementations – an assembler, a compiler, a hardware design, and two applications – are shown to work together and are proved correct using a theorem prover. Yuan Yu demonstrated proofs of 68020 code, many of which were compiled into machine code from higher-level languges. [Yu92]. Rockwell Collins has used the PVS theorem proving system to reason about code in several projects [Wilding97, Greve98, Miller99]. This paper describes how we will develop tools to incorporate previously developed techniques into an automated tool supporting a code proof process. 1.2 The CAPS Project: A Critical Microcode Verification Approach The CAPS (Collins Adaptive Processing System) is a family of Rockwell Collins proprietary processors. In a multiyear IR&D effort, Rockwell Collins adapted and developed techniques that allow for formal code verification of the microcode running on members of this family. The motivation for this research was that CAPS microprocessors are used in some of the most safety-critical products that Rockwell Collins sells, and current microprocessor verification and certification techniques are extremely laborious. On this project formal verification techniques were applied to several sequences of actual microcode [Greve02, Greve00a, Wilding01a]. Three important aspects of this work were model development tools, proof decomposition techniques, and modeling and proof automation. • Formal Model Development Tools Rockwell Collins has developed tools and techniques for writing and reasoning about low level implementations. These methods enable the construction of formalized implementations of sufficient detail to execute device production tests. Such low level models provide high confidence in the fidelity of the model • Code Proof Decomposition A crucial challenge in code correctness proofs is developing a methodology for breaking the proof down into smaller, more manageable pieces. The three primary proof decomposition techniques exploited in the CAPS program were the separation of algorithm from implementation, the exploitation of code block structure to break code execution into discrete steps, and loop and block simplification. • Modeling and Proof Automation Modeling and proving programs correct requires ingenuity since intellectual effort is required to understand what a program does. However, many of the tasks associated with the process of modeling and proving code correct can be automated. In fact, automation of the model and proof process is crucial for making code proofs practical. Three forms of automation employed in the Rockwell Collins’ CAPS program were the mechanical generation of proofs, sophisticated reasoning libraries, and fundamental theorem prover enhancements. Automation of the modeling and proof process in these respects was crucial to being able to demonstrate formal microcode verification in the CAPS project. Nearly all of the techniques described here apply to proofs other than microcode proofs, such as machine code proofs. Furthermore most also apply to other theorem proving systems besides ACL2. What has emerged from the CAPS project and other previous projects are ad hoc approaches for tackling the fundamental challenge of complexity in code proofs using proof decomposition and automation. 2. vFaat: A Modeling and Code Verification Tool The vFaat (von Neumann Formal Annotation and Automation Tool) methodology supports the kind of proof management and automation seen in the CAPS work in a way that is theorem prover and domain language independent. 2.1 The Tool Suite The vFaat tool assists in the formal analysis of code, such as machine code or microcode. The tool mechanizes and manages standard practices employed in the code proof process. The core of the tool suite is processor independent, making it useful for reasoning about object code for a wide variety of microprocessors. It is also theorem prover independent and can be targeted towards a variety of theorem proving environments. The tool flow has four basic parts – input, annotation, automation, and output. Input is the process of extracting useful information from executable object files. Annotation is the process of linking both user-provided and machine generated information to the internal data structures. Automation is a set of implementation independent analyses that the tool set provides to the end user. Output is the process of converting the internal data structures and annotation into theorem prover proof scripts. Each of these stages is described in more detail in the following sections.

The CAPS (Collins Adaptive Processing System) is a family of Rockwell Collins proprietary processors. In a multiyear IR&D effort, Rockwell Collins adapted and developed techniques that allow for formal code verification of the microcode running on members of this family. The motivation for this research was that CAPS microprocessors are used in some of the most safety-critical products that Rockwell Collins sells, and current microprocessor verification and certification techniques are extremely laborious. On this project formal verification techniques were demonstrated on examples of actual microcode. Some of this work is publically documented [Greve00a, Wilding01a]. The code verification techniques we developed for critical microcode can be generalized to other kinds of code.

Computer systems under development are routinely modeled by simulators, and formal verification can be integrated into conventional computer system development by reasoning directly about such simulators. Simulators must be extremely fast to be usable in a real development effort. We have crafted a model for a simple processor in the logic of the ACL2 theorem prover that supports both formal analysis and efficient execution, with performance near that of a simulator written in C. We demonstrate our approach using this simple model and indicate how we applied it to our latest microprocessor.

High-speed simulation models are routinely developed during the design of complex hardware systems in order to predict performance, detect design flaws, and allow hardware/software co-design. Writing such an executable model in ACL2 brings the additional benefit of formal analysis; however, much care is required to construct an ACL2 model that is both fast and analyzable. In this chapter, we develop techniques for the construction of high-speed formally analyzable simulators in ACL2, and demonstrate their utility on a simple processor model.

We have written hardware simulators in ACL2 in order to unify highspeed simulators and formal analysis models [2, 7]. The techniques used for these simulators extend to other kinds of software, which we demonstrate in this paper by implementing a much faster version of an algorithm for graph path nding previously veri ed by J Moore using ACL2 [5]. This exercise also highlights a weakness in ACL2: the occasional need to add computational complexity to functions in order to admit them to the logic.

We describe Orpheus, our vision for a development and veriication environment for ight critical hardware devices. Orpheus provides an arrangement of translation tools that are self-checking and that integrate synthesis , high-speed simulation, and formal analysis. Implementation of the Orpheus architecture would allow tight integration of these formerly distinct activities and facilitate the use of formal analysis in ight-critical system certiication. Further, exibil-ity in the choice of design representation provided by Orpheus would support both current design practice and hardware/software code-sign. This paper describes the notion of self-checking tools, the Orpheus tool architecture, and how commercially-available tools could be used to implement such a system. 1.1 Background Certiication of ight critical systems is today a labor-intensive, manual process. Verii-cation and certiication of ight critical software and application-speciic integrated circuits (ASICs) require an almost heroic eeort of intense inspections and process documentation. The complexity of systems and devices will increase, because increases in cockpit automation and application integration ooer important safety beneets, and because astonishing improvements in digital computing technology can potentially improve performance and decrease cost. The current approach to veriication and certiication may not be adequate in the face of this increased complexity. In order to reap fully the safety beneets of these technological advances we must develop new methods for veriication and certiication of ight critical devices. Several recent developments permit a superior approach to veriication and certiication. First, ight critical ASICs can now be developed using standard hardware description languages (HDLs) because recent advances in equivalency-checking tools provide an independent check that synthesis preserves functional correctness. Second, theorem proving tools have emerged that enable mechanical formal analysis of device properties. Third, translation tools are emerging that allow the integration of mathematical analysis into the conventional fabrication/simulation-based development environment. Modern hardware devices are typically developed using one of several hardware description languages (HDLs), such as Verilog or VHDL.

This report describes the experiences of Collins Avionics & Communications and SRI International in formally specifying and verifying the microcode in a Rockwell proprietary microprocessor, the AAMP-FV, using the PVS verification system. This project built extensively on earlier experiences using PVS to verify the microcode in the AAMP5, a complex, pipelined microprocessor designed for use in avionics displays and global positioning systems. While the AAMP5 experiment demonstrated the technical feasibility of formal verification of microcode, the steep learning curve encountered left unanswered the question of whether it could be performed at reasonable cost. The AAMP-FV project was conducted to determine whether the experience gained on the AAMP5 project could be used to make formal verification of microcode cost effective for safety-critical and high volume devices.

Three technologies must be advanced to enable the migration of reconfigurable computing from research to security and safety critical applications. Those technologies are rapid dynamic reconfiguration, multiple user support, and secure application separation. All three technologies are necessary to meet the requirements of future avionics, security, and defense applications. In this paper, we present a reconfigurable computing architecture that is explicitly secure for multiple user environments and supports varying degrees of criticality and privilege. At the core of our secure reconfigurable architecture is a real-time Multiple Virtual Machine (MVM) model in a direct execution JVM microprocessor [AW97,DAG98A]. Our architecture provides hardware-enforced guarantees of resource separation. We have extended this separation guarantee to support reconfigurable logic devices. Implementations of our architecture can be verified to be safe and secure [JMR98]. We outline our formal verification techniques, which are published and can be applied to modern safety-critical and security-critical development environments [DAG98B, SPM96]. We detail an approach for formally validating that our architecture enforces separation. An architecture should be developed with open system standards to exploit future technological advances. For that reason, we employ JavaTM as a cornerstone of our design. In our vision, the same Java classfiles can be used on a computer system with or without reconfigurable computing capabilities. We use the Java software method invocation interface to execute hardware algorithms on the reconfigurable computing elements. We present these concepts and preliminary results from our system simulations [SAS98].

We describe the challenge of embedded application integration and argue that the conventional formal verification approach of proving abstract behavior is not useful in this domain. We introduce invariant performance, a formulation of task isolation useful for application integration. We demonstrate invariant performance by formalizing it in the logic of PVS for a simple yet realistic embedded system.

Formal veriication can be integrated into conventional computer system development by reasoning directly about system simula-tors. However, such simulators must be extremely fast to be usable in a real development eeort. We have developed a methodology for the construction of single-threaded processor models that support both formal analysis and eecient execution. This approach can, in principle, be used with any theorem prover. We describe an instantiation of our approach for models written in the logic of ACL2, and demonstrate its scalability by constructing an executable formal model of the Rockwell JEM1 Java microprocessor. We connrm that this model is single-threaded using a tool we have developed. This check permits the safe use of destructive state update optimizations that bring the performance level of the compiled formal model to that of a conventional simulator written in C.

Practical formal veriication of complex computer systems requires proof robustness and eeciency to protect against inevitable mistakes and system spec-iication and design changes. PVS is a theorem-proving system based on higher-order logic with which we demonstrate the kind of robust code proofs needed for veriication of realistic-sized computing systems.