Static Code Analysis of IEC 61131–3 ST Programs via Symbolic Execution

A Programmable Logic Controller (PLC) is an essentially domain-specific computer used to control physical equipment and is widely used in industrial control fields. It plays a crucial role in automating complex processes for industrial automation systems, requiring high reliability as code vulnerabilities can potentially lead to disasters. Therefore, vulnerability detection in PLC programs is of significant importance. However, the availability of tools supporting vulnerability detection in PLC programming languages is limited. This paper attempts to improve industrial security from the perspective of code security and proposes a static code analysis approach specifically designed for IEC 61131–3 Structured Text (ST) programs. This approach uses structural pattern matching and symbolic execution technology to identify program defects and improve quality by detecting problematic code structures and potential issues early in the development process, thereby reducing the debugging effort required during developments. Considering the characteristic of periodic loop execution in PLCs, we introduce the loop unwinding technique to collect constraints from subsequent execution cycles for detection purposes. Based on the aforementioned approach, we implement a static code analysis tool, ST-Checker and make a series of evaluations. The experimental results show that this method is feasible and can detect potential defects that existing PLC compilers cannot detect, improving the precision of defect detection with data dependencies.