arXiv subjects

Milan Lopuhaä-Zwakenberg

Publications and source records attributed to Milan Lopuhaä-Zwakenberg.

At least 19 recordsLinked to original sources

arXiv2026

Fixed-parameter tractable inference for discrete probabilistic programs, via string diagram algebraisation

Discrete probabilistic programs (DPPs) provide a highly expressive formalism for compactly defining arbitrary finite probabilistic models. This expressivity comes at a price: DPP inference is PSPACE-hard. In this work, we show that DPP inference only takes polynomial time for programs that are 'structurally simple'. More precisely, inference can be performed in polynomial time when the primal graph of each function appearing in the probabilistic program has bounded treewidth, and the inverse acceptance probability is at most exponential in the size of the probabilistic program. Existing algorithms do not achieve this performance guarantee. Our method relies on finding suitable decompositions, algebraisations, of the string diagrams underlying DPPs, employing existing algorithms for tree decompositions. This is independent of the probabilistic setting of DPPs and has direct applications to many problems, such as evaluating queries on relational databases and cybersecurity risk assessment via attack trees.

cs.DS↗

arXiv2026

Towards realistic large random models of labeled transition systems and their 0-1 laws

Model checking is the automated verification of properties (specified in some modal logic) in labeled transition systems (LTSs); it is an essential tool in ensuring software systems function as intended. State spaces of software grow exponentially, and heuristics are needed to ensure model checking remains feasible in real-world applications. Heuristics, in turn, require a good understanding on the typical behaviour of LTSs. In this paper, we use random graph theory to create a probabilistic model of large LTSs. From a theoretical analysis of the creation of large LTSs, backed by empirical data from the Model Checking Contest, we endow these models with realistic parameter values. Then, we analyze the asymptotic behaviour of this model under LTL and CTL, two modal logics popular in model checking. We show that, depending on the precise model, as the size grows to infinity we either have a convergence law (for every formula, the probability that it holds converges to a limit) or a 0-1 law (...and this limit is 0 or 1). We also discuss the theoretical complexity of determining these limits, and give algorithms for doing so. These results are the starting point towards a deep theoretical understanding of typical LTS behaviour, and highlight the promising applicability of random graph theory to model checking. \keywords{Model checking \and Random graphs \and 0-1 laws

cs.LO↗

arXiv2026

Actual causality in fault trees

Fault trees are a widely used as effective risk models for complex systems, answering the question "what can go wrong?", especially through minimal cut set analysis. We study fault trees from the perspective of Halpern & Pearl's theory of actual causality. This allows us to use fault trees to answer the question "why has it gone wrong?", which is fundamental to failure diagnostics. We give a complete classification of each of the different notions of actual causality in terms of the fault tree's graph structure and logical structure, and show how minimal cut sets give rise to actual causes.

cs.AI↗

arXiv2026

Fuzzy Fault Trees: the Fast and the Formal

We provide a rigorous framework for handling uncertainty in quantitative fault tree analysis based on fuzzy theory. We show that any algorithm for fault tree unreliability analysis can be adapted to this framework in a fully general and computationally efficient manner. This result crucially leverages both the alpha-cut representation of fuzzy numbers and the coherence property of fault trees. We evaluate our algorithms on an established benchmark of synthetic fault trees, demonstrating their practical effectiveness.

math.GM↗

arXiv2026

How hard can it be? Quantifying MITRE attack campaigns with attack trees and cATM logic

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.

cs.CR↗

arXiv2025

A Unified Compositional View of Attack Tree Metrics

Attack trees (ATs) are popular graphical models for reasoning about the security of complex systems, allowing for the quantification of risk through so-called AT metrics. A large variety of different such AT metrics have been proposed, and despite their wide-spread practical use, no systematic treatment of attack tree metrics so far is fully satisfactory. Existing approaches either fail to include important metrics, or they are too general to provide a useful systematic way for defining concrete AT metrics, giving only an abstract characterisation of their behaviour. We solve this problem by developing a compositional theory of ATs and their functorial semantics based on gs-monoidal categories. Viewing attack trees as string diagrams, we show that components of ATs form a channel category, a particular type of gs-monoidal category. AT metrics then correspond to functors of channel categories. This characterisation is both general enough to include all common AT metrics, and concrete enough to define AT metrics by their logical structure.

cs.CR↗

arXiv2025

PFL: a Probabilistic Logic for Fault Trees

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).

cs.LO↗

arXiv2025

