Our work introduces an approach to validate threat models by providing accessible tools for observing and comparing the actual behavior of a model with the expected one. When dealing with quantitative aspects in model behavior validation, exact or statistical analysis techniques are commonly employed. Exact techniques, while providing precise quantitative properties, may face challenges in handling complex models due to the state-space explosion problem [1]. On the contrary, statistical analysis techniques, like Statistical Model Checking (SMC) [2], rely on statistically relevant samples, offering a viable solution for analyzing complex systems with potentially infinite state spaces, albeit providing statistically reliable estimations rather than exact results. In the case of black-box systems, where it is not possible to assume the complete transition structure, employing a black-box SMC [3] becomes necessary for analyzing dynamics without prior system knowledge, yielding numerical estimates and plots. However, these come without an explanation for the obtained numerical results, i.e., we do not get an explanation on the observed behavior and on why it led to such results. Consider a classic threat model depicting a thief's strategies for robbing a bank [1], analyzed using SMC to quantify the probability of a successful robbery, resulting in an unexpected low value. This prompts questions about the reasons behind the extreme value and whether it aligns with the model's intended dynamic or whether it signifies a bug. The numeric results do not provide any insights into why the analysis yielded those results or if there are issues in the model. On this basis, we formulated our proposal [4,5]. Our approach enhances SMC analysis results by automatically incorporating explicit visual information highlighting discrepancies between the model and specified criteria. This not only aids in model refinement but also serves as a comprehensive testing method, allowing experimentation with various settings within the same model structure to assess simulated model correctness. To be more specific, our method involves enriching SMC analyses by post-processing and analyzing SMC byproducts, such as log files stored while performing the simulations. We use data-driven techniques like Process Mining (PM). PM helps to identify process patterns, bottlenecks, and other model issues through visualizing activity flow [6].
Figure 1 depicts an abstract example of a model validated using our method. The input model represents an abstract model with different states, and actions used to move between those states. The simulator starts from the node A by choosing the corresponding action to move to other states of the model. To validate the output of an SMC, without our methodology, a modeler can only use the obtained numerical results, such as the probability of reaching a certain node in the model. Conversely, our approach enables the modeler to scrutinize simulation results in a model-to-model language, as opposed to model-to-numbers. Our method takes as inputs the simulated event logs, stored while performing the simulations necessary for statistical model checking. These logs are mined with Process Mining techniques and, then, used to reconstruct the first "Output Model". The rightmost model depicts the graph obtained by comparing the "Input Model" and the reconstructed one, highlighting the differences between the original model and the simulated one. The differences highlighted in the rightmost "Output Model, " i.e., the diff model, enable the modeler to quickly identify issues, such as unexpected or missing behaviors.
Several studies on risk modeling and analysis utilize SMC to evaluate the properties of a threat model [7,8]. Additionally, there are other works that perform threat modeling analysis using PM -refer to [9] for an overview of works on cybersecurity and PM. Nevertheless, to the best of our knowledge, the first preliminary work in which SMC results were enhanced with PM techniques to aid the modeler in visually identifying unwanted behaviors was presented in our previous works [4]. We further extended such work in [5] by automatically computing a diff model based on the original model specification language. The latter study demonstrated the effectiveness and scalability of our method, showcasing its applicability in both Product Line Engineering (PLE), and threat analysis domains. In the current work, we expand upon the diff model introduced in [5] and further customize it for threat model analysis. The updated diff model incorporates a new type of edge colored in green, symbolizing the initial assets possessed by the attacker before initiating the attack. For instance, an initial asset could be one of the two combinations required to open the bank vault, held by a bank clerk who decides to rob the bank. Our enhanced diff model takes into account the transitions and states in the model, depicting the attacker's initial assets by singling them out from other types of nodes and edges. This distinction helps to separate them from other transitions that are missing due to an error in the formal model. Additionally, we have incorporated a component in our method that is able to automatically fix specific classes of issues discovered in the modeler, in particular when unexpected deadlocks are detected in the simulated model. In Section 4, we conducted experiments on the RobBank model [1] to illustrate the effectiveness of our method, and we exemplify the automatic fixes proposed by our framework for the deadlocks identified in the original model.
The remainder of the paper is structured as follows: Section 2 introduces necessary background material, along with a brief introduction to the RobBank model as a running example. Following this, Section 3 presents our methodology for the diff model and the approach to fixing deadlocks. Section 4 validates our method on the presented case study. Finally, Section 5 concludes the paper and outlines future work.
We make available the use of our updated tool with all the models, the full-size figures and the replication material for this paper are available at https://t.ly/FVs6Z.
In the present work, we use RisQFLan [1], a domain-specific instantiation of QFLan [10,11,12] applied to the risk modeling and analysis domain. RisQFLan provides more capabilities than other risk analysis tools since it allows for quantitative analysis of the probability of the attack strategies in security threat models. RisQFLan allows for SMC analysis and the Probability Model Checking (PMC) technique. In RisQFLan, the probabilistic simulator and SMC (MultiVeStA) [13] interact to estimate the properties of the model statistically.
For the experiments, we adopt the threat model from [1], outlining potential attack strategies for a bank robbery. The authors emphasized that the model has infinite state space which necessitates using SMC for analysis due to the impracticality of exhaustive exploration. RisQFLan models consist of a declarative part (Attack-defence tree) and a procedural part (probabilistic attacker). Refer to [1] for a detailed presentation of RisQFLan. The Attack-defence tree (ADT) illustrates the potential attack strategies of an attacker to exploit a system. Attack trees are widely used in several domains like, e.g., defense (e.g., their use is recommended by NATO [14]), aerospace [15], or safety-critical cyber-physical systems [16].
Figure 2 illustrates the ADT depicting the root attack goal of robbing the bank and sub-attacks like OpenVault and BlowUp. OpenVault refines into LearnCombo and GetToVault, connected by an AND-relation. LearnCombo further breaks down into three nodes, FindCode, governed by a 2-out-of-3relation. An attack node succeeds only if its refinements permit it. Defense nodes, such as Memo and LockDown, decrease attack success probabilities. Countermeasures, like LockDown, are dynamic defenses activated by monitored attacks. The ADT suggests two robbery strategies: opening the vault or blowing it up, both requiring access to the vault. Opening the vault necessitates learning the combination, itself dependent on discovering at least two codes.
In addition, RisQFLan enables users to specify probabilistic attacker behavior, thereby facilitating specific analyses on different types of attackers. Figure 3 system vulnerabilities and allocating resources for system protection. Furthermore, this probabilistic attacker behavior in RisQFLan may enable the incorporation of human factors into the model. For instance, this can be achieved by modifying probabilities associated with specific vulnerabilities in the system due to user interaction, such as clicking on infected links or falling for phishing emails. Alternatively, users may design attacker behaviors that account for these human factors. In RisQFLan, the attacker behavior is modeled as a rated transition system. The transitions are labeled with the actions executed, and the rates used to compute the probability of completing one of the actions. These transitions also include the so-called guards that represent the conditions in which an action can be executed and the possible effects of executing a specific action. Besides the transition guards on a specific action, RisQFLan supports quantitative constraints that allow the imposition of limitations on the attacker's behavior by adding a total cost that an attacker can spend during the attack on a system. Any attempts to perform an attack will cost the attacker even if the attack fails, and they can keep trying to complete the attack until the limit imposed by the total cost is not reached. Once the attacker has run out of resources, they cannot try any other attacks on the system. These quantitative constraints allow us to test the system against different types of attackers with different resources. [1]. We focus on relevant parts for our experiments. For instance, in Figure 4 line 3 are listed the cost for each attack node, and in line 6 quantitative constraints allow the attacker to complete the robbery, ensuring that the total cost will never exceed 100 EUR.
Black-box statistical model checking is a method employed in analyzing RisQFLan models using the tool MultiVeStA. This approach is applied to quantitative properties, such as the likelihood of robbing the bank. MultiVeStA conducts numerous probabilistic simulations, ensuring statistically reliable estimations of the specified property. It operates as a simulation-based technique, making no assumptions about the overarching model behavior. MultiVeStA, a black-box SMC tool, facilitates simultaneous statistical analyses of multiple properties, offering scalability and the generation of confidence intervals for user-specified parameters. For instance, when estimating the expected value E[X] for robbing the bank, MultiVeStA computes the mean x from n independent simulations within a confidence interval. It has been successful applied in diverse domains, including economic agent-based models [13], highlyconfigurable systems [11,10], public transportation systems [17,18], security risk modeling [1], lending pools in decentralized finance [19], business process modeling [20], crowd steering scenarios [21], and robotic scenarios with planning capabilities [22].
This section provides a brief overview of the primary tasks involved in process-oriented data-driven techniques, commonly referred to as Process Mining (PM). PM serves as the interdisciplinary field that connects data-centric and model-based analysis techniques [6]. It utilizes real process executions to derive pertinent insights into how the observed behavior deviates from the intended behavior. PM encompasses three key activities: (control-flow) discovery, enhancement, and conformance checking. Discovery seeks to unveil an abstract representation of the executed process by consolidating all observed instances into a unified model. Once the process model is discovered, it can be enriched with additional information, such as the frequency of activity/path executions-an activity known as enhancement. Finally, conformance checking aims to identify cases where the actual executions deviate from the expected normative model. For the current work, we utilize discovery techniques to extract information from the execution traces obtained from SMC analyses. We then apply the mined model to evaluate how well the generated behavior aligns with the initial expectations.
In the following Section 3, we detail our method for constructing the updated diff model, which graphically highlights disparities between the simulated model's behavior and the model originally intended by the modeler. Additionally, we outline the steps employed to automatically resolve deadlocks identified in the simulated model.
Our method enriches SMC with PM techniques to overcome the limitations of the classic SMC black-box validation which relies only on numerical results and counterexamples. PM allows us to incorporate a white-box analysis of the behavior of the model by leveraging mining techniques on simulated model executions. However, we go beyond a simple discovery algorithm applied to event logs and, instead, we integrate these two techniques, i.e., SMC and PM, through a graphical component given in the model specification language to facilitate the automatic discovery of missing or undesirable behaviors in the model. Figure 5 illustrates our methodology presented in [5]. The steps employed to create the diff model are listed below:
• 1. Model creation -Our methodology starts with creating the model where the modeler defines all the system components, e.g., attack nodes, a list of constraints, and its procedural part. RisQFLan will then automatically generate the corresponding Attack-defence Tree and a graphical representation of the procedural part of the RisQFLan model describing the attacker's behavior. • 2. Log creation -The second step consists of the simulation of the model in which the modeler chooses the properties of the modeler that will be evaluated using the SMC tool MultiVeStA.
MultiVeStA has been extended with log capabilities in which two new functionalities enable the creation of an empty log file, invoked once per SMC analysis, and to add the rows to the log, invoked whenever an event (of interest) is to be recorded. • 3. Log pre-processing -In this step, we preprocess the event logs before applying PM techniques.
To maintain the correct order and prevent the loss of information about transitions in the logs, we rename actions by adding names of origin and target states. This step helps avoid losing crucial information about the executed process. • 4. Process mining -After pre-processing the event logs, we mine them using the Heuristic Miner (HM) [23,6] algorithm. Once the Mined PM model is discovered, we convert it from a PM model into a mined RisQFLan model (representing the procedural part of a RisQFLan model). In Figure 1, this corresponds to the first "Output Model". In this step, we return the names of the actions to their original ones which helps to compare the original RisQFLan model with the mined onethe "Input model" with the first "Output Model" in Figure 1 Additionally, the diff model includes green edges and nodes, as depicted in Figure 1 in the rightmost "Output model," representing the initial nodes acquired by the attacker before initiating the system breach.
Figure 6 illustrates the steps employed in our method to automatically fix deadlocks in the simulated model. First, we reuse the mined PM model created by mining the simulated event logs and identify the transitions that end in a deadlock. We then add new transitions to resolve these issues. Next, we extract all the system components from the RisQFLan file of the original model, which are used in an empty template of the RisQFLan file. We fill in the template with the new transition system that addresses the deadlocks.
In the following section, we demonstrate how our method can identify unwanted behaviors in the model and provide an automatic fix for those issues identified in the model.
To showcase the capability of our approach in identifying undesired behaviors within this domain, we employ MultiVeStA for the analysis of the query presented in Figure 7. This directs MultiVeStA to assess the likelihood of success for eight different attacks (line 7 in Figure 7) at each simulation step
RisQFLan bbt file ranging from 1 to 100. Similar to the approach outlined in [1], we presume that the attacker possesses a
LaserCutter capable of bypassing the Lockdown defense and has already acquired the initial code for the vault (line 2 FindoCode1, Figure 7). Our goal is to demonstrate that our methodology effectively identifies issues in the model and prompts a way to fix them.
MultiVeStA instructed the probabilistic simulator to execute 320 simulations. The analysis results for step 100 are summarized in Table 1. As expected, the probability of a complete lockdown is zero, attributed to the presence of the LaserCutter. Consequently, the likelihood of FindCode1 is 1, as both already belong to the attacker's initial assets. The SMC results show that the probability of a successful root attack is 0.19 even with LockDown disabled. This represents a low percentage (approximately 19%) of simulations concluding with a successful bank robbery. Understanding why this occurs proves to be challenging through a mere black-box examination of numerical outcomes. Illustrated in Figure 8 is the diff model generated by our methodology. It exhibits two red edges and a red node, two green edges while the remaining edges and nodes are black. The green edges represent transitions that the simulator never traversed because they were already included in the initial setup of the attacker (in Figure 7 node signifies a unique addition to our methodology: a deadlock node, indicating simulations that ended unexpectedly due to no enabled transitions. Examining the two red edges reveals that some simulations ended unexpectedly in the states TryFindCode and TryBlowUp, diminishing the overall success probability.
Issue in the model, and an automatic fix. The model has an issue with states TryFindCode and TryBlowUp, as highlighted in Figure 8. These states can only transition to attempt attacks, and if the attacker lacks sufficient funds for the corresponding attack, they get stuck due to a maximum cost constraint of 100 EUR (line 6 in Figure 4). To address this, the modeler should add escape transitions in these nodes, leading back to their parent nodes with no cost, resolving the deadlock problem and ensuring a more accurate evaluation of properties. Using the mined model, we have implemented an automatic refinement of the model that adds an escape action in the presence of a deadlock due to violating the quantitative constraints.
In Figure 9, we enhance our model by introducing a goBack action, creating transitions from TryBlowUp to Start and from TryFindCode to TryLearnCombo in Figure 9. The refined attacker behavior, shown in orange, assigns a low weight of 0.001 to these transitions, encouraging the simulator to select them
Thanks to the introduction of these new transitions, the observed dynamics no longer manifest the previously discussed deadlocks. To ensure this outcome, we utilize the identical query as depicted in Figure 7. In this particular case, MultiVeStA necessitated the execution of 320 simulations. The numerical results are listed in Table 2. Except LockDown, which remains static at zero and FindoCode1 which is again equal to 1, all other properties have exhibited an increment Now, the probability of successfully robbing the bank is approximately 45%. The resultant diff model is shown in Figure 10, where the absence of red edges or nodes means that the identified issues in the original model are fixed.
In the present work, we have expanded our approach for validating simulation models, with a specific focus on threat model analysis, and we are now making our updated tool available for practitioners. The methodology involves a combination of simulation-based analysis techniques derived from Statistical Model Checking (SMC) [2] and process-oriented data-driven techniques from Process Mining (PM) [6]. More specifically, we employ PM to elucidate SMC analyses, generating a graphical representation of the system behavior as observed in the SMC simulations. This graphical representation has been enhanced from the original implementation by incorporating additional information beneficial for the modeler when examining the results of our method. In our experimental evaluation, we demonstrate that: (1) our methodology aids in identifying issues in the model and distinguishes them from other information that are not errors, i.e., transitions belonging to the initial assets of the attacker, and (2) it generates a refined model when errors are detected in the simulated model.
In future investigations, we will focus on developing an automated tool designed to construct a comprehensive probabilistic attacker behavior based on an attack tree. This tool will assist a modeler capable of describing a system using an attack tree but unfamiliar with creating a probabilistic attacker behavior in RisQFLan. The tool will derive the system rules governing the actions permitted or restricted for the attacker from the attack tree. For example, consider an attack on a parent node, feasible only when all its child nodes are acquired. In this scenario, the sequence of attacks initiated by the simulator should be restricted from gaining the parent node before obtaining all the child nodes. This restriction is crucial, particularly when considering, for instance, an attacker attempting a lateral movement step before gaining access to the system. Allowing such a sequence of attacks would make the model unrealistic. The new automated tool will generate a complete RisQFLan file with a realistic attacker behavior that understands the rules. The modeler can easily refine it based on the type of attacker they intend to simulate. Furthermore, as part of future research, we will aim to extend the use of PM techniques beyond discovering techniques to help the modeler validate a model. Indeed, our diff model assists the modeler in checking if the behavior of the simulated model corresponds to the behavior intended by the modeler in the original model. However, the diff model can only highlight mismatches between the two models without checking if the order of sequences of attacks is correct, which, as explained above, is crucial. To ensure that the model's behavior also follows the correct order in simulating the attack on the system, we need to extract all the possible paths allowed from the attack tree. We use these paths to mine a process model, and thanks to the use of conformance checking techniques, we can ensure that the simulated model does not include cases in which the actual behavior differs from that imposed by the attack tree.