Modern industrial control systems (ICS) are increasingly integrating cyber-physical components to automate industrial processes. Such integration requires a rigorous exploration of how cyberattack impact propagates through an ICS. However, impact analysis approaches for ICS usually assume the use of specific modeling formalisms and tools, limiting their adoption by analysts familiar with potential alternatives. This work clarifies the rationale behind 20 requirements for applying SCIA: a Structured Cyberattack Impact Analysis approach with different modeling and simulation platforms. Based on a manufacturing ICS case study, we demonstrate two distinct applications of SCIA: (1) Application A, based on formal modeling and verification in UPPAAL-SMC, and (2) Application B, based on simulations in MATLAB/Simulink. We show how both applications are effective at visualizing the evolution of attacks and analyzing temporary and sustained impacts on ICS reliability and availability. In doing so, we detail the methodological differences, the extent of requirement satisfaction, and the associated trade-offs.

The Mirai botnet revolutionized the idea of IoT botnets by infecting numerous vulnerable IoT devices in 2016, leading to the rise of many Mirai variants and imitators that plague the current IoT ecosystem. Studying the botnet infection process can greatly aid us in understanding IoT botnet capabilities and the efficacy of currently available countermeasures. However, analyzing IoT botnets is difficult due to their massive scale and the numerous existing heterogeneous IoT devices that can be targeted for infection. In this paper, we model and simulate the dynamic behavior of a Mirai-like botnet infrastructure and various IoT device categories as a network of timed automata in UPPAAL-SMC. To determine the feasibility of rebooting as a countermeasure against botnets, we examine the effectiveness of rebooting on various IoT device networks. The resulting analysis provides a solid understanding of the efficacy and feasibility of rebooting on active and dormant botnet propagation processes.

Many of today's critical infrastructures, including industrial control systems (ICS), are evolving with the integration of numerous connected cyber components with legacy systems. This evolution has exposed ICSs to a new range of security vulnerabilities and threats, making cybersecurity considerations ever more critical. Understanding how severely malicious cy-berattacks can exploit such system vulnerabilities to disrupt or delay system operations is paramount for developing targeted and effective defenses. In this paper, a timed formal modelbased approach is presented to observe and analyze the manifold impact of various cyberattacks on ICS operations. The analysis is automated using UPPAAL on timed automata models of a target system and potential attackers. Representative tampering and spoofing attacks demonstrated on an illustrative manufacturing cell control system show how classical and statistical model checking, respectively, are effective at analyzing the existence and quantifying the severity of cyberattack impact on ICS mission objectives.