Type-driven Verification of Communicating Systems

It is considered a fact of life that computer software routinely fails. Often, this is merely inconvenient. When a PC, tablet or mobile phone crashes, we can restart it, perhaps losing only a small amount of work. On the other hand, errors in systems software or in network or security infrastructure can be disastrous. Recent high profile security vulnerabilities such as the "Heartbleed" bug show that even well tested and widely used software can contain serious and undetected flaws.

This project forms the initial part of an ambitious long term vision of a platform for full-stack verified software development, accessible by
both programming practitioners and researchers. We will use a type-driven approach to software verification, using the dependently typed programming language Idris.

The promise of dependently typed languages is that we can, in principle, guarantee important functional properties of software (such as preservation of size and ordering properties of data) and extra-functional properties such as resource safety (for example, that a protocol is followed accurately). However, proving such properties in general remains impractical for typical application developers, due to the difficulty of constructing proofs, the difficulty of reading and maintaining software due to proof details interfering with the details of an algorithm, and the lack of robustness and efficiency in even state of the art implementations of dependently typed languages.

Idris aims to address these problems, having been built specifically with the goal of generating good quality executable code which can interroperate with existing systems. Furthermore, it supports language constructs for building "Domain Specific Languages" (DSLs). In this project, we will further develop Idris, focussing on robustness and efficiency, and show how its support for DSL construction and type-level programming allow us to develop secure communication protocol implementations, described as a type-level DSL and verified by type checking.

In particular, we will construct verified implementations of Diffie-Hellman key exchange, and the Needham-Schroeder-Lowe protocol, and use these to implement a demonstrator application. This application (a networked chat system) will support secure communication (up to the guarantees given in the protocols), be efficient (no overhead due to proof obligations) and be able to communicate with alternative implementations in other languages.

In the course of the project, we will make significant advances in the state of the art of dependently typed programming, improving the available tools and developing new libraries and programming idioms. As well as benefitting academic researchers in the field of software verification, it will benefit the wider community of application developers and the general public.

Ultimately, the public at large will benefit from enhanced security and verification in communications technology. By providing enhanced tools for guaranteeing confidentiality and integrity of data, we greatly reduce the risk of leaking private data, and greatly reduce the costs of patching affected systems. This project will itself contribute to a longer term vision of fully verified systems infrastructure, laying foundations for secure protocol implementation and developing robust and efficient tools to support these implementations.

We are collaborating with companies who may make use of the results of this project, in particular Erlang Solutions and Galois, Inc. Erlang Solutions provide scalable distributed systems using Erlang's built-in support for concurrent and distributed systems. This project will ultimately lead to tools for adding verification and security as well as scalability. Galois Inc, based in Portland, Oregon, use functional programming and domain specific language based technology to build tools for guaranteed confidentiality, integrity and availability of systems. They will benefit from enhanced domain specific language technology to support machine checkable proofs of correctness of systems infrastructure.

The project will involve further development of the Idris programming language (http://idris-lang.org). As with all code released as part of the Idris system so far, everything produced during the project will be released under an Open Source licence, and made available via GitHub (http://www.github.com/) and the project web site.