arXiv subjects

Carlos E. Budde

Publications and source records attributed to Carlos E. Budde.

At least 19 recordsLinked to original sources

arXiv2026

A Taxonomy of Distance Metrics for Time-Sensitive Importance Splitting: Timer Bounds, Resampling, and the Global Age

Importance splitting (ISPLIT) evaluates the probabilities of rare events in non-Markovian models. It requires a heuristic importance function (IFUN) that estimates the distance to the target. While including timer evaluations in the IFUN can substantially improve the effectiveness of ISPLIT, the existing time-sensitive IFUNs evaluate simulation states with respect to single sampled timer values. Thus, reaching highly important states requires simultaneously sampling specific combinations of timer values, yielding many unproductive simulation runs. In this paper, we revisit time-sensitive ISPLIT with the goal of steering simulation runs towards important states. First, we study how timer values can be resampled conditioned on the elapsed time. The importance can be evaluated by considering the set of feasible timer values, decoupling importance estimation from timer samples. Second, we exploit the global age of a simulation to identify and prune the executions that can no longer reach the target within the remaining time budget. Together, these ideas lead to a taxonomy of distance metrics clarifying the role of timer bounds, resampling, and the global age. In particular, for models with unbounded timers, we show that time-sensitive IFUNs collapse to ordinary IFUNs under resampling. Experiments demonstrate that the proposed formulations substantially improve the accuracy of ISPLIT estimators.

stat.ME↗

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

Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)

Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error guarantees. It is traditionally used to estimate probabilities and expected rewards, i.e. means of different random variables on paths. In this paper, we develop methods using the Dvoretzky-Kiefer-Wolfowitz-Massart inequality (DKW) to extend SMC beyond means to compute quantities such as quantiles, conditional value-at-risk, and entropic risk. The DKW provides confidence bounds on the random variable's entire cumulative distribution function, a much more versatile guarantee compared to the statistical methods prevalent in SMC today. We have implemented support for computing new quantities via the DKW in the 'modes' simulator of the Modest Toolset. We highlight the implementation and its versatility on benchmarks from the quantitative verification literature.

stat.ME↗

arXiv2025

Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)

Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The 'modes' SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.

cs.LO↗

arXiv2025

Time-Sensitive Importance Splitting

State-of-the-art methods for rare event simulation of non-Markovian models face practical or theoretical limits if observing the event of interest requires prior knowledge or information on the timed behavior of the system. In this paper, we attack both limits by extending importance splitting with a time-sensitive importance function. To this end, we perform backwards reachability search from the target states, considering information about the lower and upper bounds of the active timers in order to steer the generation of paths towards the rare event. We have developed a prototype implementation of the approach for input/output stochastic automata within the Modest Toolset. Preliminary experiments show the potential of the approach in estimating rare event probabilities for an example from reliability engineering.

cs.LO↗

arXiv2024

Digging for Decision Trees: A Case Study in Strategy Sampling and Learning

We introduce a formal model of transportation in an open-pit mine for the purpose of optimising the mine's operations. The model is a network of Markov automata (MA); the optimisation goal corresponds to maximising a time-bounded expected reward property. Today's model checking algorithms exacerbate the state space explosion problem by applying a discretisation approach to such properties on MA. We show that model checking is infeasible even for small mine instances. Instead, we propose statistical model checking with lightweight strategy sampling or table-based Q-learning over untimed strategies as an alternative to approach the optimisation task, using the Modest Toolset's modes tool. We add support for partial observability to modes so that strategies can be based on carefully selected model features, and we implement a connection from modes to the dtControl tool to convert sampled or learned strategies into decision trees. We experimentally evaluate the adequacy of our new tooling on the open-pit mine case study. Our experiments demonstrate the limitations of Q-learning, the impact of feature selection, and the usefulness of decision trees as an explainable representation.

cs.FL↗

arXiv2024

Forecasting the risk of software choices: A model to foretell security vulnerabilities from library dependencies and source code evolution

Software security mainly studies vulnerability detection: is my code vulnerable today? This hinders risk estimation, so new approaches are emerging to forecast the occurrence of future vulnerabilities. While useful, these approaches are coarse-grained and hard to employ for project-specific technical decisions. We introduce a model capable of vulnerability forecasting at library level. Formalising source-code evolution in time together with library dependency, our model can estimate the probability that a software project faces a CVE disclosure in a future time window. Our approach is white-box and lightweight, which we demonstrate via experiments involving 1255 CVEs and 768 Java libraries, made public as an open-source artifact. Besides probabilities estimation, e.g. to plan software updates, this formal model can be used to detect security-sensitive points in a project, or measure the health of a development ecosystem.

cs.SE↗

arXiv2024

