REVES: REasoning in VErification and Security

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 such
properties 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 include
1) 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.

Web services and security critical software underpin Internet banking, social networks, online shopping, travel booking systems, etc. They are used on a daily basis by millions of people in the UK and over a billion people world-wide.

This project aims at developing methods and tools for making software and Web services more reliable and secure. Therefore it has a potential to impact millions of people who are routinely using such software and services. The project has a high potential to impact the economy since security related flaws in software and Web services cost millions of pounds to the economy.

One of the milestones of in this project is verification of access policies of a large scale Web service EasyChair, which is implemented in the UK and alone has 700,000 users world-wide. Since the developed methodology and tools will be largely re-usable for other Web services we expect high impact on developers and the users of such services.

In order to achieve high impact we will disseminate our results to a wide range of beneficiaries in academia, industry, developers and end users. For this we will:
1) produce world-leading results and tools for software verification and security analysis
2) publish obtained results in proceedings of world-leading conferences and journals,
3) intensively collaborate with industry, including Intel and Microsoft;
4) collaborate with partners within this UK-based Verification Institute and highly relevant Austrian RiSE (Rigorous Systems Engineering) project.

We are confident that results, methodologies and tools developed during this project will have long-lasting national and international impact in academia, industry, among developers and end-users, which will in turn have strong economical and societal benefits.