ACL on Tuesday, August 15th

Welcome and Opening Remarks (08:50‑09:00)
Location: Suite 3102

08:50‑09:00

Pete Manolios and Matt Wilding

Session 1 (09:00‑10:00)
Chair: J Strother Moore
Location: Suite 3102

09:00‑09:30

Lee Pike (Galois Connections) Mark Shields (Microsoft) John Mattews (Galois Connections) A Verifying Core for a Cryptographic Language Compiler A verifying compiler is one that emits both object code and a proof of correspondence between object and source code. We report the use of ACL2 in building a verifying compiler for mCryptol, a stream-based language for encryption algorithm specification that targets Rockwell Collins' AAMP7 microprocessor (and is designed to compile efficiently to hardware, too). This paper reports on our success in verifying the ``core'' transformations of the compiler -- those transformations over the sub-language of mCryptol that begin after ``higher-order'' aspects of the language are compiled away, and finish just before hardware or software specific transformations are exercised. The core transformations are responsible for aggressive optimizations. We have written an ACL2 macro that automatically generates both the correspondence theorems and their proofs. The compiler also supplies measure functions that ACL2 uses to automatically prove termination of mCryptol programs, including programs with mutually-recursive cliques of streams. Our verifying compiler has proved the correctness of its core transformations for multiple algorithms, including TEA, RC6, and AES. Finally, we describe an ACL2 book of primitive operations for the general specification and verification of encryption algorithms.

09:30‑10:00

David Hardin (Rockwell Collins) Eric Smith (Stanford University) William Young (University of Texas at Austin) A Robust Machine Code Proof Framework for Highly Secure Applications Security-critical applications at the highest Evaluation Assurance Level (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 (SHADE) program, we have produced an executable formal model of the Rockwell Collins AAMP7G microprocessor at the instruction set level in ACL2 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 an NSA 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 through the use of the method of “compositional cutpoints”, a technique pioneered on the SHADE program that requires neither traditional clock functions nor a Verification Condition Generator (VCG). In this paper, we will summarize the AAMP7G architecture, detail the development of the ACL2 model of the processor, describe our machine code proof framework, and discuss the use of ACL2 in the SHADE program.

Break (10:00‑10:30)

Session 2 (10:30‑11:45)
Chair: Jose Luis Ruiz-Reina
Location: Suite 3102

10:30‑11:00	John Cowles (University of Wyoming) Ruben Gamboa (University of Wyoming) Unique Factorization in ACL2: Euclidean Domains ACL2 is used to systematically study domains whose elements can be "uniquely" factored into products of "irreducible" elements. The best known examples of such domains are the positive integers, which can be factored into products of primes, and univariate polynomials with rational coefficients, which can be factored into products of irreducible polynomials. There are many other such domains. Euclidean domains are an algebraic abstraction, of both the positive integers and the rational polynomials, in which the usual proofs of unique factorization, for both the integers and the polynomials, can be generalized.
11:00‑11:30	David Greve (Rockwell Collins) Generalized Congruences 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 equivalance 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. Perhaps the most significant limitation is that equivalence relations must be binary, which precludes a most natural application of congruences: their use in reasoning about modular arithmetic. We have developed an ACL2 library (nary) that overcomes this limitation and supports generalized n-ary congruence-based rewriting on a stock ACL2 system. The library provides a means of expressing and utilizing generalized n-ary congruences with a high degree of automation. We demonstrate its utility by handily proving several "hard" theorems in modular arithmetic.
11:30‑11:45	Sol Swords (University of Texas at Austin) William R. Cook (University of Texas at Austin) Soundness of the Simply Typed Lambda Calculus in ACL2 To make it practical to mechanize proofs in programming language metatheory, several capabilities are required of the theorem proving framework. One must be able to represent and efficiently reason about complex recursively-defined expressions, define arbitrary induction schemes including mutual inductions over several objects and inductions over derivations, and reason about variable bindings with minimal overhead. We introduce a method for performing these proofs in ACL2, including a macro which automates the process of defining functions and theorems to facilitate reasoning about recursive data types. To illustrate this method, we present a proof in ACL2 of the soundness of the simply typed lambda-calculus.
11:45‑12:30	"Matt Kaufmann, J Strother Moore An Overview of Recent and Upcoming ACL2 Developments

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:15)
Chair: Matt Wilding
Location: Willow A

14:00‑14:30	Mike Gordon (University of Cambridge) Warren A. Hunt, Jr. (University of Texas at Austin) Matt Kaufmann (University of Texas) James Reynolds (Cambridge University) An Embedding of the ACL2 Logic in HOL We describe an embedding of the ACL2 logic into higher-order logic. An implementation of this embedding allows ACL2 to be used as an oracle for higher-order logic provers.
14:30‑15:00	Julien Schmaltz (Saarland University) Dominique Borrione (Joseph Fourier University, TIMA Lab.) Towards a Formal Theory of On Chip Communications in the ACL2 Logic GeNoC is a first step towards a formal theory of communication networks. It is expressed in a general mathematical notation with many quantifiers, in particular quantification over functions. We present here its expression in the first order quantifier free logic of the ACL2 theorem prover. We describe our systematic approach to cast it into ACL2, especially how we use the encapsulation principle to obtain a systematic methodology to specify and validate on chip communications architectures. We summarize the different instances of GeNoC developed so far in ACL2, some come from industrial designs. We illustrate our approach on an XY routing algorithm.
15:00‑15:15	Jared Davis (University of Texas at Austin) Memories: Array-like Records for ACL2 We have written a new records library for modelling fixed-size arrays and linear memories. Our implementation provides fixnum-optimized O(log2 n) reads and writes from addresses 0, 1, ..., n - 1. Space is not allocated until locations are used, so large address spaces can be represented. We do not use single-threaded objects or ACL2 arrays, which frees the user from syntactic restrictions and slow-array warnings. Finally, we can prove the same hypothesis-free rewrite rules found in misc/records for efficient rewriting during theorem proving.
15:15‑15:30	Matt Kaufmann, J Strother Moore ACM Software System Award Remarks

Break (15:30‑16:00)

Invited Talk (16:00‑16:45)
Location: Willow A

16:00‑16:45

Tony Hoare (Microsoft Research) The Ideal of Verified Software

Session 4: Panel: Grand Challenge Problems for the ACL2 Community (16:45‑18:15)
Chair: Pete Manolios
Location: Willow A

16:45‑18:15

David Hardin, Tony Hoare, Gerard Holzmann, J Strother Moore, ... Panel

Workshop Dinner (19:00‑21:30)
Location: outside hotel