Program Verification Techniques for Understanding Security Properties of Software

用于了解软件安全属性的程序验证技术

基本信息

批准号：
EP/K032542/1
负责人：
Peter O'Hearn
金额：
$ 111.69万
依托单位：
University College London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2013
资助国家：
英国
起止时间：
2013 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FK032542%2F1
关键词：
Program Verification Techniques Understanding Security

项目摘要

This proposal aims to develop automatic program verification methods that help security engineers to understand software that they have not written themselves. The engineer will be able to make sophisticated queries about resource requirements and temporal behaviour of code, such as about memory safety, privileges, or information flow. Our methods will even support synthesis of behavioural properties for the engineer: rather than make a closed-world assumption, where the complete program and physical computing device are known, our tools will discover logical descriptions of execution environments (preconditons, protocols, invariants, etc.) that pinpoint the assumptions necessary for code safety or those that trigger violations. Such tools would aid engineers by, for example, advising where to concentrate effort when looking for critical security breaches. They would also suggest where to place effort in hardening an application. Finally, by using strong analysis techniques based on verification, guarantees of security properties could be obtained, as well as flaws discovered. Towards realising this vision we have assembled a team whoseexperience ranges from program verification research on logics and algorithms to systems security research involving new operating system primitives and software structuring principles that achieve robust security goals.

该提案旨在开发自动程序验证方法，帮助安全工程师理解不是他们自己编写的软件。工程师将能够对资源需求和代码的时间行为进行复杂的查询，例如内存安全、权限或信息流。我们的方法甚至将支持工程师行为属性的综合：我们的工具将发现执行环境的逻辑描述（先决条件、协议、不变量等），而不是做出封闭世界的假设（在完整的程序和物理计算设备已知的情况下） .) 精确指出代码安全所需的假设或触发违规的假设。此类工具可以帮助工程师，例如，在寻找关键安全漏洞时建议将精力集中在哪里。他们还会建议在强化应用程序方面应在哪些方面下功夫。最后，通过使用基于验证的强大分析技术，可以获得安全属性的保证，并发现缺陷。为了实现这一愿景，我们组建了一个团队，其经验涵盖从逻辑和算法的程序验证研究到涉及新操作系统原语和实现稳健安全目标的软件结构原则的系统安全研究。

项目成果

期刊论文数量（10）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings

编程语言和系统 - 第 24 届欧洲编程研讨会，ESOP 2015，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2015，英国伦敦，2015 年 4 月 11-18 日，会议记录

DOI：
10.1007/978-3-662-46669-8_12
发表时间：
2015
期刊：
影响因子：
0
作者：
Batty M
通讯作者：
Batty M

Tools and Algorithms for the Construction and Analysis of Systems

用于系统构建和分析的工具和算法

DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
影响因子：
0
作者：
Basler G
通讯作者：
Basler G

Protecting Users by Confining JavaScript with COWL

DOI：
发表时间：
2014-10
期刊：
影响因子：
0
作者：
D. Stefan;Edward Z. Yang;Petr Marchenko;Alejandro Russo;David Herman;B. Karp;David Mazières
通讯作者：
D. Stefan;Edward Z. Yang;Petr Marchenko;Alejandro Russo;David Herman;B. Karp;David Mazières

Disproving termination with overapproximation