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 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.