Parametric Analyses of Attack-fault Trees^*

Issue title: Special Issue of Selected Papers from ACSD 2019

Guest editors: Jörg Keller and Wojciech Penczek

Article type: Research Article

Authors: André, Étienne^a | Lime, Didier^b | Ramparison, Mathias^{c; †} | Stoelinga, Mariëlle^d

Affiliations: [a] Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France. eandre93430@lipn13.fr | [b] École Centrale de Nantes, LS2N, CNRS, UMR 6004, Nantes, France. Didier.Lime@ec-nantes.fr | [c] Université Sorbonne Paris Nord, LIPN, CNRS, F-93430, Villetaneuse, France. mathias.ramparison@uni.lu | [d] Formal Methods and Tools, University of Twente, The Netherlands. m.i.a.stoelinga@utwente.nl

Correspondence: [†] Address for correspondence: Grenoble INP, VERIMAG, France.

Note: [*] This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002), the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015), the PHC Van Gogh project PAMPAS, by STW under the project 15474 SEQUOIA, KIA KIEM project 628.010.006 StepUp, the EU under the project 102112 SUCCESS and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.

Abstract: Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i. e., absence of unintentional failures) and security (i. e., no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to consider these problems is attack trees, a tree-based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parameterize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Moreover, we add the possibility to define counter-measures. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure.

Keywords: security, attack-fault trees, parametric timed automata, IMITATOR

DOI: 10.3233/FI-2021-2066

Journal: Fundamenta Informaticae, vol. 182, no. 1, pp. 69-94, 2021