Automated Game-Theoretic Verification of Security Systems

Overview

"Automated Game-Theoretic Verification of Security Systems" is a 1-year research project funded by EPSRC (grant number EP/K038575/1) and led by David Parker from the University of Birmingham.

The project will develop novel automated verification techniques for security systems, with a particular focus on the use of probabilistic verification techniques for stochastic games.

Dates: Nov 2013 - Oct 2014

Project members:

• David Parker (principal investigator)
• Chunyan Mu (postdoc)

Abstract

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.

Publications

Publications arising from this project: