It's QEDs All the Way Down
Presented as part of the 2016 HCSS conference.
ABSTRACT
Traditional Formal Verification efforts have suffered from a fundamental issue, namely that the verification artifacts are only a model of the system that is to be verified. This modeling gap can be ameliorated by the development of verified translators; often, however, such engineering-artifact-to-logic-specification translators are untrusted. And even if a verified translator is created, it generally functions at the source code level, leaving us to trust the compiler/assembler/linker. The situation can be improved somewhat through the use of a verified compiler, such as the CompCert C compiler; however, for CompCert, the backend assembler and linker tools charged with producing the final executable are still trusted. Further, there is no guarantee that CompCert's C semantics match that of one's own verified translator, unless the CompCert frontend can be re-used, or unless the necessary equivalence proof is carried out.
Instead of starting with a translated model, let us imagine a scenario in which a developer crafts --- within a theorem proving environment --- an initial formal specification of the functionality that she/he intends to produce. Most major theorem provers provide some sort of source code generation path from such a starting point, but none of them provides verified translation to source code, much less to machine code. Let's assume that such a verified translation path existed, allowing a developer to create a trustworthy machine code program from a logic specification by a series of verified steps. This sort of development could be conducted according to a verified program refinement process; with sufficient automation support, such verified program refinement could be performed by developers who are not theorem proving experts. Further, by utilizing a verified execution environment, including a verified program loader as well as verified runtime components such as a garbage collector and bignum library, one could achieve both verification and validation of the machine code expression of a formal logic model, with no "trusted" elements above the CPU hardware. This may be a higher level assurance than most developments require, but for certain high-assurance security-critical and safety-critical applications, we deem the effort worthwhile.
We have been experimenting with such a verified toolchain and verified execution environment, using technologies from the CakeML project. CakeML provides mechanisms to convert HOL4 logic formulas to a subset of Standard ML, as well as a verified compiler from that ML subset to x86 machine code. We have been able to perform a verified translation of a HOL4 specification of a Deterministic Finite-state Automaton-based regular expression matcher to x86 machine code, and successfully execute that machine code on x86 hardware using the CakeML verified read-eval-print loop, exercising a large number of validation test cases. HOL4 proofs formally connect the behavior of the DFA to the set-theoretic semantics of regular expressions. We have also experimented successfully with other classic functional programs, such as Priority Queues and red/black trees.
Future work includes integrating this work with an established program refinement methodology such as Kestrel's Specware; investigating the creation of efficient machine code from functional specifications (inspired by ACL2's single-threaded object feature); and executing our verified x86 machine code programs on the detailed ACL2 formal model of the x86 currently in development at the University of Texas.
BIO
Dr. David S. Hardin has made contributions in the areas of formal methods, computer architecture for High Assurance systems, as well as real-time and embedded Java. He is currently a Principal Research Engineer in the Advanced Technology Center at Rockwell Collins, where he has served as Principal Investigator for several U.S. DoD Research and Development programs. He is the editor of the book Design and Verification of Microprocessor Systems for High-Assurance Applications (Springer 2010), and a co-author of The Real-Time Specification for Java, as well as the Java 2 Micro Edition Connected Device Configuration/Foundation Profile standards. He is author or co-author of more than 40 peer-reviewed publications, and is a co-inventor on eleven U.S. patents. In 1999, Dr. Hardin co-founded aJile Systems, a startup company focused on real-time and embedded Java technology, and served as aJile's Chief Technical Officer from 1999 to 2003. Dr. Hardin was selected as a Rockwell Engineer of the Year for 1997 for his contributions to the development of the world's first Java microprocessor. His academic career includes BSEE and MSEE degrees from the University of Kentucky, and a Ph.D. in Electrical and Computer Engineering from Kansas State University, in 1989. Dr. Hardin is a proud native of the Commonwealth of Kentucky, and is a Kentucky Colonel.