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

• 一、摘要
• 二、模型設計
• 三、具體實現
• • （一）生成檢測規則
  • • 1.不變提取
    • 2.規則設計模式
  • （二）基于SMT的PLC建模
• 四、總結

一、摘要

本文提出了一種基于模型檢測的PLC惡意軟件檢測方法。PLC惡意軟件是針對目標高度定制的，因此很難提取通用模式來檢測它們，本文提出了一種基于模型檢測的PLC惡意軟件檢測方法。我們基于SMT的模型可以處理PLC系統的特征，如輸入信號不確定、邊緣檢測等。其次，針對惡意軟件檢測問題，提出了兩種檢測規則生成方法：不變量提取和規則設計模式。 前者可以從原始程序中提取不變量，后者可以降低用戶設計檢測規則的門檻。最后，我們實現了一個原型，并在三個具有代表性的ICS場景中對其進行了評估。評估結果表明，我們提出的方法可以成功地檢測出四種攻擊模式的惡意軟件。

二、模型設計

在本文中，我們提出了一種可滿足性模數理論（SMT）模型檢查方法來檢測PLC惡意軟件。

第一階段是檢測規則生成。為了檢測惡意軟件，我們需要定義白名單或規則。在我們的方案中，這項工作由目標控制系統的工程師完成。這些規則表示為時態邏輯公式。

第二階段為PLC建模。我們的目標是PLC和現場控制系統，因此我們從內部代碼對其行為進行建模。無論何時檢測到目標，我們都必須從目標PLC提取字節碼，并生成基于約束的模型（smv格式）作為模型檢查器的輸入。

模型生成后，可以驗證模型是否滿足規則。nuXmv模型檢查器用于處理檢測。如果模型不能滿足其中一條規則，則表示發生了違反正常行為的行為，并檢測到惡意軟件。

三、具體實現

（一）生成檢測規則

1.不變提取

第一種方法是從原始PLC程序中自動提取不變量。原始程序是指由工程師編寫并下載到PLC的程序，可以認為是可靠的。雖然原始程序可能有幾個不同的版本（由于系統進化或代碼修改），但它們應該共享一些共同的行為。19例如，這些程序應遵循相同的安全要求。其中一個程序中的不變量可以表示作為檢測規則的部分常見行為。在實踐中，我們使用工程站中的程序作為原始程序，并以運行在PLC上的程序為目標。

2.規則設計模式

第二種方法是規則設計模式，它指導工程師定義檢測規則。設計模式是使用LTL公式描述的模板。工程師只能專注于規則設計，而不是LTL公式的細節。模式應該足夠簡單，讓工程師能夠理解，還應該涵蓋攻擊策略。

（二）基于SMT的PLC建模

SMT模型檢驗可以看作SAT的一個擴展，用一階邏輯代替命題邏輯。有界模型檢查（BMC）和無界模型檢查（UMC）是SMT模型檢查的兩種主要方法。
在基于SMT的模型檢查中，我們需要為模型構造約束并進行求解。現代模型檢查器（如NuSMV和nuXmv）可以支持基于約束的建模，這將有助于對不確定的輸入序列和初始狀態進行建模。
在本文中，我們選擇nuXmv對系統進行建模并檢查規則。nuXmv是一種新的符號模型檢查器，它可以支持使用多個BMC技術的SMT模型檢查。

四、總結

我們的模型集成了程序和過程，可以減少誤報。其他大多數工作都以源代碼為輸入，我們的方法可以分析二進制文件，從而直接檢測惡意軟件。此外，我們還將二進制語言分解為STL語言，以支持其他語言編寫的程序（在評估中，支持LAD和SCL）。通過使用基于SMT的模型檢查，我們的方法可以處理布爾、整數和浮點數據類型，并支持對計時器、計數器和函數進行建模，以便于對準確的系統行為進行建模。與其他工作不同，我們提供了變量提取來自動生成檢測規則，用戶將從中受益。這些改進對于用戶檢測惡意軟件是切實可行的。

我們的目標是篡改PLC控制邏輯攻擊物理設備的惡意軟件，我們還注意到存在其他類型的PLC惡意軟件。一些PLC惡意軟件不會攻擊系統，而是充當后門，滲透系統并傳播蠕蟲。一些PLC惡意軟件篡改固件而不是控制邏輯，以執行低級秘密攻擊。為了檢測這些惡意軟件，我們將把我們的方法與固件和網絡流量分析技術結合起來。

本文提出了一種基于SMT模型檢測的PLC惡意軟件檢測方法。我們給出了PLC模型檢查、PLC程序和工業過程的正式定義。PLC模型檢查的問題是，我們必須枚舉所有可能的輸入信號序列來構造狀態轉移圖。使用SMT約束代替狀態轉移圖對系統建模，并使用SMT模型檢查器檢查屬性。該方法的優點是可以處理不確定的輸入信號。我們還提出了兩種方法，不變抽取和規則設計模式，以降低設計檢測規則的難度。

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. Milinkovi?c SA, Lazi?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.

總結

以上是生活随笔為你收集整理的一种使用可满足性模数理论模型检查可编程逻辑控制器系统的恶意软件检测方法的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。