权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Type-driven Verification of Communicating Systems

通信系统的类型驱动验证

基本信息

批准号：
EP/N024222/1
负责人：
Edwin Brady
金额：
$ 11.98万
依托单位：
University of St Andrews
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2016
资助国家：
英国
起止时间：
2016 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FN024222%2F1
关键词：
Type driven Verification 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 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.

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

项目成果

期刊论文数量（7）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Elaborator reflection: extending Idris in Idris

DOI：
10.1145/2951913.2951932
发表时间：
2016-09
期刊：
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
影响因子：
0
作者：
D. Christiansen;Edwin C. Brady
通讯作者：
D. Christiansen;Edwin C. Brady

Value-Dependent Session Design in a Dependently Typed Language