Проверка модели для обнаружения атак в реальном времени в системах распределения воды
Ключевые слова:
критическая инфраструктура, SCADA, формальная среда верификации, формальные методы, таймер, безопасность, охранаАннотация
Системы распределения воды представляют собой критическую инфраструктуру. Эти архитектуры очень важны, и нестандартное поведение может отразиться на безопасности человека. Фактически, злоумышленник, получивший контроль над такой архитектурой, может нанести множество повреждений как инфраструктуре, так и людям. В этой статье мы предлагаем подход к выявлению нестандартного поведения, ориентированного на системы распределения воды. Разработанный подход рассматривает формальную среду проверки. Журналы, полученные из систем распределения воды, анализируются в формальную модель, и, используя временную логику, мы характеризуем
поведение системы распределения воды во время атаки. Оценка, относящаяся к системе распределения воды, подтвердила эффективность разработанного подхода при выявлении трех различных нестандартных режимов работы.
Литература
1. S. Cheruvu, A. Kumar, N. Smith, and D.M. Wheeler, “Conceptualizing the secure internet of things,” in Demystifying Internet of Things Security, pp. 1–21, Springer, 2020.
2. K. Jia, J. Xiao, S. Fan, and G. He, “A mqtt/mqtt-sn-based user energy management system for automated residential demand response: Formal verification and cyber-physical performance evaluation,” Applied Sciences, vol. 8, no. 7, p. 1035, 2018.
3. S.A. Boyer, SCADA: supervisory control and data acquisition. International Society of Automation, 2009.
4. B. Miller and D.C. Rowe, “A survey scada of and critical infrastructure incidents.,” RIIT, vol. 12, pp. 51–56, 2012.
5. R. Taormina, S. Galelli, N.O. Tippenhauer, E. Salomons, A. Ostfeld, D.G. Eliades, M. Aghashahi, R. Sundararajan, M. Pourahmadi, M.K. Banks, et al., “Battle of the attack detection algorithms: Disclosing cyber attacks on water distribution networks”, Journal of Water Resources Planning and Management, vol. 144, no. 8, p. 04018048, 2018.
6. P.K. Hajoary and K. Akhilesh, “Role of government in tackling cyber security threat,” in Smart Technologies, pp. 79–96, Springer, 2020.
7. R. Meyur, “A bayesian attack tree based approach to assess cyber-physical security of power system,” in 2020 IEEE Texas Power and Energy Conference (TPEC), pp. 1–6, IEEE, 2020.
8. I.N. Fovino, A. Carcano, M. Masera, and A. Trombetta, “An experimental investigation of malware attacks on scada systems,” International Journal of Critical Infrastructure Protection, vol. 2, no. 4, pp. 139–145, 2009.
9. A. Carcano, I.N. Fovino, M. Masera, and A. Trombetta, “Scada malware, a proof of concept,” in International Workshop on Critical Information Infrastructures Security, pp. 211–222, Springer, 2008.
10. T. Alladi, V. Chamola, and S. Zeadally, “Industrial control systems: Cyberattack trends and countermeasures,” Computer Communications, 2020.
11. F. Daryabar, A. Dehghantanha, N.I. Udzir, S. bin Shamsuddin, et al., “Towards secure model for scada systems,” in Proceedings Title: 2012 International Conference on Cyber Security, Cyber Warfare and Digital Forensic (CyberSec), pp. 60–64, IEEE, 2012.
12. T. Wu, J.F.P. Disso, K. Jones, and A. Campos, “Towards a scada forensics architecture,” in 1st International Symposium for ICS & SCADA Cyber Security Research 2013 (ICS-CSR 2013) 1, pp. 12–21, 2013.
13. D. Upadhyay and S. Sampalli, “Scada (supervisory control and data acquisition) systems: Vulnerability assessment and security recommendations,” Computers & Security, vol. 89, p. 101666, 2020.
14. M. Gaiceanu, M. Stanculescu, P.C. Andrei, V. Solcanu, T. Gaiceanu, and H. Andrei, “Intrusion detection on ics and scada networks,” in Recent Developments on Industrial Control Systems Resilience, pp. 197–262, Springer, 2020.
15. M.G. Cimino, N. De Francesco, F. Mercaldo, A. Santone, and G. Vaglini, “Model checking for malicious family detection and phylogenetic analysis in mobile environment,” Computers & Security, vol. 90, p. 101691, 2020.
16. L. Brunese, F. Mercaldo, A. Reginelli, and A. Santone, “Formal methods for prostate cancer gleason score and treatment prediction using radiomic biomarkers,” Magnetic resonance imaging, vol. 66, pp. 165–175, 2020.
17. L. Brunese, F. Mercaldo, A. Reginelli, and A. Santone, “An ensemble learning approach for brain cancer detection exploiting radiomic features,” Computer methods and programs in biomedicine, vol. 185, p. 105134, 2020.
18. L. Brunese, F. Mercaldo, A. Reginelli, and A. Santone, “Prostate gleason score detection and cancer treatment through real-time formal verification,” IEEE Access, vol. 7, pp. 186236–186246, 2019.
19. F. Mercaldo, F. Martinelli, and A. Santone, “Real-time scada attack detection by means of formal methods,” in 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp. 231–236, IEEE, 2019.
20. R. Alur and D. Dill, “Automata for modeling real-time systems,” in International Colloquium on Automata, Languages, and Programming, pp. 322–335, Springer, 1990.
21. R. Alur and D.L. Dill, “A theory of timed automata,” Theoretical computer science, vol. 126, no. 2, pp. 183–235, 1994.
22. G. Behrmann, K.G. Larsen, O. Moller, A. David, P. Pettersson, and W. Yi, “Uppaal-present and future,” in Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No. 01CH37228), vol. 3, pp. 2881–2886, IEEE, 2001.
23. G. Behrmann, A. David, and K.G. Larsen, “A tutorial on uppaal 4.0,”Department of computer science, Aalborg university, 2006.
24. G. Behrmann, A. David, and K.G. Larsen, “A tutorial on uppaal,” in Formal methods for the design of real-time systems, pp. 200–236, Springer, 2004.
25. P. Bouyer, “Model-checking timed temporal logics,” Electronic Notes in Theoretical Computer Science, vol. 231, pp. 323–341, 2009.
26. E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 8, no. 2, pp. 244–263, 1986.
27. N.D. Francesco, G. Lettieri, A. Santone, and G. Vaglini, “Heuristic search for equivalence checking,” Software and System Modeling, vol. 15, no. 2, pp. 513–530, 2016.
28. H.E. Jensen, K.G. Larsen, and A. Skou, “Scaling up uppaal,” in International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 19–30, Springer, 2000.
29. J. Dougherty, R. Kohavi, and M. Sahami, “Supervised and unsupervised discretization of continuous features,” in Machine Learning Proceedings 1995, pp. 194–202, Elsevier, 1995.
30. F. Mercaldo and A. Santone, “Deep learning for image-based mobile malware detection,” Journal of Computer Virology and Hacking Techniques, pp. 1–15, 2020.
31. A. De Lorenzo, F. Martinelli, E. Medvet, F. Mercaldo, and A. Santone, “Visualizing the outcome of dynamic analysis of android malware with vizmal,” Journal of Information Security and Applications, vol. 50, p. 102423, 2020.
32. R. Taormina, S. Galelli, N.O. Tippenhauer, A. Ostfeld, and E. Salomons, “Assessing the effect of cyber-physical attacks on water distribution systems,” in World Environmental and Water Resources Congress 2016, pp. 436–442, 2016.
33. E. Salomons and A. Ostfeld, “Simulation of cyber-physical attacks on water distribution systems with epanet,” in Proceedings of the Singapore Cyber-Security Conference (SGCRC) 2016: Cyber-Security by Design, vol. 14, p. 123, 2016.
2. K. Jia, J. Xiao, S. Fan, and G. He, “A mqtt/mqtt-sn-based user energy management system for automated residential demand response: Formal verification and cyber-physical performance evaluation,” Applied Sciences, vol. 8, no. 7, p. 1035, 2018.
3. S.A. Boyer, SCADA: supervisory control and data acquisition. International Society of Automation, 2009.
4. B. Miller and D.C. Rowe, “A survey scada of and critical infrastructure incidents.,” RIIT, vol. 12, pp. 51–56, 2012.
5. R. Taormina, S. Galelli, N.O. Tippenhauer, E. Salomons, A. Ostfeld, D.G. Eliades, M. Aghashahi, R. Sundararajan, M. Pourahmadi, M.K. Banks, et al., “Battle of the attack detection algorithms: Disclosing cyber attacks on water distribution networks”, Journal of Water Resources Planning and Management, vol. 144, no. 8, p. 04018048, 2018.
6. P.K. Hajoary and K. Akhilesh, “Role of government in tackling cyber security threat,” in Smart Technologies, pp. 79–96, Springer, 2020.
7. R. Meyur, “A bayesian attack tree based approach to assess cyber-physical security of power system,” in 2020 IEEE Texas Power and Energy Conference (TPEC), pp. 1–6, IEEE, 2020.
8. I.N. Fovino, A. Carcano, M. Masera, and A. Trombetta, “An experimental investigation of malware attacks on scada systems,” International Journal of Critical Infrastructure Protection, vol. 2, no. 4, pp. 139–145, 2009.
9. A. Carcano, I.N. Fovino, M. Masera, and A. Trombetta, “Scada malware, a proof of concept,” in International Workshop on Critical Information Infrastructures Security, pp. 211–222, Springer, 2008.
10. T. Alladi, V. Chamola, and S. Zeadally, “Industrial control systems: Cyberattack trends and countermeasures,” Computer Communications, 2020.
11. F. Daryabar, A. Dehghantanha, N.I. Udzir, S. bin Shamsuddin, et al., “Towards secure model for scada systems,” in Proceedings Title: 2012 International Conference on Cyber Security, Cyber Warfare and Digital Forensic (CyberSec), pp. 60–64, IEEE, 2012.
12. T. Wu, J.F.P. Disso, K. Jones, and A. Campos, “Towards a scada forensics architecture,” in 1st International Symposium for ICS & SCADA Cyber Security Research 2013 (ICS-CSR 2013) 1, pp. 12–21, 2013.
13. D. Upadhyay and S. Sampalli, “Scada (supervisory control and data acquisition) systems: Vulnerability assessment and security recommendations,” Computers & Security, vol. 89, p. 101666, 2020.
14. M. Gaiceanu, M. Stanculescu, P.C. Andrei, V. Solcanu, T. Gaiceanu, and H. Andrei, “Intrusion detection on ics and scada networks,” in Recent Developments on Industrial Control Systems Resilience, pp. 197–262, Springer, 2020.
15. M.G. Cimino, N. De Francesco, F. Mercaldo, A. Santone, and G. Vaglini, “Model checking for malicious family detection and phylogenetic analysis in mobile environment,” Computers & Security, vol. 90, p. 101691, 2020.
16. L. Brunese, F. Mercaldo, A. Reginelli, and A. Santone, “Formal methods for prostate cancer gleason score and treatment prediction using radiomic biomarkers,” Magnetic resonance imaging, vol. 66, pp. 165–175, 2020.
17. L. Brunese, F. Mercaldo, A. Reginelli, and A. Santone, “An ensemble learning approach for brain cancer detection exploiting radiomic features,” Computer methods and programs in biomedicine, vol. 185, p. 105134, 2020.
18. L. Brunese, F. Mercaldo, A. Reginelli, and A. Santone, “Prostate gleason score detection and cancer treatment through real-time formal verification,” IEEE Access, vol. 7, pp. 186236–186246, 2019.
19. F. Mercaldo, F. Martinelli, and A. Santone, “Real-time scada attack detection by means of formal methods,” in 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp. 231–236, IEEE, 2019.
20. R. Alur and D. Dill, “Automata for modeling real-time systems,” in International Colloquium on Automata, Languages, and Programming, pp. 322–335, Springer, 1990.
21. R. Alur and D.L. Dill, “A theory of timed automata,” Theoretical computer science, vol. 126, no. 2, pp. 183–235, 1994.
22. G. Behrmann, K.G. Larsen, O. Moller, A. David, P. Pettersson, and W. Yi, “Uppaal-present and future,” in Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No. 01CH37228), vol. 3, pp. 2881–2886, IEEE, 2001.
23. G. Behrmann, A. David, and K.G. Larsen, “A tutorial on uppaal 4.0,”Department of computer science, Aalborg university, 2006.
24. G. Behrmann, A. David, and K.G. Larsen, “A tutorial on uppaal,” in Formal methods for the design of real-time systems, pp. 200–236, Springer, 2004.
25. P. Bouyer, “Model-checking timed temporal logics,” Electronic Notes in Theoretical Computer Science, vol. 231, pp. 323–341, 2009.
26. E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 8, no. 2, pp. 244–263, 1986.
27. N.D. Francesco, G. Lettieri, A. Santone, and G. Vaglini, “Heuristic search for equivalence checking,” Software and System Modeling, vol. 15, no. 2, pp. 513–530, 2016.
28. H.E. Jensen, K.G. Larsen, and A. Skou, “Scaling up uppaal,” in International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 19–30, Springer, 2000.
29. J. Dougherty, R. Kohavi, and M. Sahami, “Supervised and unsupervised discretization of continuous features,” in Machine Learning Proceedings 1995, pp. 194–202, Elsevier, 1995.
30. F. Mercaldo and A. Santone, “Deep learning for image-based mobile malware detection,” Journal of Computer Virology and Hacking Techniques, pp. 1–15, 2020.
31. A. De Lorenzo, F. Martinelli, E. Medvet, F. Mercaldo, and A. Santone, “Visualizing the outcome of dynamic analysis of android malware with vizmal,” Journal of Information Security and Applications, vol. 50, p. 102423, 2020.
32. R. Taormina, S. Galelli, N.O. Tippenhauer, A. Ostfeld, and E. Salomons, “Assessing the effect of cyber-physical attacks on water distribution systems,” in World Environmental and Water Resources Congress 2016, pp. 436–442, 2016.
33. E. Salomons and A. Ostfeld, “Simulation of cyber-physical attacks on water distribution systems with epanet,” in Proceedings of the Singapore Cyber-Security Conference (SGCRC) 2016: Cyber-Security by Design, vol. 14, p. 123, 2016.
Опубликован
2022-03-15
Как цитировать
Меркальдо, Ф., Мартинелли, Ф., & Сантоне, А. (2022). Проверка модели для обнаружения атак в реальном времени в системах распределения воды. Информатика и автоматизация, 21(2), 219-242. https://doi.org/10.15622/ia.21.2.1
Раздел
Информационная безопасность
Copyright (c) Francesco Mercaldo
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями: Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале. Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале. Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).