REVES: REasoning in VErification and Security

Lead Research Organisation: University of Manchester
Department Name: Computer Science


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.

Planned Impact

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.


10 25 50
Description Our research resulted in major developments in one of the hardest areas within artificial intelligence: automated theorem proving.
One of the most significant findings was research and development of the original AVATAR architecture for theorem proving systems (theorem provers). This architecture allowed our theorem prover Vampire to solve hundreds of problems that were previously beyond the reach of the best systems, including previous versions of Vampire.
We also extended AVATAR to work in the area of reasoning with both quantifiers and theories, resulting in major breakthrough in the area. While all most successful systems were using instance-based methods, we have shown that on practical problems AVATAR-based methods show superior performance on many classes of problems. This is very significant since the new method focuses on quantifier reasoning more than on theory reasoning, while all previously known methods focused on improving theory reasoning.
Exploitation Route The methods we developed significantly advance knowledge in the area and may result in new methods based on AVATAR.
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software)

Description First-order theorem provers are extensively used by high-tech companies and organisations involved in safety-critical applications
Sector Digital/Communication/Information Technologies (including Software)
Title Vampire 
Description Vampire is the first order theorem prover. It has been World Champion in first-order theorem proving in various divisions 34 times. In 2015 it has won 5 out of 8 divisions, in 4 of them solving more problems than all other systems together. In the main division Vampire has not been beaten since 2002. 
Type Of Technology Software 
Year Produced 2016 
Impact Vampire is used in many applications, including program analysis and reasoning in algebra by various universities and high tech companies. It is also a workhorse for trying new ideas in theorem proving. One can argue that many inventions implemented in Vampire, including indexing techniques, AVATAR architecture, and splitting methods considerably advanced the whole area of first-order theorem proving