Transient Evaluation of Non-Markovian Models by Stochastic State Classes and Simulation

Non-Markovian models have great expressive power, at the cost of complex analysis of the stochastic process. The method of Stochastic State Classes (SSCs) derives closed-form analytical expressions for the joint Probability Density Functions (PDFs) of the active timers with marginal expolynomial PDF, though being hindered by the number of concurrent non-exponential timers and of discrete events between regenerations. Simulation is an alternative capable of handling the large class of PDFs samplable via inverse transform, which however suffers from rare events. We combine these approaches to analyze time-bounded transient properties of non-Markovian models. We enumerate SSCs near the root of the state-space tree and then rely on simulation to reach the target, affording transient evaluation of models for which the method of SSCs is not viable while reducing computational time and variance of the estimator of transient probabilities with respect to simulation. Promising results are observed in the estimation of rare event probabilities.

cs.LO↗

arXiv2024

Vulnerability anti-patterns in Solidity: Increasing smart contracts security by reducing false alarms

Turing completeness has made Ethereum smart contracts attractive to blockchain developers and attackers alike. To increase code security, many tools can now spot most known vulnerabilities$-$at the cost of production efficiency. Recent studies show false-positive ratios over 99% in state-of-the-art technologies: this makes them impractical for use in industry and have raised questions on the direction of academic research. In this work we show how integrating and extending current analyses is not only feasible, but also a next logical step in smart-contract security. We propose light-weight static checks on the morphology and dynamics of Solidity code, stemming from a developer-centric notion of vulnerability, that we use to verify the output of other tools, flag potential false alarms, and suggest verifications. Besides technical details we implemented an open-source prototype. For three top-10 vulnerabilities it flags 324 warnings of other tools as false-positives, in 60 verified de-duplicated smart contracts selected from the blockchain by the presence of true (and false) vulnerabilities. This amounts to a 92%- to 100%-reduction in the number of false-positives for these vulnerabilities.

cs.CR↗

arXiv2024

Tools at the Frontiers of Quantitative Verification

The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

cs.LO↗

arXiv2024

Cross-ecosystem categorization: A manual-curation protocol for the categorization of Java Maven libraries along Python PyPI Topics

Context: Software of different functional categories, such as text processing vs. networking, has different profiles in terms of metrics like security and updates. Using popularity to compare e.g. Java vs. Python libraries might give a skewed perspective, as the categories of the most popular software vary from one ecosystem to the next. How can one compare libraries datasets across software ecosystems, when not even the category names are uniform among them? Objective: We study how to generate a language-agnostic categorisation of software by functional purpose, that enables cross-ecosystem studies of libraries datasets. This provides the functional fingerprint information needed for software metrics comparisons. Method: We designed and implemented a human-guided protocol to categorise libraries from software ecosystems. Category names mirror PyPI Topic classifiers, but the protocol is generic and can be applied to any ecosystem. We demonstrate it by categorising 256 Java/Maven libraries with severe security vulnerabilities. Results: The protocol allows three or more people to categorise any number of libraries. The categorisation produced is functional-oriented and language-agnostic. The Java/Maven dataset demonstration resulted in a majority of Internet-oriented libraries, coherent with its selection by severe vulnerabilities. To allow replication and updates, we make the dataset and the protocol individual steps available as open data. Conclusions: Libraries categorisation by functional purpose is feasible with our protocol, which produced the fingerprint of a 256-libraries Java dataset. While this was labour intensive, humans excel in the required inference tasks, so full automation of the process is not envisioned. However, results can provide the ground truth needed for machine learning in large-scale cross-ecosystem empirical studies.

cs.SE↗

arXiv2022

Efficient and Generic Algorithms for Quantitative Attack Tree Analysis

Numerous analysis methods for quantitative attack tree analysis have been proposed. These algorithms compute relevant security metrics, i.e. performance indicators that quantify how good the security of a system is; typical metrics being the most likely attack, the cheapest, or the most damaging one. However, existing methods are only geared towards specific metrics or do not work on general attack trees. This paper classifies attack trees in two dimensions: proper trees vs. directed acyclic graphs (i.e. with shared subtrees); and static vs. dynamic gates. For three out of these four classes, we propose novel algorithms that work over a generic attribute domain, encompassing a large number of concrete security metrics defined on the attack tree semantics; dynamic attack trees with directed acyclic graph structure are left as an open problem. We also analyse the computational complexity of our methods.

cs.CR↗

arXiv2022

Automated fault tree learning from continuous-valued sensor data: a case study on domestic heaters

