This study investigates cyberattacks targeting industrial control systems (ICS) and proposes a formal methodology for their analysis. Typical attack progression scenarios are identified and modeled using logical attack graphs. These graphs are transformed into Boolean expressions and then into Conjunctive Normal Form (CNF) to enable automated analysis via SAT/SMT solvers. The proposed methodology allows for determining whether a given attack is feasible within a specific system configuration, identifying minimal configurations that either ensure security or leave the system vulnerable. It also considers the presence of irremediable vulnerabilities and incorporates system usability constraints into the analysis process. To demonstrate the approach, a computational experiment was conducted using the z3-python library, highlighting the applicability of the method in evaluating real-world ICS security scenarios. The proposed approach can assist in designing and implementing effective countermeasures for protecting critical infrastructure systems from cyber threats.
Industrial control systems (ICS) are frequently targeted by various types of cyberattacks [
One of the challenges in this domain is the construction of attack graphs for large-scale networks.
As demonstrated in [
On the other hand, logical graph-based models can be interpreted as Boolean expressions [11], [12], which can be further analyzed using specialized tools [13]. Among these tools are SAT (Boolean Satisfiability) and SMT (Satisfiability Modulo Theories) solvers, which are designed to efficiently solve computationally complex problems [14], [15]. In the case of large attack graphs characterized by a significant number of states, the corresponding Boolean expressions may involve a vast number of variables. As a result, exhaustive enumeration of all possible configurations to find optimal ones becomes computationally infeasible within a reasonable timeframe. Therefore, it is essential to employ specialized verification tools such as SAT/SMT solvers. Using SAT/SMT solvers allows for the verification of formula satisfiability under specific constraints (e.g., usability and security policies) and enables the identification of variable assignments that satisfy the formula – effectively revealing the privileges and configurations under which an attack becomes feasible. Additionally, the solver can be used to determine minimal configurations and privilege distributions that prevent an attacker from successfully executing an attack.
In this study, we propose logical graph-based models for several types of typical attacks, the feasibility of which was validated in a controlled laboratory environment. Preventive measures against such cyber-physical attacks are also proposed. The corresponding logical attack graphs were converted into Boolean expressions, and scripts were developed using the z3-python SMT solver [16]. These scripts enabled the analysis of system configurations and privilege distributions that either permit or prevent the realization of the modeled attacks. This integration of graph-based modeling with formal verification techniques provides a novel and practical methodology for security analysis and risk mitigation in ICS environments.
To analyze the stages of typical cyberattacks, we use ICS laboratory, assembled as part of a project supported by USAID [17], which includes technological testbeds, which are built using standard hardware and software components commonly employed in industrial control systems. The technologies, communication protocols, and software-hardware tools used in these testbeds are designed to address a wide range of tasks within critical infrastructure environments. Laboratory testbeds include: ventilation and cooling system tubing with control devices; water tanks integrated with control system components; production line testbed equipped with Human-Machine Interface (HMI), production line platform, and IFM Safety system used for regulating the platform’s behavior in critical modes.
A structured summary of the examined attacks is presented in Table 1.
These include: 1. Direct packet injection using the S7COMM protocol [18]. By utilizing the Python library snap7 [19], it was possible to simulate the transmission of control commands to PLCs without authentication. For example, in the water level control system, the operational settings of the pump were altered. 2. Man-in-the-middle (MITM) attack via ARP poisoning, performed using the Ettercap tool. This attack enabled interception of all traffic between the operator and the controller, allowing data manipulation at the attacker’s discretion. In the cooling system, for instance, the fan speed could be increased to its maximum, potentially causing mechanical damage. 3. Remote Code Execution (RCE) on IFM controllers by exploiting an open Telnet port [20] with default credentials (target:target). This vulnerability allowed commands to be executed directly on the controller without interacting with the operator’s programming environment. 4. Supply Chain attack involving the insertion of a backdoor into the firmware. This attack scenario was examined in the context of a production line system. 5. Privilege Escalation, in which a vulnerability in the IFM controller kernel enabled the acquisition of superuser privileges.
MITM attack description. Initial Setup: 1. In the example of the laboratory training testbeds, the available local network infrastructure is illustrated in Figures 1-3. 2. The Control Center is a Windows 11 machine equipped with a communication panel for interacting with physical equipment, as well as a monitoring and control system for observing equipment parameters. 3. The PLC (Programmable Logic Controller) contains firmware that directly controls specific physical processes on the equipment and communicates with the Control Center over the network to receive commands and transmit operational data. 4. Additional Windows 11 machines in the network perform various user-level functions.
The system scenario corresponds to a configuration implemented in the laboratory environment. The Control Center and the PLC communicate via the S7Comm protocol. The physical equipment in this case includes air compressor, pump. The PLC maintains a database containing the current state of the equipment (e.g., pressure in a pipe, fluid level in a water tank, pump power, and the rules governing its adjustment). Operation of the physical devices is carried out through firmware functions on the PLC, which retrieve input arguments from this database.
The Control Center can read from and write to this database using the S7Comm protocol. This enables interaction between the operator’s graphical user interface (GUI) and the physical equipment. The original Control Center and PLC are software-protected, and the attacker does not have direct access to them – only network-level access.
The attacker’s scenario involves compromising a machine within the local network (Figure 1). In this setup, strict network policies (e.g., firewall rules) are either absent or have already been bypassed.
The objective of the attack is to gain control over the physical equipment without causing any noticeable changes in the graphical displays of the operator’s interface. The sequential steps of the attack are illustrated in Figures 2 and 3.
The attacker performs a Man-in-the-Middle (MITM) attack within the local network, placing themselves between the Control Center and the PLC (Figure 2). An ARP spoofing technique is used to impersonate each device to the other, enabling the interception and manipulation of all traffic exchanged between them. The attacker gains the ability to analyze the specifics of the communication protocol and to understand how internal communication between the Control Center and the PLC operates under the S7Comm protocol. As a result, the attacker identifies which memory cells in the PLC's internal database correspond to specific system parameters, as well as the functions transmitted by the Control Center.
The attacker either records a legitimate response packet from the PLC to a request issued by the Control Center or crafts a custom response packet based on the observed structure.
After analyzing intercepted traffic, the attacker crafts a malicious interface that mimics the legitimate Control Center, enabling unauthorized command injection and data spoofing without detection by the operator (Figure 3).
The attacker then reinitiates an active MITM attack (Figure 2). However, this time, any request issued by the Control Center is intercepted, and the attacker returns falsified status information – such as replaying a previously recorded valid state or injecting spoofed values that mask the actual behavior of the physical system.
IFM attack description. Another type of attack may be realized as a result of vulnerabilities [21], [22] present in certain embedded systems, such as the IFM Safety PLC, which receives signals from physical equipment and controls its behavior in the event of faults. Manufacturers frequently embed hardcoded credentials into the firmware of such devices to facilitate technical support, ease of deployment during production, legacy protocol compatibility, or other reasons. These credentials are typically immutable – logins are often identical across all devices, and passwords are either weak or follow predictable formats. Once network access to the device is gained, these credentials may be exploited by an attacker.
An example of such an attack is demonstrated for IFM security system, in a scenario where the firmware includes an active Telnet service running with root privileges. The attacker can use the hardcoded credentials to establish a Telnet session and gain elevated access to the system.
Upon obtaining administrative privileges, the attacker may modify the safety logic and overwrite the controller’s control program. For instance, this may involve disabling the emergency shutdown response, triggering false emergency reactions during normal operation, or disabling the processing of signals from visual indicators or motion sensors. The attacker may also disable relays responsible for stopping mechanical systems. In addition, the controller can be compromised by implanting malicious code, such as creating a hidden user account to maintain unauthorized access, or deploying a script that is triggered by a specific sensor reading or event.
Remarks: A known kernel-level vulnerability in the controller [23] – related to a race condition – enables local privilege escalation. Exploiting this vulnerability requires address space probing on the device. However, this is not always feasible, as the device has limited computational resources, and brute-force attempts may require several days. To mitigate such attacks, it is recommended to use cryptographically secured communication protocols (e.g., S7Comm+), wherever possible. Additionally, the implementation of appropriate traffic monitoring and filtering policies (e.g., SIEM (Security Information and Event Management) systems and network firewalls) within the local network is critical. As further countermeasures, firmware should be updated to patched versions that eliminate known vulnerabilities, remote access should be restricted or disabled entirely, and external authentication mechanisms should be employed to reinforce access control.
Attack using CaddyWiper malware description
To illustrate more sophisticated attacks that operate across multiple layers of the information and operational systems within a critical infrastructure environment, we examine a complex attack involving the CaddyWiper malware [24], which was specifically designed to target the Ukrainian energy sector [25].
A schematic representation of this attack across the layers of the Purdue Model for ICS Security is shown in Figure 4.
The attack sequence can be outlined with reference to the techniques classified under the MITRE ATT&CK framework.
The diagram (Figure 4) illustrates how the attack progresses from initial access (e.g., phishing, remote services) through lateral movement, malware execution, and impact, affecting both IT (Information Technology) and OT (Operation Technology) layers. Each stage corresponds to specific tactics and techniques as defined in the MITRE ICS matrix, highlighting the multi-layered nature of advanced persistent threats targeting critical infrastructure.
The Initial Access phase is achieved using a variety of techniques, given in [26]. For instance, adversaries may deploy CaddyWiper onto corporate devices with access to SCADA (Supervisory Control and Data Acquisition) systems via technique marked as T0865 (Spearphishing Attachment) [27], by sending phishing emails containing malicious documents. Initial access may also be obtained through T0822 (External Remote Services) [28], for example, by exploiting exposed RDP or VPN services using stolen credentials to gain access to SCADA engineering workstations. In cases where 71 insufficient attention is paid to supply chain security, T0862 (Supply Chain Compromise) [29] may be employed, whereby SCADA software updates or third-party contractors become vectors for malware injection. may be executed to sever SCADA components from control over field devices (e.g., pumps, turbines, generators).
The final phase focuses on anti-forensics and cover-up. This corresponds to T0872 (Indicator Removal on Host) [37], wherein CaddyWiper deletes itself after execution to avoid post-incident analysis. Additionally, T0809 (Data Destruction) is used to erase Historian server data, resulting in the loss of SCADA process history and depriving operators of critical event information.
The identification of vulnerabilities and insecure configurations that may be exploited by an attacker can be conducted in a semi-automated manner using network security scanning tools.
In this chapter, we present models of cyberattacks in the form of logical attack graphs. A logical attack graph is defined as = { , , ; }, where , , and are sets of vertices, and is the set of edges. The vertices
∈ represent direct exploits or attack actions. These nodes logically link the prerequisites (system configurations) to the consequences (privileges ∈ ) that the attacker may acquire.
The vertices ∈
denote system configurations, which may either reflect implemented cybersecurity measures or inherent system vulnerabilities. Graphically, the elements are represented as follows: (attacks) as ovals, (privileges) as diamonds, and (configurations) as rectangles.
When multiple edges lead into an attack vertex , the vertex functions as a logical AND (conjunction), indicating that all incoming conditions must be satisfied to enable the attack. In contrast, when multiple edges lead into a privilege vertex , it behaves as a logical OR (disjunction), meaning that the privilege can be gained if any of the conditions are met.
Privileges
may be acquired independently or as a result of exploiting vulnerable configurations. The attack vertices themselves are not explicitly included in the Boolean expressions, as they are considered intermediate steps resulting from prior conditions.
The overall outcome of an attack scenario is represented by a Boolean value : = = indicates that the attack is feasible under the given configurations and privileges. signifies that the attack is not possible under the current conditions.
Attack model with rogue control center. In the example of the attack graph involving a rogue control center, we illustrate a Man-in-the-Middle (MITM) attack executed via ARP poisoning. The corresponding logical attack graph is depicted in Figure 5.
The logical relationships within the graph can be expressed using the following Boolean formula: = ( ∨ ∨ ) ∧ ( ∨ ∨ ) ∧ ( ∨ ). (1)
Here, , , and are Boolean variables representing system configurations, attacker privileges, and attack actions, respectively. The operator ∧ denotes logical AND (conjunction), and ∨ denotes
In Figure 5, the graph models an attack on a PLC that combines ARP spoofing with a MITM logical OR (disjunction). technique. Specifically: : a device(s) with insecure configuration, : a device(s) with physical accessibility for the attacker, : a communication channel that allows injection of fake messages, : a communication path vulnerable to fake instruction injection, : a monitoring and detection system that lacks integrity verification of sensor data, : a vulnerability that permits triggering critical operating modes due to unauthenticated commands.
The privilege corresponds to the ability to sniff network traffic and identify the IP addresses of the operator and the PLC. Privilege represents the ability to impersonate a trusted sender.
The associated attacks include: : exploitation of vulnerable devices, : use of social engineering or similar methods to gain internal network access, : the ARP poisoning attack itself.
The graph (Figure 5) depicts the relationships between system configurations, attacker privileges, and the sequence of actions required to successfully compromise a PLC through ARP spoofing.
Rectangles represent system configurations, diamonds denote attacker privileges, and ovals indicate attack actions. Conjunctive and disjunctive logic is used to model dependencies between these elements.
Attack on IFM Safety system. An attack that exploits vulnerabilities in the hardware and software of the existing IFM security system is represented by the logical graph in Figure 6.
In this graph: denotes a vulnerability to external access; represents a configuration that is accessible from the local network; corresponds to insecure administrator access, such as default or weak credentials; indicates a configuration that permits the execution of system-level scripts, which can dangerously influence control logic; is a vulnerable configuration allowing external command execution; refers to a PLC configuration that enables the attacker to trigger overheating or other hazardous states.
The associated privileges are defined as follows: : Access to the internal network, such as via default network credentials or insecure services. : Access to system configuration files, achieved through administrator-level credentials (often hardcoded or poorly secured). : The critical privilege that allows the attacker to inflict physical harm on the system or disrupt its operation.
The attack actions include: : Exploitation of device vulnerabilities, allowing the attacker to extract internal system information. : Privilege escalation or kernel exploitation of the PLC, leading to deeper logical and physical intrusion into the system.
This attack model is especially relevant for water supply systems and industrial production lines that utilize IFM controllers, where such vulnerabilities can lead to serious safety and operational risks.
Access to configuration files is essential for understanding the internal logic of the system and for making unauthorized modifications to its behavior. The Boolean expression corresponding to the logical attack graph presented in Figure 6 is given by: = ( ∨ ∨ ) ∧ ( ∨ ∨ ∨ ) ∧ ( ∨ ).
(2)
The graph (Figure 6) models how an attacker can exploit vulnerabilities in network accessibility, administrative access, and PLC configurations to gain critical privileges. Rectangles denote system configurations (e.g., insecure remote access, weak credentials), diamonds represent attacker privileges (e.g., internal network access, control file extraction), and ovals correspond to specific attack actions. The logical structure illustrates how the combination of these factors may lead to system compromise and potential physical harm.
The attack model involving CaddyWiper malware. The attack model that leverages CaddyWiper malware can be represented using a logical graph, as illustrated in Figure 7, based on the structured stages of its execution. The corresponding Boolean expression for the attack feasibility is: = ( ∨ ∨ ∨ ) ∧ ( ∨ ∨ ) ∧ ( ∨ ∨ ) ∧ ( ∨ ∨ ) ∧ ( ∨ ∨ (3) ∨
∨ ).
The components used in equation (3) are defined as follows:
Initial Access and Infection: : Vulnerability to phishing attacks. : Insecure or compromised server account credentials with SCADA access. : Malware infection via SCADA software updates.
: Privilege to access SCADA systems.
SCADA Exploitation: Lateral Movement: : Critical vulnerabilities in SCADA components. : Vulnerability in the controller’s (PLC) web interface. : Privilege to manipulate SCADA data (e.g., hijacking or spoofing). : Propagation via Windows Management Instrumentation (WMI). : Propagation via Group Policy vulnerabilities.
: Privilege to propagate within the internal network.
Execution and Persistence: : Use of PowerShell or VBScript for malware deployment and activation. : Overwriting of the master boot record (MBR).
: Privilege to execute arbitrary code within SCADA environments.
Impact and Data Destruction: : Deletion of configuration files. : Deletion of system backup copies.
: Deletion of historian data from SCADA systems. : Privilege leading to loss of SCADA component control and disruption of industrial processes.
This model reflects a multi-stage, coordinated attack that targets critical infrastructure, demonstrating how combinations of vulnerabilities and acquired privileges can lead to severe operational consequences.
The graph (Figure 7) illustrates how a combination of vulnerabilities – ranging from phishing and software updates to SCADA misconfigurations – and attacker-acquired privileges can lead to full system compromise. Nodes in the graph represent system configurations (rectangles), attacker privileges (diamonds), and logical relationships among them. The structure captures multiple phases of the attack lifecycle, including initial access, lateral movement, malware execution, and impact on industrial processes, consistent with the Purdue Model.
We can analyze the formula using SAT/SMT solvers. These solvers require that the expressions be provided in Conjunctive Normal Form (CNF). The expressions must be represented in CNF. For , ,
this condition is satisfied.
In the computational experiment, the following problems were formulated: 1) Maximize the number of vulnerable configurations that remain active and/or maximize the number of privileges gained by the attacker, such that the expression evaluates to False, under the condition that certain vulnerable configurations always evaluate to True. These correspond to system vulnerabilities that cannot be mitigated. 2) Identify all combinations of configurations and privileges for which the formula evaluates to
True.
When solving problems 1) and 2), it is necessary to take into account the security policy constraints existing in the system. Such constraints may include: the inability to disable vulnerable services due to usability requirements, the inability to eliminate certain vulnerabilities because doing so would require updated hardware versions, or for other practical limitations. These constraints are also included as part of the SAT/SMT problem formulation. An example of input data is shown in Figure 8.
In Figure 9 the excerpt from the SAT/SMT solver output is shown. It is addressing the task of identifying all configuration and privilege combinations that allow the attack to succeed. As shown in Figure 9, the number of configuration combinations that allow the attack to be executed is large when the number of configurations and potential privileges is high. This list can be used to analyze the potential preconditions for a successful attack. Some of the combinations can be filtered out by setting input constraints on configuration values that are not vulnerable (i.e., set to False). (a) (b) (c)
The result of identifying the maximum number of configurations and privileges under which the attack becomes infeasible is shown in Figure 10. This type of analysis allows for the identification of specific configurations and privileges that must be adjusted to prevent the attack, without unnecessary reconfiguration of the system.
To prevent the attack based on ARP spoofing ( ), according to the logic of the SAT/SMT solver, it is sufficient that at least one element in the cyberattack chain – represented by a disjunction within parentheses – fails to hold. This can be minimally achieved by correcting the monitoring and detection subsystem ( ) – for example, by introducing redundant observation channels or by establishing reference values to detect anomalies artificially created by the attacker. Additionally, it is necessary to prevent the ability to activate critical operating modes that could damage physical components ( ). This requires the implementation of mechanical safeguards and local control of critical parameters at the device level.
In other scenarios, a greater number of corrections may be required, which could involve revoking user privileges and potentially conflict with the system’s usability policy. In this example, = , meaning that it is not feasible to eliminate all insecurely configured devices with access to external networks. Similarly, = indicates that integrity checks for messages cannot be implemented due to the lack of cryptographic verification tools on relevant devices and in the communication protocols used.
For the attack on the IFM security system ( ), the minimal corrective strategy involves modifying the vulnerable PLC configuration ( ) that may expose configuration data and revoking privilege , which allows PLC reconfiguration during runtime. The computation was performed under the constraint = , which represents access with default credentials. Unfortunately, this cannot be mitigated because the credentials are hardcoded into the devices' firmware.
The general methodology of critical infrastructure network assessment is represented in the form of pseudocode (Figure 11). The Figure 11 outlines the step-by-step process: from modeling attacks and identifying system configurations and privileges, to formulating Boolean expressions, transforming them into Conjunctive Normal Form (CNF), and solving them to evaluate attack feasibility. The output supports decision-making by identifying vulnerable configurations and suggesting minimal corrective actions to enhance system security.
The proposed methodology was validated on three real-world attack models and approved in practical experiments on laboratory testbeds. For each attack, we computed minimal sets of configuration changes required to block the attack using Z3. It is much less than the total number of vulnerable combinations and configurations combinations, which lead to = . These characteristics and solver performance are summarized in Table 2.
Additionally, using expressions (1)-(3), we can analyze dependence of attack feasibility probability on the number of vulnerable configurations and privileges { , }, which characterizes the general system resilience. The results are presented in Figure 12 for and respectively. Each point represents the fraction of true Z3 outcomes over 100 random samples with active variables.
The scripts developed for conducting the computer experiment are presented in [38].
By reviewing the solver’s suggestions, a system administrators can form their own judgment about which changes should be implemented. The solver provides a formal estimate of the minimal set of configurations and/or privileges that need to be modified to render the attack infeasible. However, due to financial or other practical considerations, it may be more feasible to apply alternative changes. Therefore, the administrator should also analyze other viable options. The SAT/SMT solver facilitates this process by producing a structured list of all vulnerable configuration combinations that make the attack possible, enabling the selection of the most appropriate variant for system reconfiguration.
The proposed models, constructed in the form of logical graphs, enable a comprehensive reconstruction of cyberattacks, allowing for the analysis of their impact on ICS components. These models facilitate the identification of weak configurations and the necessary conditions that enable successful attacks. An analysis of typical attack graphs across various ICS elements reveals that reducing the attack surface requires minimizing the number of communication channels that could potentially be exploited. Additionally, the number of vulnerable devices should be reduced by upgrading them to more secure alternatives. Wherever feasible, cryptographic mechanisms should (c)
Figure 12: Probability of successful attack realization ( = True) depending on the number of active (vulnerable) system configurations and privileges: (a) , (b) , (c) . be employed to ensure authentication and integrity of control and monitoring messages. Physical safeguards, such as mechanical fuses, should also be considered to prevent systems from entering unsafe operational states.
The proposed methodology allows for the detection of critical system configurations and provides a list of minimally required changes to block potential attack paths. The integration of SAT/SMT solvers into this process enables automation of the analysis and configuration evaluation. The developed solver scripts serve as a practical tool to assist security administrators in making informed decisions.
Ultimately, timely reconfiguration of ICS environments, based on the identified attack vectors, enables proactive defense. This approach helps to anticipate possible infection, propagation, and persistence mechanisms used by advanced malware, thereby strengthening the system’s overall cybersecurity posture.
We thank the students of the Institute of Physics and Technology – Yurii Prykhodko, Oleksii Bondarenko, and Dmytro Krygin – for their assistance with the laboratory testbed experiments.
During the preparation of this work, the authors used GPT-4o in order to make grammar and style check. After using this tool, the authors reviewed and edited the content and take full responsibility for the publication’s content.