| Title | A2G2V: Automatic Attack Graph Generation and Visualization and Its Applications to Computer and SCADA Networks |
| Publication Type | Journal Article |
| Year of Publication | 2020 |
| Authors | Ghazo, A. T. Al, Ibrahim, M., Ren, H., Kumar, R. |
| Journal | IEEE Transactions on Systems, Man, and Cybernetics: Systems |
| Volume | 50 |
| Pagination | 3488–3498 |
| Date Published | oct |
| ISSN | 2168-2232 |
| Keywords | A2G2V algorithm, architecture description tool, atomic-level vulnerabilities, attack graph, Attack Graphs, automatic attack graph generation, composability, Computational modeling, Computer architecture, computer network security, computer networks, control networks, Cyber-physical systems, Cyber-Physical Systems (CPS), Cyber-physical systems security, data visualisation, enumerating counterexamples, formal verification, graph theory, Internet of Things, Internet of Things (IoT), Internet of Things systems, model checking, model-checking tools, model-checking-based automated attack graph generator and visualizer, networked system, Predictive Metrics, pubcrawl, Resiliency, SCADA networks, SCADA systems, security, Tools, visualization, visualization tool |
| Abstract | Securing cyber-physical systems (CPS) and Internet of Things (IoT) systems requires the identification of how interdependence among existing atomic vulnerabilities may be exploited by an adversary to stitch together an attack that can compromise the system. Therefore, accurate attack graphs play a significant role in systems security. A manual construction of the attack graphs is tedious and error-prone, this paper proposes a model-checking-based automated attack graph generator and visualizer (A2G2V). The proposed A2G2V algorithm uses existing model-checking tools, an architecture description tool, and our own code to generate an attack graph that enumerates the set of all possible sequences in which atomic-level vulnerabilities can be exploited to compromise system security. The architecture description tool captures a formal representation of the networked system, its atomic vulnerabilities, their pre-and post-conditions, and security property of interest. A model-checker is employed to automatically identify an attack sequence in the form of a counterexample. Our own code integrated with the model-checker parses the counterexamples, encodes those for specification relaxation, and iterates until all attack sequences are revealed. Finally, a visualization tool has also been incorporated with A2G2V to generate a graphical representation of the generated attack graph. The results are illustrated through application to computer as well as control (SCADA) networks. |
| DOI | 10.1109/TSMC.2019.2915940 |
| Citation Key | ghazo_a2g2v_2020 |
A2G2V: Automatic Attack Graph Generation and Visualization and Its Applications to Computer and SCADA Networks