This PhD project will develop a suite of tool-supported techniques for the synthesis of architectural designs and reconfigurations that optimize defense against security threats in self-adaptive systems.
Self-protecting systems  use the principles of self-adaptation to dynamically adjust their architecture and parameters to defend against cyber-attacks. This capability is in great demand in systems across multiple domains, which have to provide timely response to cyber-attacks that employ new exploits and vulnerabilities that are continually appearing. However, this potential is currently underachieved because in these systems: (a) robustness against cyber-attacks is not built a priori into the structural design of the system as an intrinsic characteristic (instead, the system only reacts against cyber-attacks a posteriori), and (b) mechanisms for decision-making only reason about expected behavior, rather than adversarial behavior. That is, these approaches are able to reason about concepts such as mean time
to failure and other probabilistic estimates, instead of assuming the worst case in which an adversary will deliberately exploit weak points in the system. Although some recent approaches have started using game-theoretical frameworks to synthesize defensive strategies, their effectiveness is limited by architectural designs in which the adversarial nature of the environment has not been explicitly considered a priori.
This project, which is aligned with the University of York research theme “risk, evidence, and decision making”, will develop techniques and tools for automating the synthesis of both architectural designs and reconfigurations to optimize robustness against cyber-attacks in self-adaptive systems.
The project will extend our recent research on synthesis of architectural designs with quantitative guarantees  with techniques for: (a) generating designs and reconfigurations that use game-theoretical quantitative verification  to optimize robustness against cyber-attacks, and (b) techniques for checking the correctness of the generated designs, as well as analyzing the tradeoffs among robustness to cyber-attacks and other extra-functional properties like availability, performance, and cost.
 Eric Yuan, Naeem Esfahani, Sam Malek: A Systematic Survey of Self-Protecting Software Systems. ACM Transactions on Autonomous and Adaptive Systems 8(4): 17:1-17:41 (2014)
 Javier Camara, David Garlan, Bradley R. Schmerl: Synthesis and Quantitative Verification of Tradeoff Spaces for Families of Software Systems. 11th European Conference on Software Architecture, ECSA 2017: 3-21
 Marta Z. Kwiatkowska: Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice. 43rd International Colloquium on Automata, Languages and Programming, ICALP 2016: 4:1-4:18
Interested applicants are encouraged to contact the project supervisor Dr Javier Cámara at [email protected]
for further information.