Querying Attack-Fault-Defense Trees: Property Specification in Smart Grid and Aerospace Case Studies

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.

cs.LO↗

arXiv2025

Attack-Defense Trees with Offensive and Defensive Attributes (with Appendix)

Effective risk management in cybersecurity requires a thorough understanding of the interplay between attacker capabilities and defense strategies. Attack-Defense Trees (ADTs) are a commonly used methodology for representing this interplay; however, previous work in this domain has only focused on analyzing metrics such as cost, damage, or time from the perspective of the attacker. This approach provides an incomplete view of the system, as it neglects to model defender attributes: in real-world scenarios, defenders have finite resources for countermeasures and are similarly constrained. In this paper, we propose a novel framework that incorporates defense metrics into ADTs, and we present efficient algorithms for computing the Pareto front between defense and attack metrics. Our methods encode both attacker and defender metrics as semirings, allowing our methods to be used for many metrics such as cost, damage, and skill. We analyze tree-structured ADTs using a bottom-up approach and general ADTs by translating them into binary decision diagrams. Experiments on randomly generated ADTS demonstrate that both approaches effectively handle ADTs with several hundred nodes.

cs.CR↗

arXiv2025

Safety and Security Risk Mitigation in Satellite Missions via Attack-Fault-Defense Trees

Cyber-physical systems, such as self-driving cars or digitized electrical grids, often involve complex interactions between security, safety, and defense. Proper risk management strategies must account for these three critical domains and their interaction because the failure to address one domain can exacerbate risks in the others, leading to cascading effects that compromise the overall system resilience. This work presents a case study from Ascentio Technologies, a mission-critical system company in Argentina specializing in aerospace, where the interplay between safety, security, and defenses is critical for ensuring the resilience and reliability of their systems. The main focus will be on the Ground Segment for the satellite project currently developed by the company. Analyzing safety, security, and defense mechanisms together in the Ground Segment of a satellite project is crucial because these domains are deeply interconnected--for instance, a security breach could disable critical safety functions, or a safety failure could create opportunities for attackers to exploit vulnerabilities, amplifying the risks to the entire system. This paper showcases the application of the Attack-Fault-Defense Tree (AFDT) framework, which integrates attack trees, fault trees, and defense mechanisms into a unified model. AFDT provides an intuitive visual language that facilitates interdisciplinary collaboration, enabling experts from various fields to better assess system vulnerabilities and defenses. By applying AFDT to the Ground Segment of the satellite project, we demonstrate how qualitative analyses can be performed to identify weaknesses and enhance the overall system's security and safety. This case highlights the importance of jointly analyzing attacks, faults, and defenses to improve resilience in complex cyber-physical environments.

cs.CR↗

arXiv2024

Provable Privacy Advantages of Decentralized Federated Learning via Distributed Optimization

Federated learning (FL) emerged as a paradigm designed to improve data privacy by enabling data to reside at its source, thus embedding privacy as a core consideration in FL architectures, whether centralized or decentralized. Contrasting with recent findings by Pasquini et al., which suggest that decentralized FL does not empirically offer any additional privacy or security benefits over centralized models, our study provides compelling evidence to the contrary. We demonstrate that decentralized FL, when deploying distributed optimization, provides enhanced privacy protection - both theoretically and empirically - compared to centralized approaches. The challenge of quantifying privacy loss through iterative processes has traditionally constrained the theoretical exploration of FL protocols. We overcome this by conducting a pioneering in-depth information-theoretical privacy analysis for both frameworks. Our analysis, considering both eavesdropping and passive adversary models, successfully establishes bounds on privacy leakage. We show information theoretically that the privacy loss in decentralized FL is upper bounded by the loss in centralized FL. Compared to the centralized case where local gradients of individual participants are directly revealed, a key distinction of optimization-based decentralized FL is that the relevant information includes differences of local gradients over successive iterations and the aggregated sum of different nodes' gradients over the network. This information complicates the adversary's attempt to infer private data. To bridge our theoretical insights with practical applications, we present detailed case studies involving logistic regression and deep neural networks. These examples demonstrate that while privacy leakage remains comparable in simpler models, complex models like deep neural networks exhibit lower privacy risks under decentralized FL.

cs.LG↗

arXiv2024

Quantitative analysis of attack-fault trees via Markov decision processes

