Theorem Proving in Higher Order Logics

Traditional security protocols are mainly concerned with key establishment and principal authentication and rely on predistributed keys and properties of cryptographic operators. In contrast, new application areas are emerging that establish and rely on properties of the physical world. Examples include protocols for secure localization, distance bounding, and device pairing.

We present a formal model that extends inductive, trace-based approaches in two directions. First, we refine the standard Dolev-Yao model to account for network topology, transmission delays, and node positions. This results in a distributed intruder with restricted, but more realistic, communication capabilities. Second, we develop an abstract message theory that formalizes protocol-independent facts about messages, which hold for all instances. When verifying protocols, we instantiate the abstract message theory, modeling the properties of the cryptographic operators under consideration. We have formalized this model in Isabelle/HOL and used it to verify distance bounding protocols where the concrete message theory includes exclusive-or.

VCC is an industrial-strength verification environment for low-level concurrent system code written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove the correctness of these annotations. It includes tools for monitoring proof attempts and constructing partial counterexample executions for failed proofs. This paper motivates VCC, describes our verification methodology, describes the architecture of VCC, and reports on our experience using VCC to verify the Microsoft Hyper-V hypervisor.

One sometimes reads in a mathematical proof that a certain assumption can be made ‘without loss of generality’ (WLOG). In other words, it is claimed that considering what first appears only a special case does nevertheless suffice to prove the general result. Typically the intuitive justification for this is that one can exploit symmetry in the problem. We examine how to formalize such ‘WLOG’ arguments in a mechanical theorem prover. Geometric reasoning is particularly rich in examples and we pay special attention to this area.

HOL Light is an interactive proof assistant for classical higher-order logic, intended as a clean and simplified version of Mike Gordon’s original HOL system. Theorem provers in this family use a version of ML as both the implementation and interaction language; in HOL Light’s case this is Objective CAML (OCaml). Thanks to its adherence to the so-called ‘LCF approach’, the system can be extended with new inference rules without compromising soundness. While retaining this reliability and programmability from earlier HOL systems, HOL Light is distinguished by its clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof tools and has been applied to some non-trivial tasks in the formalization of mathematics and industrial formal verification.

Mizar

is the name of a formal language derived from informal mathematics and computer software that enables proof-checking of texts written in that language. The system has been actively developed since 1970s, growing into a popular proof assistant accompanied with a huge repository of formalized mathematical knowledge. In this short overview, we give an outline of the key features of the

Mizar

language, the ideas and theory behind the system, its main applications, and current development.

We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-Löf’s intuitionistic type theory but extends it with numerous programming language features. It supports a wide range of inductive data types, including inductive families and inductive-recursive types, with associated flexible pattern-matching. Unlike other proof assistants, Agda is not tactic-based. Instead it has an Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.

Logical framework

research is based on the philosophical point of view that it should be possible to capture mathematical concepts such as proofs, logics, and meaning in a formal system — directly, adequately (in the sense that there are no spurious or exotic witnesses), and without having to commit to a particular logical theory. Instead of working with one general purpose representation language, we design special purpose logical frameworks for capturing reoccurring concepts for special domains, such as, for example, variable renaming, substitution application, and resource management for programming language theory. Most logical frameworks are based on constructive type theories, such as Isabelle (on the simply-typed

λ

-calculus), LF [HHP93] (on the dependently typed

λ

-calculus), and LLF (on a linearly typed

λ

-calculus). The representational strength of the logical framework stems from the choice of definitional equality on terms. For example,

α

-conversion models the tacit renaming of variables,

β

-contraction models substitution application, and

η

-expansion guarantees the adequacy of encodings.

Several mechanisms such as Canonical Structures [14], Type Classes [13,16], or Pullbacks [10] have been recently introduced with the aim to improve the power and flexibility of the type inference algorithm for interactive theorem provers. We claim that all these mechanisms are particular instances of a simpler and more general technique, just consisting in providing suitable hints to the unification procedure underlying type inference. This allows a simple, modular and not intrusive implementation of all the above mentioned techniques, opening at the same time innovative and unexpected perspectives on its possible applications.

Psi-calculi are extensions of the pi-calculus, accommodating arbitrary nominal datatypes to represent not only data but also communication channels, assertions and conditions, giving it an expressive power beyond the applied pi-calculus and the concurrent constraint pi-calculus.

We have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature is that the framework needs to treat binding sequences, as opposed to single binders, in an efficient way. While different methods for formalising single binder calculi have been proposed over the last decades, representations for such binding sequences are not very well explored.

