Quantitative evaluation of attack defense trees using stochastic timed automata

Abstract

Security analysis is without doubt one of the most important issues in a society relying heavily on computer infrastructure. Unfortunately security analysis is also very difficult due to the complexity of systems. This is bad enough when dealing with ones own computer systems - but nowadays organisations rely on third-party services - cloud services - along with their own in-house systems. Combined this makes it overwhelming difficult to obtain an overview of possible attack scenarios. Luckily, some formalisms such as attack trees exist that can help security analysts. However, temporal behaviour of the attacker is rarely considered by these formalisms. In this paper we build upon previous work on attack-defence trees to build a proper temporal semantics. We consider the attack-defence tree a reachability objective for an attacker and thereby separate the attacker logic from the attack-defence tree. We give a temporal stochastic semantics for arbitrary attackers (adhering to certain requirements to make the attacker “sane”) and we allow annotating attacker actions with time-dependent costs. Furthermore, we define what we call a cost-preserving attacker profile and we define a parameterised attacker profile. The defined semantics is implemented via a translation to uppaal SMC. Using uppaal SMC we answer various questions such as the expected cost of an attack, we find the probability of a successful attack and we even show how an attacker can find an optimal parameter setting using ANOVA and Tukeys test.