A model-checking approach that uses a translation of Rockwell’s Ladder Diagrams into an equivalent formal model, on which a set of automatic analysis can be performed. These analysis include checking for logic equivalence and automated test generation, offering benefits in critical environments for detecting malicious or unexpected code behaviors. This research suggests that the use of static analysis techniques for PLC programs needs to be further pushed in order to obtain more secure and reliable programs.
One of the most effective techniques to disrupt a critical industrial processes is to inject PLCs with malicious code. A threat actor gaining access to an Engineering Station may load a program designed to change the process logic or disable security features involved in critical operations. While many general-purpose programming languages nowadays rely on static analysis tools to help with the analysis of memory errors or other security flaws, this is much less the case for PLCs languages and IDEs. So when will we see endpoint detection and response in PLC's?
Speaker: Roberto Bruttomesso, Software Engineer Coordinator