Binary-Level Formal Verification Based Automatic Security Ensurement for PLC in Industrial IoT

Currently, the security of the control logic of Programmable Logic Controllers (PLCs) is facing a serious threat, significantly impacting industrial production. Consequently, ensuring the security of PLC control logic becomes imperative. Formal verification emerges as a promising methodology for verifing PLC security through behavioral modeling and security testing. However, existing formal verification approaches primarily focus on modeling the PLC source code, overlooking the identification of compile-time errors and real-time runtime logic checks. Therefore, it is essential to apply formal verification to PLC control logic at the binary level. In this study, we introduce VoICS, a system designed to facilitate binary-level formal verification. Using reverse engineering, VoICS automatically parses PLC programs written by various programming languages at the binary level and constructs control flow graphs (CFGs). Furthermore, we use an algorithm combining two model optimization methods (i.e., trim invalid states and unnecessary states compression) to convert the reversed PLC assembly program into nuXmv format model. Lastly, VoICS establishes the corresponding constraints and performs formal verification on the model using nuXmv. The evaluation results demonstrate the capability of VoICS in identifying instances of unreliable control logic within PLC control programs, thus reinforcing the dependability of the industrial automation system.