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.
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.
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.
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.
During the last 20 years there have been several widely used versions of the HOL system:
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.