Submitted: March 2015
Abstract
Formal specification and verification have become a crucial element of design processes both in industry and research. One main area of application are security-critical systems. For security-critical systems, the focus of specification and verification lies on their robustness against systematic attacks of malicious intruders trying to break into a system, change its behaviour or to steal secret information from it. Security always depends both on the specific vulnerabilities of a system and the precise skills of the attacker.
The most prominent modelling technique for security-critical systems are attack trees. Attack trees allow to refine the goal an attacker wants to reach into unique and atomic events in the system and combinations thereof with operators comparable to conjunction and disjunction. Extensions of attack trees have lately been proposed, which introduce the possibility to specify time in terms of exponential delays. A formal semantics in terms of acyclic phase-type distributions has made attack trees amenable for standard model checking techniques.
Another prominent approach is ADVISE, which includes more powerful modelling and analysis features, for instance, the possibility to analyse success probabilities and overall durations of attacks. For analysis, ADVISE relies on dedicated tools.
In this thesis, we first examine the aforementioned modelling techniques with the intention to derive a set of criteria modelling techniques should satisfy concerning expressiveness, ease of use and adaptability to individual needs of system designers. With these criteria in mind, we developed a novel modelling technique for security-critical systems called attack-defence graphs (ADG), which we show to be easy to use, but at the same time expressive enough to model security-critical systems precisely. Furthermore, a formal semantics in terms of stochastic timed automata is provided. This allows us to specify properties for security-critical systems using standard modal logics and verify them with existing model checking tools. To this end, we developed ADeGraM, a Java tool, which allows to automatically translate attack-defence graphs into Modest, a specification language for stochastic hybrid systems. An additional special focus of attack-defence graphs has been the semantically sound representation of the competing parties in a security-critical system by turning the formal semantics into a game.