Formal methods for risk analysis

Supervisor: Milan Lopuhaä-Zwakenberg and Reza Soltani

Contact: Milan Lopuhaä-Zwakenberg

Attack trees are a popular and useful tool to model a system's vulnerability to attackers. They are used in quantitative security analysis: they can be used to calculate security metrics such as the minimal time or resources an attacker needs to successfully compromise the system. As attack trees can grow quite large in practice, there is an ongoing need for algorithms that can calculate security metrics on a feasible timescale.

In this project, the student adds to this field of research by implementing proposed algorithms, inventing new ones, or analyzing the behaviour of existing methods. Some possible avenues for research are:

• Linear programming: many security metrics can be phrased as optimization problems (such as the minimal cost of a succesful attack). Therefore, a student could create new metric calculation algorithms based on optimization techniques such as linear programming.
• Multi-metric analysis: it often makes sense to consider the interplay between metrics: one attack may be more costly to the attacker than another, but do more damage in return. There are some ideas on how to co-analyze metrics, but these have hardly been implemented, and there is also plenty of room for new ideas.
• Attack tree properties: As the problem of calculating security metrics is NP-hard, many existing algorithms are of worst-case exponential complexity. However, it is unclear how these algorithms fare in practice, and what properties of the attack tree have an impact on algorithm complexity.
• Modular analysis: An underused idea in attack tree analysis is to split up the attack tree into so-called modules and analyze each module separately. This idea can be applied to many different algorithms, and it would be interesting to see what difference this makes on both a theoretical and an experimental level.

Of course, there are many other possibilities, and students are welcome to bring their own ideas to the table.

Supervisors: Milan Lopuhaä-Zwakenberg, Azqa Nadeem

Contact: Milan Lopuhaä-Zwakenberg

Attack trees/graphs are models of attacker strategies that show all the possible pathways an attacker can follow to penetrate a network. Traditionally, these attack trees are generated using expert knowledge regarding vulnerabilities and network topologies. Recently, alert-driven attack graphs have been proposed as a novel data-driven approach to generate attack graphs without a priori expert knowledge. In this project, we aim to combine the two approaches in order to find potential missing paths in data-driven attack graphs and/or expert-driven attack trees. We apply this setting to a network of IoT devices. We build expert-driven attack trees from the IoT network specification. Next, we deploy a number of cyber attacks and collect network logs which are used to construct data-driven attack graphs. The final step is to compare the two approaches to find “unknown unknowns” in both approaches.

Supervisors: Reza Soltani, Stefano Maria Nicoletti

Contact: Stefano Maria Nicoletti

Fault Tree (FT) models are formalisms typically used in reliability engineering, safety, and risk analysis. A known drawback of FTs is that they assume statistical independence between basic events. Nevertheless, in real engineering complex systems, it is common to have dependencies not only between components but also with environmental and operational conditions.

Thus, the goal of this project is to investigate to what extend it is possible to deal with this limitation by making an interconnection with a Bayesian Network (BN). BN are probabilistic graphical models widely used to model dependencies between random variables. Useful literature in this direction is [1] and [2].

General research question

To what extend is it possible to account for dependencies of random variables via a Bayesian Network connected to the basic events of a Fault Tree model?

References

[1] Thomas, S., & Groth, K. M. (2021). Toward a hybrid causal framework for autonomous vehicle safety analysis. Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, 1748006X211043310. https://doi.org/10.1177/1748006X211043310

[2] Moradi, R., & Groth, K. M. (2020). Modernizing risk assessment: A systematic integration of PRA and PHM techniques. Reliability Engineering & System Safety, 204, 107194. https://doi.org/10.1016/j.ress.2020.107194

Tasks

• Learn about Bayesian Networks and Fault Trees
• Investigate how to combine these models to account for statistical dependency
• Implement the approach, for example as a Python script.

Requirements

It is advisable to have the following knowledge:

• Knowledge in probability theory.
• Knowing about Bayesian Networks is a plus.
• Familiarity with the Python programming language.

Supervisors: Faiza Bukhsh, Milan Lopuhaä-Zwakenberg, Azqa Nadeem

Contact: Milan Lopuhaä-Zwakenberg

Both attack graphs and business process models have been used in the literature to model attacker strategies. Alert-driven attack graphs are extracted from discrete markovian finite state automata that are great for modeling the semantic meaning of symbols, i.e., identical symbols that have different futures/pasts are modeled using different states. On the other hand, business process models are great for modeling concurrency, i.e., modeling simultaneous attacker actions. In this project, we aim to compare the merits of each approach in modeling attacker strategies from a dataset of intrusion alerts collected through a penetration testing competition. We also aim to combine the two approaches to get the best of both worlds, i.e., modeling concurrent attacker actions while also considering their semantic meaning.

