ATM: a Logic for Quantitative Security Properties on Attack Trees

Abstract Critical infrastructure systems — for which high reliability and availability are paramount — must operate securely. Attack trees (ATs) are hierarchical diagrams that offer a flexible modelling language used to assess how systems can be attacked. ATs are widely employed both in industry and academia but — in spite of their popularity — little work has been done to give practitioners instruments to formulate queries on ATs in an understandable yet powerful way. In this paper we fill this gap by presenting $$\textsf {ATM}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ATM</mml:mi> </mml:math> , a logic to express quantitative security properties on ATs. $$\textsf {ATM}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ATM</mml:mi> </mml:math> allows for the specification of properties involved with security metrics that include “cost”, “probability” and “skill” and permits the formulation of insightful what-if scenarios. To showcase its potential, we apply $$\textsf {ATM}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ATM</mml:mi> </mml:math> both to the case study of a CubeSAT and to a larger model, constructed from the real-life cyberespionage campaign Operation Dream Job , as recorded by the MITRE ATT&amp;CK Database. We showcase property specification on the corresponding attack trees and propel usability of $$\textsf {ATM}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ATM</mml:mi> </mml:math> by presenting $$\textsf {LangATM}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LangATM</mml:mi> </mml:math> – a domain specific language for our logic. Finally, we present theory and algorithms — based on binary decision diagrams — to check properties and compute metrics of $$\textsf {ATM}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ATM</mml:mi> </mml:math> -formulae.