Many industrial sectors have been collecting big sensor data. With recent technologies for processing big data, companies can exploit this for automatic failure detection and prevention. We propose the first completely automated method for failure analysis, machine-learning fault trees from raw observational data with continuous variables. Our method scales well and is tested on a real-world, five-year dataset of domestic heater operations in The Netherlands, with 31 million unique heater-day readings, each containing 27 sensor and 11 failure variables. Our method builds on two previous procedures: the C4.5 decision-tree learning algorithm, and the LIFT fault tree learning algorithm from Boolean data. C4.5 pre-processes each continuous variable: it learns an optimal numerical threshold which distinguishes between faulty and normal operation of the top-level system. These thresholds discretise the variables, thus allowing LIFT to learn fault trees which model the root failure mechanisms of the system and are explainable. We obtain fault trees for the 11 failure variables, and evaluate them in two ways: quantitatively, with a significance score, and qualitatively, with domain specialists. Some of the fault trees learnt have almost maximum significance (above 0.95), while others have medium-to-low significance (around 0.30), reflecting the difficulty of learning from big, noisy, real-world sensor data. The domain specialists confirm that the fault trees model meaningful relationships among the variables.

cs.LG↗

arXiv2021

Efficient Algorithms for Quantitative Attack Tree Analysis

Numerous analysis methods for quantitative attack tree analysis have been proposed. These algorithms compute relevant security metrics, i.e. performance indicators that quantify how good the security of a system is, such as the most likely attack, the cheapest, or the most damaging one. This paper classifies attack trees in two dimensions: proper trees vs. directed acyclic graphs (i.e. with shared subtrees); and static vs. dynamic gates. For each class, we propose novel algorithms that work over a generic attribute domain, encompassing a large number of concrete security metrics defined on the attack tree semantics. We also analyse the computational complexity of our methods.

cs.CR↗

arXiv2019

Rare Event Simulation for non-Markovian repairable Fault Trees

Dynamic Fault Trees (DFT) are widely adopted in industry to assess the dependability of safety-critical equipment. Since many systems are too large to be studied numerically, DFTs dependability is often analysed using Monte Carlo simulation. A bottleneck here is that many simulation samples are required in the case of rare events, e.g. in highly reliable systems where components fail seldomly. Rare Event Simulation (RES) provides techniques to reduce the number of samples in the case of rare events. We present a RES technique based on importance splitting, to study failures in highly reliable DFTs. Whereas RES usually requires meta-information from an expert, our method is fully automatic: by cleverly exploiting the fault tree structure we extract the so-called importance function. We handle DFTs with Markovian and non-Markovian failure and repair distributions (for which no numerical methods exist) and show the efficiency of our approach on several case studies.

cs.DC↗

arXiv2019

A compositional semantics for Repairable Fault Trees with general distributions

Fault Tree Analysis (FTA) is a prominent technique in industrial and scientific risk assessment. Repairable Fault Trees (RFT) enhance the classical Fault Tree (FT) model by introducing the possibility to describe complex dependent repairs of system components. Usual frameworks for analyzing FTs such as BDD, SBDD, and Markov chains fail to assess the desired properties over RFT complex models, either because these become too large, or due to cyclic behaviour introduced by dependent repairs. Simulation is another way to carry out this kind of analysis. In this paper we review the RFT model with Repair Boxes as introduced by Daniele Codetta-Raiteri. We present compositional semantics for this model in terms of Input/Output Stochastic Automata, which allows for the modelling of events occurring according to general continuous distribution. Moreover, we prove that the semantics generates (weakly) deterministic models, hence suitable for discrete event simulation, and prominently for Rare Event Simulation using the FIG tool.

cs.FL↗

arXiv2019

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems

Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-Agents Systems--EAMAS. The ADT-EAMAS transformation is performed in a systematic manner that ensures correctness. The transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools.

cs.CR↗

arXiv2012

Narrow-escape-time problem: the imperfect trapping case

We present a master equation approach to the \emph{narrow escape time} (NET) problem, i.e. the time needed for a particle contained in a confining domain with a single narrow opening, to exit the domain for the first time. We introduce a finite transition probability, $ν$, at the narrow escape window allowing the study of the imperfect trapping case. Ranging from 0 to $\infty$, $ν$ allowed the study of both extremes of the trapping process: that of a highly deficient capture, and situations where escape is certain ("perfect trapping" case). We have obtained analytic results for the basic quantity studied in the NET problem, the \emph{mean escape time} (MET), and we have studied its dependence in terms of the transition (desorption) probability over (from) the surface boundary, the confining domain dimensions, and the finite transition probability at the escape window. Particularly we show that the existence of a global minimum in the NET depends on the `imperfection' of the trapping process. In addition to our analytical approach, we have implemented Monte Carlo simulations, finding excellent agreement between the theoretical results and simulations.

cond-mat.stat-mech↗