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 ATM, a logic to express quantitative security properties on ATs. ATM 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 ATM to the case study of a CubeSAT, presenting three different ways in which an attacker can compromise its availability. We showcase property specification on the corresponding attack tree and we present theory and algorithms - based on binary decision diagrams - to check properties and compute metrics of ATM-formulae.

翻译：关键基础设施系统——其高可靠性和可用性至关重要——必须安全运行。攻击树（ATs）是一种分层图，提供了灵活的建模语言，用于评估系统可能遭受的攻击方式。尽管ATs在工业界和学术界被广泛采用，但鲜有研究为从业者提供一种既易于理解又功能强大的工具，用于在ATs上制定查询。本文通过提出ATM（一种用于在ATs上表达定量安全属性的逻辑）填补了这一空白。ATM允许指定涉及“成本”、“概率”和“技能”等安全度量的属性，并支持构建富有洞见的假设情景分析。为展示其潜力，我们将ATM应用于CubeSAT的案例研究，呈现了攻击者可能破坏其可用性的三种不同方式。我们展示了相应攻击树上的属性规范，并提出了基于二元决策图的理论与算法，用于检查属性并计算ATM公式的度量值。