Supervisor: Reza Soltani, Milan Lopuhaä-Zwakenberg

Contact: Milan Lopuhaä-Zwakenberg

In the cyber-physical domain, safety and security have a complex relationship that entails trade-offs. Specifically, taking steps to improve safety may weaken security, and vice versa. Security and safety are frequently looked into separately in different studies.

When it comes to safety, Fault Trees (FT) analysis is frequently used to identify potential problems, such as component failures that propagate throughout a system. From a security perspective, we use Attack Trees (AT) to understand how attackers might break things down into smaller steps and elements to achieve their goals.

Attack-Fault Trees (AFT) are utilized for a thorough study that considers elements related to safety and security. AFTs have limitations; for example, it is not possible to fully show the effect of safety and security on each other. One of the solutions is to convert AFTs into game automata.

 In earlier work, we have modeled FTs as a 1.5-player game [1]. One could use an analogous approach to model an AFT as a 2-player game. Such a time-game automaton could then be subject to comprehensive quantitative safety-security analysis using model checkers.

 Some research questions:

• If the attacker knows about the safety failures, how does this affect the cost and probability of the attack?
• Can attacks increase safety failure?

Reference:

1.        Soltani, R., Volk, M., Diamonte, L., Lopuhaä-Zwakenberg, M., Stoelinga, M. (2023). Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors. In: Cimatti, A., Titolo, L. (eds) Formal Methods for Industrial Critical Systems. FMICS 2023. Lecture Notes in Computer Science, vol 14290. Springer, Cham. https://doi.org/10.1007/978-3-031-43681-9_12

For more information, please contact r.soltani@utwente.nl or m.a.lopuhaa@utwente.nl. 

Supervisor: Milan Lopuhaä-Zwakenberg

Decision trees and fault trees are two models to represent the reliability of complex systems. While the information they contain is mathematically identical, the fact that the models are formed in different ways means that they are used by different people for different reasons. Therefore, it would be interesting to convert decision trees to fault trees, but contrary to the opposite direction this conversion has not been explored so far.

In this project, the student will study and develop algorithms to convert decision trees into fault trees. While it is reasonably straightforward to come up with naïve algorithms, we are particularly interested in how those algorithms can be improved by decreasing their computation time and by outputting smaller fault trees.

Supervisor: Reza Soltani, Milan Lopuhaä-Zwakenberg

Contact: Milan Lopuhaä-Zwakenberg

Discover how game theory principles provide invaluable insights into assessing and enhancing safety measures, predicting adversarial behaviors, and fortifying cybersecurity frameworks.

Currently, when it comes to safety, Fault Trees (FT) analysis is frequently used to identify potential problems, such as component failures that propagate throughout a system. From a security perspective, we use Attack Trees (AT) to understand how attackers might break things down into smaller steps and elements to achieve their goals.

Attack-Fault Trees (AFT) are utilized for a thorough study that considers elements related to safety and security. However, AFTs have limitations; for example, it is not possible to fully show the effect of safety and security on each other.

 The goal of the project is to investigate the relationship between safety and security from a game theory perspective and how we can implement the player concept for these domains.

 Please feel free to contact r.soltani@utwente.nl for more discussion or if you have any questions.

Supervisors: Milan Lopuhaä-Zwakenberg, Tom van Dijk

Fault trees are a common formalism to model how failures occur in system components and how they eventually lead to overall system failure. Analysing fault trees reveals how likely system failures are and whether the reliability of components needs to be improved.

As fault trees can contain thousands of elements, their analysis must be efficient in both time and memory consumption. One common approach is to use binary decision diagrams (BDDs) as a data structure. A BDD is graph which encodes a Boolean function in a compact representation. Translating a fault tree into a BDD yields an efficient representation which allows to analyse large fault trees. However, the memory consumption of the BDD depends on certain factors such as the variable ordering or the order in which smaller BDDs are composed during the translation.

The goal of this research project is to improve the existing fault tree analysis. The fault tree analysis we look at is implemented in the Storm model checker and uses the Sylvan library to create and handle BDDs. Building upon Sylvan and Storm, we aim to extend and optimize the existing implementation of fault tree analysis via BDDs.

Tasks

Possible research tasks are:

• Find heuristics for good variable orderings which yield small BDDs.
• Investigate whether different orders for the composition of sub-BDDs affect the peak memory requirement.
• Investigate whether multiple cores can be further exploited during the analysis.
• Integrate modular approaches which only require parts of the BDD to be stored in memory at a time.
• Bring in own ideas.

Requirements

