This document is available on the web at http://www.cl.cam.ac.uk/~mjcg/proposals/Zurich/.
   It is best read in a browser because the hyperlinks will be live (in the postscript version they are underlined).

Programming, logic and verified systems

The scope and objectives of the meeting on Verified Software: Theories, Tools, Experiments include a discussion of the "steps on the long road towards the creation of verified software" with the aim of working towards "the achievement of the long-standing challenge of the Verifying Compiler".

Ultimately one would like to be able to construct large scale verified software written in industrial strength programming languages. However, in the short term one can accumulate insights by investigating small examples written in verification-friendly notations. This note discusses one such study: verified cryptographic systems written in logic and compiled by mechanised proof.

Can formal logic be a serious system implementation language?

It would be wonderful to have a language that realistically competes with C++, C# and Java for implementing industrial strength systems, which has a tractable semantics that supports formal verification of non-trivial programs, and a highly assured implementation guaranteeing that the semantics is correct. Alas, this is almost certainly impossible: any language with the sort of features found in existing industrial strength high-level languages is very unlikely to be capable of having either a tractable semantics or formally verified implementations.

Some fairly widely used languages do have a formal semantics, notably the denotational semantics of Scheme and the celebrated formal operational semantics of ML, but these semantics do not provide a practical basis for formal reasoning about programs in the languages. They are, however, valuable as reference documents and for proving meta-theorems (like the type preservation for ML). There are subsets of real languages with tractable semantics and assured implementations (e.g. SPARKAda), but then one has to be confident that the semantics of the subset is consistent with the semantics of the full language.

Logic is manifestly a language that has maximum tractability for formal reasoning. It is nothing like C++, C# or Java, but nevertheless maybe there are useful niches containing practical systems that can implemented directly in logic and executed in a way that guarantees correct results. Programming in logic -- logic programming -- is not a new idea, but modern theorem provers provide new possibilities.

Logic programming in a theorem prover

Theorem proving systems like ACL2, Coq, PVS, Isabelle, MetaPRL, Forte/ReFLect and HOL provide powerful synergies between computation and deduction and blur the distinction between specification and implementation.

Some of these systems allow scripting in a functional language to create bespoke interpreters for executing logic specifications. This use of a strategy or tactic language for controlling deduction contrasts with the uniform proof procedures of traditional logic and functional programming. It provides a mechanism for running "non-executable" specifications by custom deduction, and for some applications may even be used to create deployable implementations.

The verified cryptographic systems project

A collaboration between the universities of Oxford, Cambridge and Utah is working on a project that aims to program some interesting systems in logic and create implementations by theorem proving. Our goal is to create highly assured hardware and software that executes cryptographic algorithms.

Our approach is to specify cryptographic algorithms and the mathematics needed for their verification in higher order logic (specifically in the HOL Logic), and then to implement them by formal deductive compilation to ARM software and custom hardware (both also modelled in higher order logic). The ARM family of microprocessors are low power microprocessor cores with more than two billion core-based chips shipped by 2003 and now running at over 1.2 billion chips per year. The aim is to generate "golden" implementations that can be used to evaluate other implementations generated by a more conventional process.

We plan to investigate both formal verification and correct-by-construction synthesis. The semantics of instruction execution will be provided by our existing verified model of the ARM processor. We will create infrastructure, such as collections of theories and application-focused proof tools, to support the verification of cryptographic libraries for both AES and Elliptic Curve Cryptography (ECC). For synthesis, we plan to use the Total Functional Language (TFL), which is a functional programming layer on top of higher order logic and implemented in both the HOL4 and Isabelle systems. TFL enables abstract algorithms to be specified in a mixture of mathematics and programming idioms and then reasoned about using a theorem prover. We hope to compile TFL both to ARM assembler and to custom hardware (which would be interfaced to an ARM processor using standard mechanisms).

We plan to investigate implementing constructs from Cryptol in TFL as a prelude to providing verification support for algorithms expressed in it, and a high assurance synthesis route from Cryptol to ARM assembler.

As infrastructure for this work, we are starting to develop libraries of formally verified theorems in higher order logic to support the mathematics and abstract algorithms underlying ECC and all the operations necessary for RSA encryption. These libraries will build on existing theories of finite fields that have already been formalised.

The HOL4 theorem proving system

The verified cryptographic systems project is using the HOL4 system, which is the latest version of the HOL automated proof system for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking (e.g. the HolCheck BDD-based model checker with SAT-based counterexample-guided abstraction refinement).

During the last 20 years there have been several widely used versions of the HOL system:

  1. HOL88 from Cambridge;
  2. HOL90 from Calgary and Bell Labs;
  3. HOL98 from Cambridge, Glasgow and Utah.
HOL 4 is the successor to these. Its development was partly supported by the PROSPER project. HOL 4 is based on HOL98 and incorporates ideas and tools from HOL Light. The ProofPower system is another implementation of HOL. It was originally developed by ICL, but is now freely available from Lemma 1. All the HOL systems use Robin Milner's LCF approach.

Starting from scratch, it takes on average about a month to become comfortable using HOL. Many people learn the system from the free tutorial, others take courses that are offered from time to time. HOL4 is an open source project with a BSD-style licence that allows its free use in commercial products. New developers are welcome.

Conclusion

The verified cryptographic systems project is small scale, but it does aim to produce deployable verified software running on a verified Commercial Off The Shelf (COTS) processor. The approach used is not suitable for most commercial applications, but we expect the Verifying Compiler will need many different technologies, and we hope small scale studies like ours can make a little contribution to the Grand Challenge.


Mike Gordon (Cambridge), Joe Hurd (Oxford), Konrad Slind (Utah).