Martín Barrère, Chris Hankin
In this paper, we present a novel MaxSAT-based technique to compute Maximum Probability Minimal Cut Sets (MPMCSs) in fault trees. We model the MPMCS problem as a Weighted Partial MaxSAT problem and solve it using a parallel SAT-solving architecture. The results obtained with our open source tool indicate that the approach is effective and efficient.
Martín Barrère, Chris Hankin
This paper presents a MaxSAT benchmark focused on the identification of Maximum Probability Minimal Cut Sets (MPMCSs) in fault trees. We address the MPMCS problem by transforming the input fault tree into a weighted logical formula that is then used to build and solve a Weighted Partial MaxSAT problem. The benchmark includes 80 cases with fault trees of different size and composition as well as the optimal cost and solution for each case.
Martín Barrère, Chris Hankin, Nicolas Nicolau et al.
This paper presents a MaxSAT benchmark focused on identifying critical nodes in AND/OR graphs. We use AND/OR graphs to model Industrial Control Systems (ICS) as they are able to semantically grasp intricate logical interdependencies among ICS components. However, identifying critical nodes in AND/OR graphs is an NP-complete problem. We address this problem by efficiently transforming the input AND/OR graph-based model into a weighted logical formula that is then used to build and solve a Weighted Partial MaxSAT problem. The benchmark includes 80 cases with AND/OR graphs of different size and composition as well as the optimal cost and solution for each case.
Martín Barrère, Chris Hankin, Nicolas Nicolau et al.
In recent years, Industrial Control Systems (ICS) have become an appealing target for cyber attacks, having massive destructive consequences. Security metrics are therefore essential to assess their security posture. In this paper, we present a novel ICS security metric based on AND/OR graphs that represent cyber-physical dependencies among network components. Our metric is able to efficiently identify sets of critical cyber-physical components, with minimal cost for an attacker, such that if compromised, the system would enter into a non-operational state. We address this problem by efficiently transforming the input AND/OR graph-based model into a weighted logical formula that is then used to build and solve a Weighted Partial MAX-SAT problem. Our tool, META4ICS, leverages state-of-the-art techniques from the field of logical satisfiability optimisation in order to achieve efficient computation times. Our experimental results indicate that the proposed security metric can efficiently scale to networks with thousands of nodes and be computed in seconds. In addition, we present a case study where we have used our system to analyse the security posture of a realistic water transport network. We discuss our findings on the plant as well as further security applications of our metric.
Luis Muñoz-González, Daniele Sgandurra, Martín Barrère et al.
Attack graphs are a powerful tool for security risk assessment by analysing network vulnerabilities and the paths attackers can use to compromise network resources. The uncertainty about the attacker's behaviour makes Bayesian networks suitable to model attack graphs to perform static and dynamic analysis. Previous approaches have focused on the formalization of attack graphs into a Bayesian model rather than proposing mechanisms for their analysis. In this paper we propose to use efficient algorithms to make exact inference in Bayesian attack graphs, enabling the static and dynamic network risk assessments. To support the validity of our approach we have performed an extensive experimental evaluation on synthetic Bayesian attack graphs with different topologies, showing the computational advantages in terms of time and memory use of the proposed techniques when compared to existing approaches.