A malware detection method for checking PLC system using satisfiability modulus theoretical model

One 、 Abstract

In this paper, a model-based detection method is proposed PLC Malware detection method .PLC Malware is highly customized for the target , Therefore, it is difficult to extract general patterns to detect them , In this paper, a model-based detection method is proposed PLC Malware detection method . We are based on SMT Our model can handle PLC Characteristics of the system , If the input signal is uncertain 、 Edge detection, etc . secondly , For malware detection , Two detection rule generation methods are proposed ： Invariant extraction and rule design patterns . The former can extract invariants from the original program , The latter can reduce the threshold for users to design detection rules . Last , We implemented a prototype , And in three representative ICS It is evaluated in the scenario . The evaluation results show that , Our method can successfully detect malware with four attack modes .

Two 、 Model design

In this paper , We propose a satisfiability modulus theory （SMT） Model checking method to detect PLC Malware .

1. The first stage is detection rule generation . To detect malware , We need to define white lists or rules . In our plan , This work is completed by the engineer of the target control system . These rules are expressed as temporal logic formulas .
2. The second stage is PLC modeling . Our goal is PLC And field control systems , So we model its behavior from internal code . Whenever a target is detected , We must all start from the goal PLC Extract bytecode , And generate constraint based models （smv Format ） As input to the model checker .
3. After the model is generated , You can verify whether the model meets the rules .nuXmv The model checker is used to handle detection . If the model cannot satisfy one of the rules , It means that there is a violation of normal behavior , And malware is detected .

3、 ... and 、 Concrete realization

（ One ） Generate detection rules

1. Invariant extraction

The first method is from the original PLC Invariants are automatically extracted from the program . The original program is written by the engineer and downloaded to PLC The program , It can be considered reliable . Although the original program may have several different versions （ Due to system evolution or code modification ）, But they should share some common behaviors .19 for example , These procedures should follow the same safety requirements . Invariants in one of the programs can represent some common behaviors as detection rules . In practice , We use the program in the engineering station as the original program , And run in PLC The program on .

2. Rule design pattern

The second method is rule design pattern , It instructs engineers to define inspection rules . The design pattern is to use LTL Template of formula description . Engineers can only focus on rule design , instead of LTL The details of the formula . The pattern should be simple enough , Let engineers understand , Attack strategies should also be covered .

（ Two ） be based on SMT Of PLC modeling

SMT Model checking can be seen as SAT An extension of , Replace propositional logic with first-order logic . Bounded model checking （BMC） And unbounded model checking （UMC） yes SMT Two main methods of model checking .
Based on SMT Model checking of , We need to construct constraints for the model and solve . Modern model checker （ Such as NuSMV and nuXmv） It can support constraint based modeling , This will help to model uncertain input sequences and initial states .
In this paper , We choose nuXmv Model the system and check the rules .nuXmv Is a new symbolic model checker , It can support the use of multiple BMC technology SMT Model check .

Four 、 summary

Our model integrates programs and processes , Can reduce false positives . Most other work takes source code as input , Our method can analyze binary files , So as to directly detect malware . Besides , We also decompose binary languages into STL Language , To support programs written in other languages （ In the evaluation , Support LAD and SCL）. By using based on SMT Model check for , Our method can deal with Boolean 、 Integer and floating point data types , And support the timer 、 Modeling counters and functions , In order to model the accurate system behavior . Unlike other jobs , We provide variable extraction to automatically generate detection rules , Users will benefit . These improvements are feasible for users to detect malware .

Our goal is to tamper PLC Malware that controls logical attacks on physical devices , We also note that there are other types PLC Malware . some PLC Malware will not attack the system , Instead, it acts as a back door , Infiltrate the system and spread worms . some PLC Malware tampers with firmware rather than control logic , To carry out low-level secret attacks . To detect these malware , We will combine our method with firmware and network traffic analysis technology .