• Knowledge about fault trees and binary decision diagrams is beneficial but not required.
• Experience with C/C++ is strongly recommended as the implementation uses these languages.

Supervisor: Milan Lopuhaä-Zwakenberg

Risk models such as fault trees (FTs) are formalisms typically used in reliability engineering, safety, and risk analysis. A known drawback of FTs is the time-consuming manual construction of these models, making them prone to human errors and incompleteness. Thanks to the ever-increasing availability of inspection and monitoring data, the development of algorithms that take care of this task in a data-driven manner are possible.

In [1] this challenge was tackled using multi-objective evolutionary algorithms, yielding compact and reliable FT models. Building upon this work, several interesting research directions are possible.

Possible research directions

• Boolean circuit design: Circuit designs aims to find circuits with a minimal number of logical gates representing a given Boolean function. FT models can be encoded by Boolean formulas. A possible research direction is to find and apply existing algorithms from circuit design for FT inference.
• Guiding the evolutionary algorithms: The current algorithm [1] takes a long time to converge when randomly applying genetic operators. One possible research direction is therefore to investigate to what extent knowledge about the models can be included to guide the genetic operators.
• Noisy and incomplete data sets: Current approaches only consider noise-free and complete failure data sets, which is of course not representative of real applications. Thus, it is interesting to investigate how to effectively deal and account for noise and incompleteness in failure data sets when inferring FT models in a data-driven manner.

References

[1] Jimenez-Roa, L. A., Heskes, T., Tinga, T., & Stoelinga, M. I. A. (2021). Automatic inference of fault tree models via multi-objective evolutionary algorithms. Preprint available online.

Requirements

Most research directions encompass a prototypical implementation. It is therefore advisable to be familiar with the Python programing language.

Supervisors: Stefano Maria Nicoletti, Reza Soltani

Contact: Stefano Maria Nicoletti

The introduction and adoption of new technologies implies the rise of new risks, related both to accidental damage (safety) and to malicious attacks (security). Furthermore, safety and security are often intertwined: passwords protect medical data from unauthorized access but are an obstacle for patients' safety during emergencies, IoT sensors can help to monitor the pressure levels of a pipeline but may provide extended attack surfaces for malicious hackers.
The existence of interdependencies between safety and security calls for a better (formal) understanding of this kind of interactions:

• At what level do safety and security interact? What interacts with what?
• Do these interactions regard requirements, countermeasures, factors (etc.)?

Tasks

The suggested tasks are the following:

• Together with your supervisor, decide on a case study of interest and investigate how safety and security interact in this setting
• Chose a formalism to analyse said case study (by discussing with your supervisors) and understand its modelling capabilities
• Starting from the chosen case study, investigate which of the different interactions between safety and security are captured by the formalism of choice
• Investigate at what level these interactions take place

For this topic, you should have a strong interest in multidisciplinary research.

Supervisors: Milan Lopuhaä-Zwakenberg, Benedikt Peterseim

Contact: Milan Lopuhaä-Zwakenberg

A constant problem in risk analysis is that many parameters are unknown or only approximately known. One way to deal with this is the mathematical formalism of fuzzy numbers, where a parameter does not have a singular value, but multiple ones with various degrees of certainty. These are then used in numerical analysis, and the final result will be a fuzzy number as well, quantifying the uncertainty of the risk analysis itself.

While fuzzy numbers are very useful from a mathematical perspective, their standard form requires in theory infinite memory to store, making it useless for practical applications. There exist some simplified versions of fuzzy numbers, such as triangular fuzzy numbers, but these are too restrictive: many mathematical operations that are used in risk analysis are not supported by fuzzy numbers.

The aim of this project is to study a new type of fuzzy numbers, called polyhedral fuzzy numbers, that are general enough to be used in risk analysis but specific enough to allow for efficient computation. In the project, the student makes efficient algorithms for mathematical operations on fuzzy numbers. A natural domain of application are attack trees and fault trees, but this can be changed according to the student's interest.

Supervisor: Stefano Maria Nicoletti, Reza Soltani, Mariëlle Stoelinga

Contact: Stefano Maria Nicoletti

Fault trees are an important formalism to assess the reliability of systems. Typically, they have been very successfully applied to complex hardware systems, like railroads or chemical plants. However, software is getting more and more important. Hence, software fault trees have been developed to account for software failures as well. One important research question is how to estimate the failure rate of software components.

Research directions:

The key idea of this project is to find good estimations for failure rates of software. Possible directions are:

• Develop a Bayesian network capturing the dependencies between different influences on the software reliability (used programming language, experience of the team, test coverage, size of project, etc.)
• Integrating existing tools (e.g., SonarQube) for better estimation of software failure rates.