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

The choice of one’s programming language and relative ecosystem of libraries can affect the likelihood of encountering a critical vulnerability. Simply counting the vulnerabilities by mining a software repository is not enough, and case-control studies are a well-accepted methodology to determine relative risk. Yet, they require the ability to compare ‘equals with equals’ as a library for text processing is likely subject to less security scrutiny than a library for web applications. To compare libraries, we implemented a human-guided protocol to transfer classification categories from an ecosystem to libraries of another ecosystem. By building of this categorization, we performed a case-control study with the vulnerabilities available on Snyk and with status ’reviewed’ in the Github security Advisories till 2024. We mapped 76 Java/Maven libraries and 221 Python/PyPI packages as ’cases’ (libraries with vulnerabilities with a CVSS critical score) compared them against 58 Java/Maven and 166 Python/PyPI ’controls’ (Only with a high CVSS score). We found and overall the odds ratio of ending with a critical vulnerability is slightly higher when using a Java/Maven library in comparison to using a Python/PyPi package (1.13x). We refine the analysis to understand possible reasons for our result by using the CVSS vector metric. A possible explanation is that a vulnerability with low attack complexity has disproportionately higher chances to be critical in Java/Maven (38.9x) than in Python/PyPI (5.9x). Such results might be explained by the lack of past security interest in the Python ecosystem. By using the introduction of the OWASP dependency checker in 2023 for Python as possible indication of community interest, we found a risk reversal: after 2023 the risk of ending with a critical vulnerability (as opposed to just a high severity one) is significantly higher (2.4x) for a Python/PyPI package than for a Java/Maven library. To allow replication and updates, we make the dataset and the protocol individual steps available as open data.

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.

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.

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.

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.

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.

This dataset has been superseded by https://zenodo.org/records/10480832

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.

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.

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.

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.

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.

To address the issue of educating and training new experts in cybersecurity, it is crucial to identify the specific educational needs of the various professions that exist in the field. We measure these needs by analysing six cybersecurity-related job profiles—each with its own specific skill requirements—that have been assessed by academic and industrial organisations from the cybersecurity community in 14 European countries. We find that it is possible to identify a series of “transversal” skills relevant to all job profiles, and thus of utmost importance in the cybersecurity curricula. However, we also observe that academic and industrial priorities differ substantially, and that skills related to the area of Human security do not rank particularly high, possibly exposing the difficulty of integrating such concepts in traditional education.

This work discusses an approach to estimate the likelihood of occurrence and evolution in time of software security issues. First, software vulnerability assessment is revised under the light of recent studies. Then, guidelines are proposed that allow for (formal) modelling stochastic aspects of cybersecurity-relevant scenarios. This opens a connection to the field of formal methods, where automated tools like statistical model checkers can estimate the value of property queries characterising such scenarios. But exploitable vulnerabilities and attacks in cybersecurity are rare events, which calls for specialised tools. In view of this, the work finalises presenting FIG, a statistical model checker specialised on rare event simulation. FIG, an open source software tool freely available at https://git.cs.famaf.unc.edu.ar/dsg/fig, can be used to estimate the probability of an attack within the next release cycle.

This dataset contains expert assessments of the cybersecurity skills required for six job profiles in Europe, as determined via surveys responded by cybersecurity experts from academia and industry. The data can be used to identify educational needs in the cybersecurity sector and compare against other frameworks. The six cybersecurity-oriented job profiles used in the surveys are: General cybersec auditor; Technical cybersec auditor; Threat modelling engineer; Security engineer; Enterprise cybersecurity practitioner; Cybersecurity analyst. Data-i.e. expert assessments-was collected via surveys, targeted at European experts in cybersecurity from academia and industry. Respondents characterised the skills needed to perform in six job profiles using the CSEC+ framework: a cybersecurity skills framework prepared as a spreadsheet where cybersecurity skills must be ranked in a Likert scale from 0 (irrelevant) to 4 (advance knowledge needed). Metadata requested included the type of organisation of the respondent (Large company, SME, Academic/Research, Public administration, Other) and the country of origin. There were three data-collection phases: (1) an initial phase, used also to refine later larger-scale processes, carried out in Oct 2021-Jan 2022 and resulting in 13 expert assessments from four EU countries; (2) a second phase implemented as an online service broadcast to a larger audience, carried out in Mar-Apr 2022 and resulting in 15 assessments from eight European countries; (3) and a third phase, allowing direct online input and distributed in PC and mobile form, carried out in Sep-Oct 2022 and resulting in 32 assessments from ten European countries. The raw data gathered was stored and processed via spreadsheets, computing statistical information (mean, stdev) on how much each cybersecurity skill and area was deemed necessary to perform in each job profile. This is visualised as a heatmap where colour intensity symbolises value, and circle diffusion symbolises spread. Processed data further includes visualisations on how the area of origin of the respondent (academia, as in "producer of education", vs. industry, as in "consumer of education") influences the responses. This is shown as bar plots, where whiskers represent confidence intervals used for statistical-significance tests. This data can serve as basis to understand the educational needs for the cybersecurity sector in Europe. It can be reused for comparison against frameworks, other than CSEC+, to assess the need of education in specific cybersecurity sectors such as human security. Furthermore, the Qualtrics survey template (included) is a ready-made solution for replication studies.

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.

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.

Maturity assessment models have repeatedly been applied to education and to cyber security with the aim of improving the performance and management of private and public institutions. However, no attempts have been made so far to create a framework for the evaluation of cyber security education, which is an increasingly pressing matter due to the demand for cyber security professionals in the European Union. This paper contributes with a proposal for a maturity assessment model of cyber security education, including a discussion of one of the main issues in the field: the definition of knowledge units for the standardization of cyber security education in Europe.