A malware detection method using satisfiability modulo theory model checking for the programmable logic controller system

Abstract

Summary Nowadays programmable logic controllers (PLCs) are suffering increasing cyberattacks. Attackers could reprogram PLCs to inject malware that would cause physical damages and economic losses. These PLC malwares are highly customized for the target which makes it difficult to extract a general pattern to detect them. In this article, we propose a PLC malware detection method based on model checking. Firstly, we improve the existing modeling method for PLC system by using the Satisfiability Modulo Theory (SMT) constraints to model the PLC system. We also present an algorithm that can transform the PLC program to the model. Our SMT‐based model can deal with the features of the PLC system such as undetermined input signals, edge detection and so on. Secondly, we focus on malware detection and propose two methods, invariant extraction and rule design pattern, to generate detection rules. The former can extract the invariants from an original program, and the latter can lower the bar for user to design detection rules. Finally, we implement a prototype and evaluate it on three representative ICS scenarios. The evaluation result shows that our proposed method can successfully detect the malwares using four attack patterns.