Adequate risk assessment of safety critical systems needs to take both safety and security into account, as well as their interaction. A prominent methodology for modeling safety and security are attack-fault trees (AFTs), which combine the well-established fault tree and attack tree methodologies for safety and security, respectively. AFTs can be used for quantitative analysis as well, capturing the interplay between safety and security metrics. However, existing approaches are based on modeling the AFT as a priced-timed automaton. This allows for a wide range of analyses, but Pareto analsis is still lacking, and analyses that exist are computationally expensive. In this paper, we combine safety and security analysis techniques to introduce a novel method to find the Pareto front between the metrics reliability (safety) and attack cost (security) using Markov decision processes. This gives us the full interplay between safety and security while being considerably more lightweight and faster than the automaton approach. We validate our approach on a case study of cyberattacks on an oil pipe line.

cs.CR↗

arXiv2024

ATM: a Logic for Quantitative Security Properties on Attack Trees

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.

cs.CR↗

arXiv2024

Fuzzy Fault Trees Formalized

Fault tree analysis is a vital method of assessing safety risks. It helps to identify potential causes of accidents, assess their likelihood and severity, and suggest preventive measures. Quantitative analysis of fault trees is often done via the dependability metrics that compute the system's failure behaviour over time. However, the lack of precise data is a major obstacle to quantitative analysis, and so to reliability analysis. Fuzzy logic is a popular framework for dealing with ambiguous values and has applications in many domains. A number of fuzzy approaches have been proposed to fault tree analysis, but -- to the best of our knowledge -- none of them provide rigorous definitions or algorithms for computing fuzzy unreliability values. In this paper, we define a rigorous framework for fuzzy unreliability values. In addition, we provide a bottom-up algorithm to efficiently calculate fuzzy reliability for a system. The algorithm incorporates the concept of $α$-cuts method. That is, performing binary algebraic operations on intervals on horizontally discretised $α$-cut representations of fuzzy numbers. The method preserves the nonlinearity of fuzzy unreliability. Finally, we illustrate the results obtained from two case studies.

cs.AI↗

arXiv2024

Querying Fault and Attack Trees: Property Specification on a Water Network

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.

cs.LO↗

arXiv2024

Fuzzy quantitative attack tree analysis

Attack trees are important for security, as they help to identify weaknesses and vulnerabilities in a system. Quantitative attack tree analysis supports a number security metrics, which formulate important KPIs such as the shortest, most likely and cheapest attacks. A key bottleneck in quantitative analysis is that the values are usually not known exactly, due to insufficient data and/or lack of knowledge. Fuzzy logic is a prominent framework to handle such uncertain values, with applications in numerous domains. While several studies proposed fuzzy approaches to attack tree analysis, none of them provided a firm definition of fuzzy metric values or generic algorithms for computation of fuzzy metrics. In this work, we define a generic formulation for fuzzy metric values that applies to most quantitative metrics. The resulting metric value is a fuzzy number obtained by following Zadeh's extension principle, obtained when we equip the basis attack steps, i.e., the leaves of the attack trees, with fuzzy numbers. In addition, we prove a modular decomposition theorem that yields a bottom-up algorithm to efficiently calculate the top fuzzy metric value.

cs.CR↗

arXiv2024

Attack tree metrics are operad algebras

Attack Trees (ATs) are a widely used tool for security analysis. ATs can be employed in quantitative security analysis through metrics, which assign a security value to an AT. Many different AT metrics exist, and there exist multiple general definitions that aim to study a wide variety of AT metrics at once. However, these all have drawbacks: they do not capture all metrics, and they do not easily generalize to extensions of ATs. In this paper, we introduce a definition of AT metrics based on category theory, specifically operad algebras. This encompasses all previous definitions of AT metrics, and is easily generalized to extensions of ATs. Furthermore, we show that under easily expressed operad-theoretic conditions, existing metric calculation algorithms can be extended in considerable generality.

cs.CR↗

arXiv2023

Fault tree reliability analysis via squarefree polynomials

Fault tree (FT) analysis is a prominent risk assessment method in industrial systems. Unreliability is one of the key safety metrics in quantitative FT analysis. Existing algorithms for unreliability analysis are based on binary decision diagrams, for which it is hard to give time complexity guarantees beyond a worst-case exponential bound. In this paper, we present a novel method to calculate FT unreliability based on algebras of squarefree polynomials and prove its validity. We furthermore prove that time complexity is low when the number of multiparent nodes is limited. Experiments show that our method is competitive with the state-of-the-art and outperforms it for FTs with few multiparent nodes.

cs.DS↗