InstruPro: Instrumenting Programmable Logic Controller (PLC) based on Model Checking

Programmable Logic Controller (PLC) suffers from various types of attacks due to misconfiguration in its logic system. These misconfigurations cannot be found by looking at the logic/rules only. Therefore, we propose a methodology where temporal logic is used to find the misconfigurations in the subsequent rules. Our framework is capable of finding the codes in PLC that are responsible for abnormal behavior in PLC. Having accomplished that, an automated approach to instrument the code. We run our methodology on some real world PLC program applications and found that our approach can eradicate a good number of abnormal behaviors successfully.