Biblio

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.

Cyber-Physical-Systems are subject to cyber-attacks due to existing vulnerabilities in the various components constituting them. System Resiliency is concerned with the extent the system is able to bounce back to a normal state under attacks. In this paper, two communication Networks are analyzed, formally described, and modeled using Architecture Analysis & Design Language (AADL), identifying their architecture, connections, vulnerabilities, resources, possible attack instances as well as their pre-and post-conditions. The generated network models are then verified against a security property using JKind model checker integrated tool. The union of the generated attack sequences/scenarios resulting in overall network compromise (given by its loss of stability) is the Attack graph. The generated Attack graph is visualized graphically using Unity software, and then used to assess the worst Level of Resilience for both networks.