-
An ontological lens on attack trees: Toward adequacy and interoperability
Authors:
Ítalo Oliveira,
Stefano M. Nicoletti,
Gal Engelberg,
Mattia Fumagalli,
Dan Klein,
Giancarlo Guizzardi
Abstract:
Attack Trees (AT) are a popular formalism for security analysis. They are meant to display an attacker's goal decomposed into attack steps needed to achieve it and compute certain security metrics (e.g., attack cost, probability, and damage). ATs offer three important services: (a) conceptual modeling capabilities for representing security risk management scenarios, (b) a qualitative assessment to…
▽ More
Attack Trees (AT) are a popular formalism for security analysis. They are meant to display an attacker's goal decomposed into attack steps needed to achieve it and compute certain security metrics (e.g., attack cost, probability, and damage). ATs offer three important services: (a) conceptual modeling capabilities for representing security risk management scenarios, (b) a qualitative assessment to find root causes and minimal conditions of successful attacks, and (c) quantitative analyses via security metrics computation under formal semantics, such as minimal time and cost among all attacks. Still, the AT language presents limitations due to its lack of ontological foundations, thus compromising associated services. Via an ontological analysis grounded in the Common Ontology of Value and Risk (COVER) -- a reference core ontology based on the Unified Foundational Ontology (UFO) -- we investigate the ontological adequacy of AT and reveal four significant shortcomings: (1) ambiguous syntactical terms that can be interpreted in various ways; (2) ontological deficit concerning crucial domain-specific concepts; (3) lacking modeling guidance to construct ATs decomposing a goal; (4) lack of semantic interoperability, resulting in ad hoc stand-alone tools. We also discuss existing incremental solutions and how our analysis paves the way for overcoming those issues through a broader approach to risk management modeling.
△ Less
Submitted 30 June, 2025;
originally announced June 2025.
-
Querying Attack-Fault-Defense Trees: Property Specification in Smart Grid and Aerospace Case Studies
Authors:
Reza Soltani,
Stefano M. Nicoletti,
Milan Lopuhaä-Zwakenberg,
Mariëlle Stoelinga
Abstract:
This paper introduces AFDL, a logic-based framework for reasoning about safety, security, and defense interactions in Attack-Fault-Defense Trees, which is a model that captures all safety, security, and defense domains in a single framework. We showcase both AFDL and propose a structured domain specific query language, LangAFDL, which enables domain experts to express complex analysis goals throug…
▽ More
This paper introduces AFDL, a logic-based framework for reasoning about safety, security, and defense interactions in Attack-Fault-Defense Trees, which is a model that captures all safety, security, and defense domains in a single framework. We showcase both AFDL and propose a structured domain specific query language, LangAFDL, which enables domain experts to express complex analysis goals through intuitive templates. LangAFDL supports both Boolean and quantified queries as well as minimal cut set analysis, capturing the interplay between safety, security, and defensive measures. We illustrate the expressiveness and utility of the approach through representative queries over two different real-world case studies: Gridshield and Ground Segment as a Service. The formalization lays the automated safety-security groundwork for analyses in mission-critical systems and paves the way for future tool development and integration into design workflows.
△ Less
Submitted 30 July, 2025; v1 submitted 30 June, 2025;
originally announced June 2025.
-
BayesL: Towards a Logical Framework for Bayesian Networks
Authors:
Stefano M. Nicoletti,
Mariëlle Stoelinga
Abstract:
We introduce BayesL, a novel logical framework for specifying, querying, and verifying the behaviour of Bayesian networks (BNs). BayesL (pronounced "Basil") is a structured language that allows for the creation of queries over BNs. It facilitates versatile reasoning concerning causal and evidence-based relationships, and permits comprehensive what-if scenario evaluations without the need for manua…
▽ More
We introduce BayesL, a novel logical framework for specifying, querying, and verifying the behaviour of Bayesian networks (BNs). BayesL (pronounced "Basil") is a structured language that allows for the creation of queries over BNs. It facilitates versatile reasoning concerning causal and evidence-based relationships, and permits comprehensive what-if scenario evaluations without the need for manual modifications to the model.
△ Less
Submitted 30 June, 2025;
originally announced June 2025.
-
WATCHDOG: an ontology-aWare risk AssessmenT approaCH via object-oriented DisruptiOn Graphs
Authors:
Stefano M. Nicoletti,
E. Moritz Hahn,
Mattia Fumagalli,
Giancarlo Guizzardi,
Mariëlle Stoelinga
Abstract:
When considering risky events or actions, we must not downplay the role of involved objects: a charged battery in our phone averts the risk of being stranded in the desert after a flat tyre, and a functional firewall mitigates the risk of a hacker intruding the network. The Common Ontology of Value and Risk (COVER) highlights how the role of objects and their relationships remains pivotal to perfo…
▽ More
When considering risky events or actions, we must not downplay the role of involved objects: a charged battery in our phone averts the risk of being stranded in the desert after a flat tyre, and a functional firewall mitigates the risk of a hacker intruding the network. The Common Ontology of Value and Risk (COVER) highlights how the role of objects and their relationships remains pivotal to performing transparent, complete and accountable risk assessment. In this paper, we operationalize some of the notions proposed by COVER -- such as parthood between objects and participation of objects in events/actions -- by presenting a new framework for risk assessment: WATCHDOG. WATCHDOG enriches the expressivity of vetted formal models for risk -- i.e., fault trees and attack trees -- by bridging the disciplines of ontology and formal methods into an ontology-aware formal framework composed by a more expressive modelling formalism, Object-Oriented Disruption Graphs (DOGs), logic (DOGLog) and an intermediate query language (DOGLang). With these, WATCHDOG allows risk assessors to pose questions about disruption propagation, disruption likelihood and risk levels, keeping the fundamental role of objects at risk always in sight.
△ Less
Submitted 30 June, 2025; v1 submitted 18 December, 2024;
originally announced December 2024.
-
How hard can it be? Quantifying MITRE attack campaigns with attack trees and cATM logic
Authors:
Stefano M. Nicoletti,
Milan Lopuhaä-Zwakenberg,
Mariëlle Stoelinga,
Fabio Massacci,
Carlos E. Budde
Abstract:
The landscape of cyber threats grows more complex by the day. Advanced Persistent Threats carry out attack campaigns - e.g. operations Dream Job, Wocao, and WannaCry - against which cybersecurity practitioners must defend. To prioritise which of these to defend against, cybersecurity experts must be equipped with the right toolbox to evaluate the most threatening ones. In particular, they would st…
▽ More
The landscape of cyber threats grows more complex by the day. Advanced Persistent Threats carry out attack campaigns - e.g. operations Dream Job, Wocao, and WannaCry - against which cybersecurity practitioners must defend. To prioritise which of these to defend against, cybersecurity experts must be equipped with the right toolbox to evaluate the most threatening ones. In particular, they would strongly benefit from (a) an estimation of the likelihood values for each attack recorded in the wild, and (b) transparently operationalising these values to compare campaigns quantitatively. Security experts could then perform transparent and accountable quantitatively-informed decisions. Here we construct such a framework: (1) quantifying the likelihood of attack campaigns via data-driven procedures on the MITRE knowledge-base, (2) introducing a methodology for automatic modelling of MITRE intelligence data, that captures any attack campaign via template attack tree models, and (3) proposing an open-source tool to perform these comparisons based on the cATM logic. Finally, we quantify the likelihood of all MITRE Enterprise campaigns, and compare the likelihood of the Wocao and Dream Job MITRE campaigns - generated with our proposed approach - against manually-built attack tree models. We demonstrate how our methodology is substantially lighter in modelling effort, and capable of capturing all the quantitative relevant data.
△ Less
Submitted 10 December, 2024; v1 submitted 9 October, 2024;
originally announced October 2024.
-
Querying Fault and Attack Trees: Property Specification on a Water Network
Authors:
Stefano M. Nicoletti,
Milan Lopuhaä-Zwakenberg,
E. Moritz Hahn,
Mariëlle Stoelinga
Abstract:
We provide an overview of three different query languages whose objective is to specify properties on the highly popular formalisms of fault trees (FTs) and attack trees (ATs). These are BFL, a Boolean Logic for FTs, PFL, a probabilistic extension of BFL and ATM, a logic for security metrics on ATs. We validate the framework composed by these three logics by applying them to the case study of a wa…
▽ More
We provide an overview of three different query languages whose objective is to specify properties on the highly popular formalisms of fault trees (FTs) and attack trees (ATs). These are BFL, a Boolean Logic for FTs, PFL, a probabilistic extension of BFL and ATM, a logic for security metrics on ATs. We validate the framework composed by these three logics by applying them to the case study of a water distribution network. We extend the FT for this network - found in the literature - and we propose to model the system under analysis with the Fault Trees/Attack Trees (FT/ATs) formalism, combining both FTs and ATs in a unique model. Furthermore, we propose a novel combination of the showcased logics to account for queries that jointly consider both the FT and the AT of the model, integrating influences of attacks on failure probabilities of different components. Finally, we extend the domain specific language for PFL with novel constructs to capture the interplay between metrics of attacks - e.g., "cost", success probabilities - and failure probabilities in the system.
△ Less
Submitted 29 January, 2024;
originally announced January 2024.
-
Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry
Authors:
Pedro Quaresma,
Pierluigi Graziani,
Stefano M. Nicoletti
Abstract:
The pursue of what are properties that can be identified to permit an automated reasoning program to generate and find new and interesting theorems is an interesting research goal (pun intended). The automatic discovery of new theorems is a goal in itself, and it has been addressed in specific areas, with different methods. The separation of the "weeds", uninteresting, trivial facts, from the "whe…
▽ More
The pursue of what are properties that can be identified to permit an automated reasoning program to generate and find new and interesting theorems is an interesting research goal (pun intended). The automatic discovery of new theorems is a goal in itself, and it has been addressed in specific areas, with different methods. The separation of the "weeds", uninteresting, trivial facts, from the "wheat", new and interesting facts, is much harder, but is also being addressed by different authors using different approaches. In this paper we will focus on geometry. We present and discuss different approaches for the automatic discovery of geometric theorems (and properties), and different metrics to find the interesting theorems among all those that were generated. After this description we will introduce the first result of this article: an undecidability result proving that having an algorithmic procedure that decides for every possible Turing Machine that produces theorems, whether it is able to produce also interesting theorems, is an undecidable problem. Consequently, we will argue that judging whether a theorem prover is able to produce interesting theorems remains a non deterministic task, at best a task to be addressed by program based in an algorithm guided by heuristics criteria. Therefore, as a human, to satisfy this task two things are necessary: an expert survey that sheds light on what a theorem prover/finder of interesting geometric theorems is, and - to enable this analysis - other surveys that clarify metrics and approaches related to the interestingness of geometric theorems. In the conclusion of this article we will introduce the structure of two of these surveys - the second result of this article - and we will discuss some future work.
△ Less
Submitted 22 January, 2024;
originally announced January 2024.
-
ATM: a Logic for Quantitative Security Properties on Attack Trees
Authors:
Stefano M. Nicoletti,
Milan Lopuhaä-Zwakenberg,
E. Moritz Hahn,
Mariëlle Stoelinga
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…
▽ More
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.
△ Less
Submitted 17 May, 2024; v1 submitted 17 September, 2023;
originally announced September 2023.
-
PFL: a Probabilistic Logic for Fault Trees
Authors:
Stefano M. Nicoletti,
Milan Lopuhaä-Zwakenberg,
E. Moritz Hahn,
Mariëlle Stoelinga
Abstract:
Safety-critical infrastructures must operate in a safe and reliable way. Fault tree analysis is a widespread method used for risk assessment of these systems: fault trees (FTs) are required by, e.g., the Federal Aviation Administration and the Nuclear Regulatory Commission. In spite of their popularity, little work has been done on formulating structural queries about FT and analyzing these, e.g.,…
▽ More
Safety-critical infrastructures must operate in a safe and reliable way. Fault tree analysis is a widespread method used for risk assessment of these systems: fault trees (FTs) are required by, e.g., the Federal Aviation Administration and the Nuclear Regulatory Commission. In spite of their popularity, little work has been done on formulating structural queries about FT and analyzing these, e.g., when evaluating potential scenarios, and to give practitioners instruments to formulate queries on FTs in an understandable yet powerful way. In this paper, we aim to fill this gap by extending BFL [32], a logic that reasons about Boolean FTs. To do so, we introduce a Probabilistic Fault tree Logic (PFL). PFL is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties that comprise probabilities. Alongside PFL, we present LangPFL, a domain specific language to further ease property specification. We showcase PFL and LangPFL by applying them to a COVID-19 related FT and to a FT for an oil/gas pipeline. Finally, we present theory and model checking algorithms based on binary decision diagrams (BDDs).
△ Less
Submitted 4 August, 2025; v1 submitted 30 March, 2023;
originally announced March 2023.
-
BFL: a Logic to Reason about Fault Trees
Authors:
Stefano M. Nicoletti,
E. Moritz Hahn,
Marielle Stoelinga
Abstract:
Safety-critical infrastructures must operate safely and reliably. Fault tree analysis is a widespread method used to assess risks in these systems: fault trees (FTs) are required - among others - by the Federal Aviation Authority, the Nuclear Regulatory Commission, in the ISO26262 standard for autonomous driving and for software development in aerospace systems. Although popular both in industry a…
▽ More
Safety-critical infrastructures must operate safely and reliably. Fault tree analysis is a widespread method used to assess risks in these systems: fault trees (FTs) are required - among others - by the Federal Aviation Authority, the Nuclear Regulatory Commission, in the ISO26262 standard for autonomous driving and for software development in aerospace systems. Although popular both in industry and academia, FTs lack a systematic way to formulate powerful and understandable analysis queries. In this paper, we aim to fill this gap and introduce Boolean Fault tree Logic (BFL), a logic to reason about FTs. BFL is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties. Alongside BFL, we present model checking algorithms based on binary decision diagrams (BDDs) to analyse specified properties in BFL, patterns and an algorithm to construct counterexamples. Finally, we propose a case-study application of BFL by analysing a COVID19-related FT.
△ Less
Submitted 1 June, 2024; v1 submitted 29 August, 2022;
originally announced August 2022.
-
Model-based Joint Analysis of Safety and Security: Survey and Identification of Gaps
Authors:
Stefano M. Nicoletti,
Marijn Peppelman,
Christina Kolb,
Mariëlle Stoelinga
Abstract:
We survey the state-of-the-art on model-based formalisms for safety and security joint analysis, where safety refers to the absence of unintended failures, and security to absence of malicious attacks. We conduct a thorough literature review and - as a result - we consider fourteen model-based formalisms and compare them with respect to several criteria: (1) Modelling capabilities and Expressivene…
▽ More
We survey the state-of-the-art on model-based formalisms for safety and security joint analysis, where safety refers to the absence of unintended failures, and security to absence of malicious attacks. We conduct a thorough literature review and - as a result - we consider fourteen model-based formalisms and compare them with respect to several criteria: (1) Modelling capabilities and Expressiveness: which phenomena can be expressed in these formalisms? To which extent can they capture safety-security interactions? (2) Analytical capabilities: which analysis types are supported? (3) Practical applicability: to what extent have the formalisms been used to analyze small or larger case studies? Furthermore, (1) we present more precise definitions for safety-security dependencies in tree-like formalisms; (2) we showcase the potential of each formalism by modelling the same toy example from the literature and (3) we present our findings and reflect on possible ways to narrow highlighted gaps. In summary, our key findings are the following: (1) the majority of approaches combine tree-like formal models; (2) the exact nature of safety-security interaction is still ill-understood and (3) diverse formalisms can capture different interactions; (4) analyzed formalisms merge modelling constructs from existing safety- and security-specific formalisms, without introducing ad hoc constructs to model safety-security interactions, or (5) metrics to analyze trade offs. Moreover, (6) large case studies representing safety-security interactions are still missing.
△ Less
Submitted 23 October, 2023; v1 submitted 11 June, 2021;
originally announced June 2021.
