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:

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:

5 publications:
  • [NPZ17] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Systems. Real-Time Systems, Springer. To appear. 2017. [pdf] [bib]
  • [DFK+15] Klaus Draeger, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems. Logical Methods in Computer Science, 11(2). 2015. [pdf] [bib] [Proposes techniques for permissive controller synthesis on stochastic games, implemented in an extension of PRISM.]
  • [NPZ15] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Real-Time Systems. In Proc. 13th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'15), volume 9268 of LNCS, pages 240-255, Springer. September 2015. [pdf] [bib] [Develops techniques for verification and controller synthesis on a partially observable variant of probabilistic timed automata, implemented in an extension of PRISM.]
  • [BCC+14] Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelík, Vojtěch Forejt, Jan Křetínský, Marta Kwiatkowska, David Parker and Mateusz Ujma. Verification of Markov Decision Processes using Learning Algorithms. In Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA'14), volume 8837 of LNCS, pages 98-114, Springer. November 2014. [pdf] [bib] [Presents MDP verification techniques, implemented in PRISM, based on real-time dynamic programming and delayed Q-learning.]
  • [DFK+14] Klaus Draeger, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of LNCS, pages 531-546, Springer. April 2014. [pdf] [bib] [Presents permissive controller synthesis techniques for stochastic games, implemented in an extension of PRISM.]