Many verification and validation activities involve reasoning about constraints over complex, hierarchical data types. For example, distributed protocols are often defined using state machines that govern the behavior of processes communicating with messages which are hierarchical data types with state-dependent constraints and dependencies between component fields. Fuzzing, analyzing and evaluating implementations of such protocols requires solving complex queries that pose challenges to current SMT solvers. Generating fields that satisfy type constraints is one of the challenges and this can be tackled using enumerative data types: types that come with an enumerator, an efficiently computable function from natural numbers to elements of the type. Enumerative data types were introduced in ACL2s as a key component of counterexample generation, but they do not handle constraints such as dependencies between types. We extend enumerative data types with constraints and show how this extension enables applications such as hardware-in-the-loop fuzzing of complex distributed protocols.

The decentralized perimeter surveillance system (DPSS) seeks to provide a decentralized protocol for evenly distributing surveillance of a perimeter over time across an ensemble of unmanned aerial vehicles (UAVs) whose members may communicate only when in close proximity to each other. The protocol must also converge to an even distribution of the perimeter in bounded time. Two versions of the DPSS protocol presented in the original paper seem to converge in bounded time but only informal proofs and arguments are given. A later application of model checking to these protocols found an error in one of the key lemmas, invalidating the informal proof for one and casting doubt on the other. Therefore, a new hand proof of the convergence time for the simpler version of the DPSS protocol or algorithm, Algorithm A or DPSS-A, was developed by Jeremy Avigad and Floris van Doorn. This paper describes a mechanization of that hand proof in the logic of ACL2 and discusses three specific ACL2 utilities that proved useful for expressing and reasoning about the DPSS model.

Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification, while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed framework unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems.

We are developing a model-based fuzzing framework that employs mathematical models of system behavior to guide the fuzzing process. Whereas traditional fuzzing frameworks generate tests randomly, a model-based framework can deduce tests from a behavioral model using a constraint solver. Because the state space being explored by the fuzzer is often large, the rapid generation of test vectors is crucial. The need to generate tests quickly, however, is antithetical to the use of a constraint solver. Our solution to this problem is to use the constraint solver to generate an initial solution, to generalize that solution relative to the system model, and then to perform rapid, repeated, randomized sampling of the generalized solution space to generate fuzzing tests. Crucial to the success of this endeavor is a generalization procedure with reasonable size and performance costs that produces generalized solution spaces that can be sampled efficiently. This paper describes a generalization technique for logical formulae expressed in terms of Boolean combinations of linear constraints that meets the unique performance requirements of model-based fuzzing. The technique represents generalizations using trapezoidal solution sets consisting of ordered, hierarchical conjunctions of linear constraints that are more expressive than simple intervals but are more efficient to manipulate and sample than generic polytopes. Supporting materials contain an ACL2 proof that verifies the correctness of a low-level implementation of the generalization algorithm against a specification of generalization correctness. Finally a post-processing procedure is described that results in a restricted trapezoidal solution that can be sampled (solved) rapidly and efficiently without backtracking, even for integer domains. While informal correctness arguments are provided, a formal proof of the correctness of the restriction algorithm remains as future work.

The Static IMPerative AnaLyzer (SIMPAL) is a tool for performing compositional reasoning over software programs that utilize preexisting software components. SIMPAL features a specification language, called Limp, for modeling programs that utilize preexisting components. Limp is an extension of the Lustre synchronous data flow language. Limp extends Lustre by introducing control flow elements, global variables, and syntax specifying preconditions, postconditions, and global variable interactions of preexisting components. SIMPAL translates Limp programs to an equivalent Lustre representation which can be passed to the JKind model checking tool to perform assume-guarantee reasoning, reachability, and viability analyses. The feedback from these analyses can be used to refine the program to ensure the software functions as intended.

In our current work a library of formally verified software components is to be created, and assembled, using the Low-Level Virtual Machine (LLVM) intermediate form, into subsystems whose top-level assurance relies on the assurance of the individual components. We have thus undertaken a project to build a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem prover. Our translator produces executable ACL2 formal models, allowing us to both prove theorems about the translated models as well as validate those models by testing. The resulting models can be translated and certified without user intervention, even for code with loops, thanks to the use of the def : : ung macro which allows us to defer the question of termination. Initial measurements of concrete execution for translated LLVM functions indicate that performance is nearly 2.4 million LLVM instructions per second on a typical laptop computer. In this paper we overview the translation process and illustrate the translator's capabilities by way of a concrete example, including both a functional correctness theorem as well as a validation test for that example.

Embedded hypervisors allow integration of a mixture of legacy and modern applications onto a single computing platform, thus reducing size, weight, power, and cost (SWaP-C). DornerWorks is developing extensions to the open source Xen hypervisor that will meet DO-178C Level A requirements for safety and high robustness requirements based on Common Criteria Evaluation Assurance Level (EAL) 6+ for security. Our extensions provide compliance with the ARINC 653 standard, including time and space partitioning and refine the idea of I/O partitioning. Our partitioning of I/O provides deterministic bandwidth allocation to guest domains. To meet security requirements we apply modern formal analysis techniques to our design. A distinctive aspect of our hypervisor is our use of permissive licensing based on open source with meticulous configuration management. We believe that the transparency and availability offered by a permissive license and an open architecture coupled with rigorous certification artifacts for both safety and security establishes a compelling alternative for partitioning of software in safety and security-critical systems.

We describe an ACL2 package for defining partial recursive functions that also supports efficient execution. While packages for defining partial recursive functions already exist for other theorem provers, they often require inductive definitions or recursion operators which are not available in ACL2 and they provide little, if any, support for executing the resulting definitions. We use step-indexing as the underlying implementation technology, enabling the definitions to be carried out in first order logic. We also show how recent enhancements to ACL2's guard feature can be used to enable the efficient execution of partial recursive functions.

Understanding and analyzing information flow is crucial in the evaluation of security critical software systems. Data Flow Logic (DFL) is a domain specific language under development at Rockwell Collins for use in specifying and verifying dynamic information flow properties of such systems. The language employs C source code annotations to enable concise, consumable, abstract specifications of crucial information flow properties. A static analysis engine is also being developed to allow substantial portions of such specifications to be verified automatically. This paper highlights the motivation, methodology and status of the DFL tool suite.

Information flow modeling describes how information can be transferred between different locations within a software and/or hardware system. In this chapter, we define a notion of information flow based on traces that is useful for describing flow relations for synchronous dataflow languages such as SimulinkⓇ (The Mathworks, Inc.) and SCADE™ (Esterel Technologies, Inc.) that are often used for hardware/software codesign. We then define an automated method for analyzing information flow properties of Simulink models using model checking. This method is based on creating a flow model that tracks information flow throughout the model. Often, information flow properties are defined in terms of some form of noninterference, which states informally that objects in one security domain cannot perceive the actions of objects within another domain. We demonstrate that this method preserves the GWV functional notion of noninterference. We then describe how this proof relates to the GWV theorem and provide some insight into the relationship of the flow model and the flow graphs used in GWVr1. Finally, we demonstrate our analysis technique by analyzing the architecture of the Turnstile high-assurance cross-domain guard platform using our Gryphon translation framework and the Prover™ model checker.

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.

Support for congruence-based rewriting is built into ACL2. This capability allows ACL2 to treat certain predicate relations "just like equality" under appropriate conditions and allows specific theorems involving those equivalence relations to be used as rewrite rules to guide the simplification process. Although this has proven to be an extremely powerful capability, it comes with limitations. One significant limitation is that equivalence relations cannot be parameterized. This precludes one very natural application of congruences: their use in reasoning about arbitrary modulus arithmetic. We have developed a technique for emulating parameterized congruence-based rewriting on a stock ACL2 system using binding hypotheses and bind-free. We have also developed a library (nary) that provides a means of expressing and utilizing such congruences with a high degree of automation. We demonstrate the application of this library to problems in modular arithmetic and other similar domains.

this paper a security property that we believe has boththese desired properties. We are currently demonstrating that the securitycan be proved byshowing that it holds of a system under development. Thegoal of this paper is to show that the security policy can be used, whichwe demonstrate two ways. First, we introduce some theorems similar towhat others have used to describe a separation kernel and prove that ourspecication implies theirs. Second, we formalize an example applicationthat ...

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].

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.

Symbolic simulation is the simulation of the execution of a computer system on an incompletely defined, or symbolic, state. This process results in a set of expressions that define the final machine state symbolically in terms of the initial machine state. We describe our use of symbolic simulation in conjunction with the development of the JEM1, the world's first Java processor. We demonstrate that symbolic simulation can be used to detect microcode design errors and that it can be integrated into our current design process.