The main effort in the formalisation is to keep the machine checked proofs as close to their pen-and-paper counterparts as possible. We discuss two approaches to reasoning about binding sequences along with their strengths and weaknesses. We also cover custom induction rules to remove the bulk of manual alpha-conversions.

We present a Coq formalization of constructive

ω

-cpos (extending earlier work by Paulin-Mohring) up to and including the inverse-limit construction of solutions to mixed-variance recursive domain equations, and the existence of invariant relations on those solutions. We then define operational and denotational semantics for both a simply-typed CBV language with recursion and an untyped CBV language, and establish soundness and adequacy results in each case.

Inductively defined predicates are frequently used in formal specifications. Using the theorem prover

Isabelle

, we describe an approach to turn a class of systems of inductively defined predicates into a system of equations using data flow analysis; the translation is carried out

inside

the logic and resulting equations can be turned into functional program code in

SML

,

OCaml

or

Haskell

using the existing code generator of

Isabelle

. Thus we extend the scope of code generation in

Isabelle

from functional to functional-logic programs while leaving the trusted foundations of code generation itself intact.

This paper presents a formalization of a library for automata on bit strings in the theorem prover Isabelle/HOL. It forms the basis of a reflection-based decision procedure for Presburger arithmetic, which is efficiently executable thanks to Isabelle’s code generator. With this work, we therefore provide a mechanized proof of the well-known connection between logic and automata theory.

We consider the EFO fragment of simple type theory, which restricts quantification and equality to base types but retains lambda abstractions and higher-order variables. We show that this fragment enjoys the characteristic properties of first-order logic: complete proof systems, compactness, and countable models. We obtain these results with an analytic tableau system and a concomitant model existence lemma. All results are with respect to standard models. The tableau system is well-suited for proof search and yields decision procedures for substantial fragments of EFO.

We consider a formalisation of a notion of observer (or intruder) theories, commonly used in symbolic analysis of security protocols. An observer theory describes the knowledge and capabilities of an observer, and can be given a formal account using deductive systems, such as those used in various “environment-sensitive” bisimulation for process calculi, e.g., the spi-calculus. Two notions are critical to the correctness of such formalisations and the effectiveness of symbolic techniques based on them: decidability of message deduction by the observer and consistency of a given observer theory. We consider a formalisation, in Isabelle/HOL, of both notions based on an encoding of observer theories as pairs of symbolic traces. This encoding has recently been used in a theory of open bisimulation for the spi-calculus. We machine-checked some important properties, including decidability of observer deduction and consistency, and some key steps which are crucial to the automation of open bisimulation checking for the spi-calculus, and highlight some novelty in our Isabelle/HOL formalisations of decidability proofs.

The paper presents the development, by using the proof assistant Isabelle/HOL, of a compiler back-end translating from a functional source language to the bytecode language of an abstract machine. The Haskell code of the compiler is extracted from the Isabelle/HOL specification and this tool is also used for proving the correctness of the implementation. The main correctness theorem not only ensures functional semantics preservation but also resource consumption preservation: the heap and stacks figures predicted by the semantics are confirmed in the translation to the abstract machine.

The language and the development belong to a wider Proof Carrying Code framework in which formal compiler-generated certificates about memory consumption are sought for.

A fundamental issue in multithreaded programming is detecting

data races

. A program is said to be well synchronised if it does not contain data races w.r.t. an interleaving semantics. Formally ensuring this property is central, because the

java

Memory Model then guarantees that one can safely reason on the interleaved semantics of the program. In this work we formalise in the

coq

proof assistant a

java

bytecode data race analyser based on the conditional must-not alias analysis of Naik and Aiken. The formalisation includes a context-sensitive points-to analysis and an instrumented semantics that counts method calls and loop iterations. Our

java

-like language handles objects, virtual method calls, thread spawning and lock and unlock operations for threads synchronisation.

Optical systems are becoming increasingly important as they tend to resolve many bottlenecks in the present age communications and electronics. Some common examples include their usage to meet high capacity link demands in communication systems and to overcome the performance limitations of metal interconnect in silicon chips. Though, the inability to efficiently analyze optical systems using traditional analysis approaches, due to the continuous nature of optics, somewhat limits their application, specially in safety-critical applications. In order to overcome this limitation, we propose to formally analyze optical systems using a higher-order-logic theorem prover (HOL). As a first step in this endeavor, we formally analyze eigenvalues for planar optical waveguides, which are some of the most fundamental components in optical devices. For the formalization, we have utilized the mathematical concepts of differentiation of piecewise functions and one-sided limits of functions. In order to illustrate the practical effectiveness of our results, we present the formal analysis of a planar asymmetric waveguide.