This paper proposes a new method based on SMT Model checking PLC Malware detection method . We have given PLC Model check 、PLC Formal definitions of procedures and industrial processes .PLC The problem with model checking is , We must enumerate all possible input signal sequences to construct a state transition diagram . Use SMT Modeling the system with constraints instead of state transition diagrams , And use SMT The model checker checks properties . The advantage of this method is that it can deal with uncertain input signals . We also propose two methods , Invariant extraction and rule design patterns , To reduce the difficulty of designing detection rules .

1. Berger H.Automating with STEP 7 in STL and SCL: Programmable Controllers SIMA TIC S7-300/400. Hoboken, NJ: John Wiley & Sons; 2012.
2. Beresford BD. Exploiting siemens simatic S7 PLCs.Black Hat. 2011.
3. Klick J, Lau S, Marzin D, Malchow JO, Roth V. Internet-facing PLCs as a network backdoor.Commun Netw Sec. 2015;2015:524-532.
4. Gjendemsjø M. Creating a Weapon of Mass Disruption: Attacking Programmable Logic Controllers (Master's thesis). Norwegian University of Science
and T echnology; 2013.
5. T zokatziou G, Maglaras L, Janicke H. Insecure by design: using human interface devices to exploit SCADA systems. Paper presented at: Proceedings of
the 3rd International Symposium for ICS & SCADA Cyber Security Research; 2015:103-106; BCS Learning & Development Ltd.
6. Milinkovíc SA, Lazíc LR. Industrial PLC security issues. Paper presented at: Proceedings of the 2012 20th T elecommunications Forum (TELFOR);
2012:1536-1539; IEEE.
7. Falliere N, Murchu LO, Chien E. W32. stuxnet dossier . tech. rep., Symantec Corperation; 2011.
8. Vávra, J., & Hromada, M. An evaluation of cyber threats to industrial control systems. Paper presented at: Proceedings of the International Conference
on Military T echnologies; 2015:1-5; IEEE.
9. Moser A, Kruegel C, Kirda E. Limits of static analysis for malware detection.ACSAC Comput Sec Appl Conf. 2007;2007:421-430.
10. Mclaughlin S, Mcdaniel P. SABOT :specification-based payload generation for programmable logic controllers. Paper presented at: Proceedings of the
2012 ACM Conference on Computer and Communications Security; 2012:439-449; ACM.
11. Mohan S, Bak S, Betti E, Y un H, Sha L, Caccamo M. S3A: Secure system simplex architecture for enhanced security and robustness of cyber-physical
systems. Paper presented at: Proceedings of the 2nd ACM International Conference on High Confidence Networked Systems; 2013:65-74; ACM.
12. John KH, Tiegelkamp M.IEC 61131-3: Programming Industrial Automation Systems Concepts and Programming Languages, Requirements for Programming
Systems, Decision-Making Aids. Berlin, Heidelberg / Germany: Springer; 2010.
13. Clarke EM, Grumberg O, Peled DA.Model Checking. Berlin, Heidelberg / Germany: Springer; 1997.
14. Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y. Symbolic model checking using SA T procedures instead of BDDs. Paper presented at: Proceedings of the
1999 Design Automation Conference; 1999:317-320; IEEE.
15. De Moura L, Rner N. Satisfiability modulo theories: introduction and applications.Commun ACM. 2011;54(9):69-77. https:/ /doi.org/10.1145/1995376.
1995394.
16. Allen FE. Control flow analysis.ACM SIGPLAN Not. 1970;5(7):1-19.
17. McLaughlin SE. On dynamic malware payloads aimed at programmable logic controllers. Paper presented at: Proceedings of the 6th USENIX Workshop
on Hot T opics in Security . USENIX. HotSec 2011.
18. Langner R. A time bomb with fourteen bytes. http:/ /www.langner .com/en/2011/07/21/a-time-bomb-with-fourteen-bytes/; 2011.
19. Beckert B, Ulbrich M, V ogel-Heuser B, Weigl A. Regression verification for programmable logic controller software. Paper presented at: Proceedings of
the International Conference on Formal Engineering Methods; 2015: 234-251; Springer .
20. Huuck R. Semantics and analysis of instruction list programs.Electr Notes Theoret Comput Sci. 2005;115:3-18. https:/ /doi.org/10.1016/j.entcs.2004.09.
026.
21. Biallas S, Brauer J, Kowalewski S. Arcade. PLC: a verification platform for programmable logic controllers. Paper presented at: Proceedings of the 2012
Proceedings of the 27th IEEE/ ACM International Conference; 2012: 338-341
22. McLaughlin SE, Zonouz SA, Pohly DJ, McDaniel PD.A T rusted Safety V erifier for Process Controller Code. V ol 14. San Diego, CA: NDSS; 2014.
23. Darvas D, Blanco VE, Fernández AB. PLCverif: a tool to verify PLC programs based on model checking techniques. Paper presented at: Proceedings of
the 15th International Conference on Accelerator and Large Experimental Physics Control Systems; 2015:911-915.
24. Spenneberg R, Brüggemann M, Schwartke H. Plc-blaster: a worm living solely in the plc.Black Hat Asia. 2016.
25. Abbasi A, Hashemi M. Ghost in the plc designing an undetectable programmable logic controller rootkit via pin control attack.Black Hat Europe.
2016;2016:1-35.
26. Garcia L, Brasser F, Cintuglu MH, Sadeghi AR, Mohammed OA, Zonouz SA.Hey , My Malware Knows Physics!Attacking PLCs with Physical Model Aware Rootkit.
San Diego, CA: NDSS; 2017.
27. Meng W, Li W, Wang Y, Au MH. Detecting insider attacks in medical cyber-physical networks based on behavioral profiling.Futur Gener Comput Syst.
2018. https:/ /doi.org/10.1016/j.future.2018.06.007.
28. Wang Y, Meng W, Li W, Liu Z, Liu Y, Xue H. Adaptive machine learning-based alarm reduction via edge computing for distributed intrusion detection
systems.Concurr Comput Pract Exp. 2019;31(19):1-12. https:/ /doi.org/10.1002/cpe.5101.
29. Y oo H, Kalle S, Smith J, Ahmed I. overshadow PLC to detect remote control-logic injection attacks. Paper presented at: Proceedings of the 2019
International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment; 2019:109-132; Springer .
30. Keliris A, Maniatakos M. ICSREF: a framework for automated reverse engineering of industrial control systems binaries. Paper presented at: Proceedings
of the Network and Distributed Systems Security (NDSS) Symposium; 2019; NDSS.
31. Pavlovic O, Pinger R, Kollmann M. Automated formal verification of PLC programs written in IL. Paper presented at: Proceedings of the 2007 Conference
on Automated Deduction; 2007:152-163; CADE.
32. Schlich B, Brauer J, Wernerus J, Kowalewski S. Direct model checking of PLC programs in IL.IF AC Proc V ol. 2009;42(5):28-33.
33. Darvas D, Adiego BF, Vörös A, Bartha T, Viñuela EB, Suárez VMG. Formal verification of complex properties on PLC programs. Paper presented at:
Proceedings of the International Conference on Formal T echniques for Distributed Objects, Components, and Systems; 2014:284-299; Spring.
34. Zonouz S, Rrushi J, McLaughlin S. Detecting industrial control malware using automated PLC code analytics.IEEE Secur Priv. 2014;12(6):40-47. https:/ /
doi.org/10.1109/MSP .2014.113.
35. Stattelmann S, Biallas S, Schlich B, Kowalewski S. Applying static code analysis on industrial controller code. Paper presented at: Proceedingsof the 2014
IEEE Emerging T echnology and Factory Automation (ETF A); 2014:1-4; IEEE.
36. Malchow JO, Marzin D, Klick J, Kovacs R, Roth V. Plc guard: a practical defense against attacks on cyber-physical systems. Paper presented at:
Proceedings of the 2015 IEEE Communications and Network Security (CNS); 2015:326-334; IEEE.