Automated Game-Theoretic Verification of Security Systems

点击翻译按钮获取中文摘要

We are surrounded by computerised systems, upon whose secure and reliable operation we are increasingly dependent. Yet flaws in these systems are common, from power plants to travel cards, and these come at high costs for individuals, companies and governments alike. So, rigorous, mathematically-sound techniques to check the security of computerised systems are essential. Security, though, is not absolute: we may only be able to guarantee that an attack on a system is possible with low probability, rather than impossible. Furthermore, system designs often need to trade off the degree of security or privacy offered against other practical concerns such as response time or power consumption. So, effective methods for the analysis of security also need to take these quantitative aspects into account.This project will develop fully-automated techniques to formally verify the correctness of security systems, to identify flaws in their operation, and to fix or optimise aspects of their design. We will do so by bringing together techniques from several different areas: (i) game-theoretic methods, to reason about the interactions between a security system and its potential attackers; and (ii) automated verification and synthesis techniques, with a particular emphasis on quantitative aspects such as probability or resource usage. Building upon recent advances in these fields, and upon existing efforts to create efficient and scalable verification methods, this project will develop novel techniques to verify security systems, implement them in freely-available software tools and apply them to a variety of security applications, from electronic voting schemes to anonymous communication networks.