A new logic is posited for the widely used HOL theorem prover, as an extension of the existing higher order logic of the HOL4 system. The logic is extended to three levels, adding kinds to the existing levels of types and terms. New types include type operator variables and universal types as in System

F

. Impredicativity is avoided through the stratification of types by ranks according to the depth of universal types. The new system, called

HOL-Omega

or

HOL

ω

, is a merging of HOL4, HOL2P[11], and major aspects of System

F

ω

from chapter 30 of [10]. This document presents the abstract syntax and semantics for the kinds, types, and terms of the logic, as well as the new fundamental axioms and rules of inference. As the new logic is constructed according to the design principles of the LCF approach, the soundness of the entire system depends critically and solely on the soundness of this core.

Existing theorem prover tools do not adequately support reasoning about general recursive datatypes. Better support for such datatypes would facilitate reasoning about a wide variety of real-world programs, including those written in continuation-passing style, that are beyond the scope of current tools.

This paper introduces a new formalization of a universal domain that is suitable for modeling general recursive datatypes. The construction is purely definitional, introducing no new axioms. Defining recursive types in terms of this universal domain will allow a theorem prover to derive strong reasoning principles, with soundness ensured by construction.

This paper presents a separation-logic framework for reasoning about low-level C code in the presence of virtual memory. We describe our abstract, generic Isabelle/HOL framework for reasoning about virtual memory in separation logic, and we instantiate this framework to a precise, formal model of ARMv6 page tables. The logic supports the usual separation logic rules, including the frame rule, and extends separation logic with additional basic predicates for mapping virtual to physical addresses. We build on earlier work to parse potentially type-unsafe, system-level C code directly into Isabelle/HOL and further instantiate the separation logic framework to C.

In a game from game theory, a Nash equilibrium (NE) is a combination of one strategy per agent such that no agent can increase its payoff by unilaterally changing its strategy. Kuhn proved that all (tree-like) sequential games have NE. Osborne and Rubinstein abstracted over these games and Kuhn’s result: they proved a sufficient condition on agents’

preferences

for all games to have NE. This paper proves a

necessary and sufficient condition

, thus accounting for the game-theoretic frameworks that were left aside.

The proof is formalised

using Coq, and contrary to usual game theory it adopts an inductive approach to trees for definitions and proofs. By rephrasing a few game-theoretic concepts, by ignoring useless ones, and by characterising the proof-theoretic strength of Kuhn’s/Osborne and Rubinstein’s development, this paper also

clarifies

sequential game theory. The introduction sketches these clarifications, while the rest of the paper details the formalisation.

FinFuns are total functions that are constant except for a finite set of points, i.e. a generalisation of finite maps. We formalise them in Isabelle/HOL and present how to safely set up Isabelle’s code generator such that operations like equality testing and quantification on FinFuns become executable. On the code output level, FinFuns are explicitly represented by constant functions and pointwise updates, similarly to associative lists. Inside the logic, they behave like ordinary functions with extensionality. Via the update/constant pattern, a recursion combinator and an induction rule for FinFuns allow for defining and reasoning about operators on FinFuns that directly become executable. We apply the approach to an executable formalisation of sets and use it for the semantics for a subset of concurrent Java.

This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the

Coq

system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom. Finally, we present two applications of our proof techniques: a key lemma for characterising the discrete logarithm, and a matrix decomposition problem.

We present a comprehensive set of tactics that make it practical to use separation logic in a proof assistant. These tactics enable the verification of partial correctness properties of complex pointer-intensive programs. Our goal is to make separation logic as easy to use as the standard logic of a proof assistant. We have developed tactics for the simplification, rearranging, splitting, matching and rewriting of separation logic assertions as well as the discharging of a program verification condition using a separation logic description of the machine state. We have implemented our tactics in the Coq proof assistant, applying them to a deep embedding of Cminor, a C-like intermediate language used by Leroy’s verified CompCert compiler. We have used our tactics to verify the safety and completeness of a Cheney copying garbage collector written in Cminor. Our ideas should be applicable to other substructural logics and imperative languages.

This paper reports on a case study, which we believe is the first to produce a formally verified end-to-end implementation of a functional programming language running on commercial processors. Interpreters for the core of McCarthy’s LISP 1.5 were implemented in ARM, x86 and PowerPC machine code, and proved to correctly parse, evaluate and print LISP s-expressions. The proof of evaluation required working on top of verified implementations of memory allocation and garbage collection. All proofs are mechanised in the HOL4 theorem prover.

