REVES: REasoning in VErification and Security

该提案侧重于推进软件和Web服务的基于推理的验证和安全分析。在我们的日常生活中，我们依赖于软件和网络服务的安全，例如在使用数字银行或社交网络时，因此我们正在解决的问题既具有挑战性又非常重要。这个问题非常重要，其中一个主要挑战来自于安全关键应用程序中使用的软件的巨大复杂性和不断增长的规模。通常，这样的软件包含数十万到数百万行代码，这些代码由不同的开发人员使用不同的平台和要求编写。我们如何确保这些复杂的软件系统运行正常，没有安全漏洞？我们的方针是在严格的数学基础上开发用于核查和安全分析的全自动方法和工具。这些方法基于形式逻辑中验证问题的形式化，并应用自动定理证明来证明安全属性被满足，或者在证明失败时发现安全漏洞。经过50多年的研究，自动定理证明产生了深刻的理论结果和强大的工具。我们的团队在这一领域处于世界领先地位，我们的定理证明系统(吸血鬼和iProver)在过去几年中赢得了世界杯一阶定理证明(CASC)的几乎所有主要组别。然而，程序验证和安全性分析需要在定理证明和形式化方面取得更大的进展，本项目包括三个主要部分：(A)使用符号消除和内插自动生成程序属性。(B)定理证明器在实际大规模Web服务验证中的应用。(C)使用量词和理论的高效推理及其在验证程序属性中的应用。(A)继续我们从2009年开始的程序属性自动生成算法的研究。这种属性的生成对于分析非常大的程序非常重要，包括检查它们的安全相关功能。(B)的目的是为大规模Web服务的验证或访问策略设计一种实用的低成本方法，通过验证一个真实的Web服务来证明该方法的可行性，并通过基于定理证明器和模型查找器的工具来支持该方法。(C)部分植根于我们的理解，即有效的量词和理论推理对于定理证明器在验证和程序分析中的应用至关重要，并将在未来十年甚至更长时间内成为自动推理研究的核心。该项目旨在设计和实现同时使用量词和理论的高效自动推理算法。该项目的里程碑包括：1)基础理论突破：Web服务访问策略的形式化；安全验证的高效不变量生成和内插；高效的量词和理论推理方法；2)实用工具：我们将开发新的推理方法和工具，以及基于这些推理工具的验证和程序分析工具。3)将开发的方法和工具应用于现实生活验证问题：我们将全面验证EasyChain的与安全相关的访问策略，它是英国开发的面向学术用户的最大(如果不是最大的)Web服务之一；我们将与业界合作：英特尔和微软，在工业环境中应用开发的方法。

This proposal focuses on advancing reasoning-based verification and security analysis of software and Web services. In our everyday life we rely on security of software and Web services e.g. when using digital banking or social networks and therefore the problem we are addressing is both challenging and important.This problem is highly non-trivial and one of the major challenges comes from the enormous complexity and growing size of the software used in security-critical applications. Typically such software contains from hundreds of thousands to millions lines of code written by different developers using different platforms and requirements. How we can ensure that these complex software systems are functioning correctly and do not have security vulnerabilities? Our approach is to develop fully automatic methods and tools for verification and security analysis based on rigours mathematical foundations. These methods are based on formalisation of the verification problem in formal logic and applying automated theorem proving to prove that the security properties are satisfied, or otherwise find security vulnerabilities if such a proof fails. Over 50 years of research in automated theorem proving resulted in deep theoretical results and powerful tools based on these results. Our group is world-leading in this area, our theorem proving systems (Vampire and iProver) have been winning almost all major divisions in the world cup in first-order theorem proving (CASC) the last years. However, program verification and security analysis requires further considerable advances in both theorem proving and formalisation which we address in this project.The project consists of three major parts: (A) Automatic generation of program properties using symbol elimination and interpolation.(B) Application of theorem provers in verification of real-life large-scale Web services.(C) Efficient reasoning with quantifiers and theories with applications in verifying program properties.Part (A) continues the line of research in algorithms for an automatic generation of program properties we started in 2009. Generation of suchproperties is very important for analysing very large programs, including checking their security-related features. The aim of (B) is to design a practical low-cost methodology for verification or access policies for large-scale Web services, demonstration of viability of this methodology by verifying a real-life Web service, and supporting this methodology by tools based on theorem provers and model finders. Part (C) is rooted in our understanding that efficient reasoning with both quantifiers and theories is crucial for applications of theorem provers in verification and program analysis and will be central in automated reasoning research for the next decade or even longer. It aims at the design and implementation of efficient algorithms for automated reasoning when both quantifiers and theories are used.The milestones of the project include1) fundamental theoretical breakthroughs: formalisation of access policies of Web services; efficient invariant generation and interpolation for security verification; efficient methods for reasoning with quantifiers and theories 2) practical tools: we will develop new reasoning methods and tools, and verification and program analysis tools based on these reasoning tools.3) application of developed methods and tools to real-life verification problems: we will fully verify security-related access policies of EasyChair,which is one of the largest, if not the largest, Web service for academic users developed in the UK; we will collaborate with industry: Intel and Microsoft to apply developed methods in an industrial environment.