REVES: REasoning in VErification and Security

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