We present four coinductive operational semantics for the While language accounting for both terminating and non-terminating program runs: big-step and small-step relational semantics and big-step and small-step functional semantics. The semantics employ traces (possibly infinite sequences of states) to record the states that program runs go through. The relational semantics relate statement-state pairs to traces, whereas the functional semantics return traces for statement-state pairs. All four semantics are equivalent. We formalize the semantics and their equivalence proofs in the constructive setting of Coq.

Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prime targets for mechanized formalization. In previous work we produced a rigorous

x86-CC

model, formalizing the Intel and AMD architecture specifications of the time, but those turned out to be unsound with respect to actual hardware, as well as arguably too weak to program above. We discuss these issues and present a new

x86-TSO

model that suffers from neither problem, formalized in HOL4. We believe it is sound with respect to real processors, reflects better the vendor’s intentions, and is also better suited for programming. We give two equivalent definitions of x86-TSO: an intuitive operational model based on local write buffers, and an axiomatic total store ordering model, similar to that of the SPARCv8. Both are adapted to handle x86-specific features. We have implemented the axiomatic model in our

memevents

tool, which calculates the set of all valid executions of test programs, and, for greater confidence, verify the witnesses of such executions directly, with code extracted from a third, more algorithmic, equivalent version of the definition.

We are interested in the verification of Newton’s method. We use a formalization of the convergence and stability of the method done with the axiomatic real numbers of Coq’s Standard Library in order to validate the computation with Newton’s method done with a library of exact real arithmetic based on co-inductive streams. The contribution of this work is twofold. Firstly, based on Newton’s method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Secondly, we prove that rounding at each step in Newton’s method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding turns out to be much more efficient.

We present the implementation in Isabelle/HOL of a translation of LTL formulae into Büchi automata. In automaton-based model checking, systems are modelled as transition systems, and correctness properties stated as formulae of temporal logic are translated into corresponding automata. An LTL formula is represented by a (generalised) Büchi automaton that accepts precisely those behaviours allowed by the formula. The model checking problem is then reduced to checking language inclusion between the two automata. The automaton construction is thus an essential component of an LTL model checking algorithm. We implemented a standard translation algorithm due to Gerth

et al

. The correctness and termination of our implementation are proven in Isabelle/HOL, and executable code is generated using the Isabelle/HOL code generator.

This pearl examines how to verify functional programs written using the state monad. It uses Coq’s Program framework to provide strong specifications for the standard operations that the state monad supports, such as return and bind. By exploiting the monadic structure of such programs during the verification process, it becomes easier to prove that they satisfy their specification.

There are many automatic tools to prove termination of term rewrite systems, nowadays. Most of these tools use a combination of many complex termination criteria. Hence generated proofs may be of tremendous size, which makes it very tedious (if not impossible) for humans to check those proofs for correctness.

In this paper we use the theorem prover Isabelle/HOL to automatically certify termination proofs. To this end, we first formalized the required theory of term rewriting including three major termination criteria: dependency pairs, dependency graphs, and reduction pairs. Second, for each of these techniques we developed an executable check which guarantees the correct application of that technique as it occurs in the generated proofs. Moreover, if a proof is not accepted, a readable error message is displayed. Finally, we used Isabelle’s code generation facilities to generate a highly efficient and certified Haskell program,

CeTA

, which can be used to certify termination proofs without even having Isabelle installed.

In this paper a general framework for separation logic inside the HOL theorem prover is presented. This framework is based on Abstract Separation Logic. It contains a model of an abstract, imperative programming language as well as an abstract specification logic for this language. While the formalisation mainly follows the original definition of Abstract Separation Logic, it contains some additional features. Most noticeably is added support for procedures.

As a case study, the framework is instantiated to build a tool that is able to parse Smallfoot specifications and verify most of them completely automatically. In contrast to Smallfoot this instantiation can handle the content of data-structures as well as their shape. This enables it to verify fully functional specifications. Some noteworthy examples that have been verified are parallel mergesort and an interactive filter-function for single linked lists.

This paper describes an extension of Paulson’s inductive protocol verification approach for liveness reasoning. The extension requires no change of the system model underlying the original inductive approach. Therefore, all the advantages, which makes Paulson’s approach successful for safety reasoning are kept, while liveness reasoning becomes possible. To simplify liveness reasoning, a new fairness notion, named

Parametric Fairness

is used instead of the standard ones. A probabilistic model is established to support this new fairness notion. Experiments with small examples as well as real world communication protocols confirm the practicality of the extension. All the work has been formalized with Isabelle/HOL using Isar.

This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.