ATM: a Logic for Quantitative Security Properties on Attack Trees
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913354089496576 |
|---|---|
| author | Nicoletti, Stefano M. Lopuhaä-Zwakenberg, Milan Hahn, E. Moritz Stoelinga, Mariëlle |
| author_facet | Nicoletti, Stefano M. Lopuhaä-Zwakenberg, Milan Hahn, E. Moritz Stoelinga, Mariëlle |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2309_09231 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | ATM: a Logic for Quantitative Security Properties on Attack Trees Nicoletti, Stefano M. Lopuhaä-Zwakenberg, Milan Hahn, E. Moritz Stoelinga, Mariëlle Cryptography and Security Logic in Computer Science 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. |
| title | ATM: a Logic for Quantitative Security Properties on Attack Trees |
| topic | Cryptography and Security Logic in Computer Science |
| url | https://arxiv.org/abs/2309.09231 |