Type-driven Verification of Communicating Systems

计算机软件经常会出现故障，这被认为是生活中的一个事实。通常，这只是不方便。当个人电脑、平板电脑或手机崩溃时，我们可以重新启动它，也许只会损失一小部分工作。另一方面，系统软件或网络或安全基础设施中的错误可能是灾难性的。最近备受关注的安全漏洞，如“心脏出血”漏洞表明，即使是经过良好测试和广泛使用的软件也可能包含严重且未被发现的缺陷。这个项目形成了一个雄心勃勃的长期愿景的初始部分，即一个全栈验证软件开发平台，编程从业者和研究人员都可以访问。我们将使用类型驱动的方法来进行软件验证，使用依赖类型的编程语言Idris。依赖类型语言的承诺是，原则上，我们可以保证软件的重要功能属性（例如保存数据的大小和排序属性）和额外的功能属性，例如资源安全（例如，准确地遵循协议）。然而，对于典型的应用程序开发人员来说，证明这些属性通常仍然是不切实际的，这是由于构造证明的困难，由于证明细节干扰算法细节而导致阅读和维护软件的困难，以及即使在依赖类型语言的最先进实现中也缺乏鲁棒性和效率。Idris旨在解决这些问题，它的构建目标是生成高质量的可执行代码，这些代码可以与现有系统进行交互。此外，它支持用于构建“领域特定语言”（dsl）的语言构造。在本项目中，我们将进一步开发Idris，重点关注鲁棒性和效率，并展示其对DSL构造和类型级编程的支持如何允许我们开发安全通信协议实现，将其描述为类型级DSL并通过类型检查进行验证。特别是，我们将构建Diffie-Hellman密钥交换和Needham-Schroeder-Lowe协议的验证实现，并使用它们实现演示应用程序。此应用程序（网络聊天系统）将支持安全通信（达到协议中给出的保证）、高效（由于证明义务而没有开销），并且能够与其他语言的替代实现进行通信。

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 byboth 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.