Model Checking for Real-Time Attack Detection in Water Distribution Systems

Мұқаба

Дәйексөз келтіру

Толық мәтін

Аннотация

Water distribution systems represents critical infrastructures. These architectures are really critical and an irregular behaviour can be reflected in human safety. As a matter of fact, an attacker obtaining the control of such of an architecture is able to perpetrate a plethora of damages, both to the infrastructure but also to people. In this paper, we propose an approach to identify irregular behaviours focused on water distribution systems. The designed approach considers formal verification environment. The logs retrieved from water distribution systems are parsed into a formal model and, by exploiting timed temporal logic, we characterize the behaviour of a water distribution system while an attack is happening. The evaluation, referred to a water distribution system, confirmed the effectiveness of the designed approach in the identification of three different irregular behaviours.

Авторлар туралы

F. Mercaldo

University of Molise

Хат алмасуға жауапты Автор.
Email: francesco.mercaldo@iit.cnr.it
Via Francesco De Sanctis St. 1

F. Martinelli

National Research Council of Italy

Email: fabio.martinelli@iit.cnr.it
Via Giuseppe Moruzzi St. 1

A. Santone

University of Molise

Email: antonella.santone@unimol.it
Via Francesco De Sanctis St. 1

Әдебиет тізімі

  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.

Қосымша файлдар

Қосымша файлдар
Әрекет
1. JATS XML
Жүктеу

Согласие на обработку персональных данных с помощью сервиса «Яндекс.Метрика»

1. Я (далее – «Пользователь» или «Субъект персональных данных»), осуществляя использование сайта https://journals.rcsi.science/ (далее – «Сайт»), подтверждая свою полную дееспособность даю согласие на обработку персональных данных с использованием средств автоматизации Оператору - федеральному государственному бюджетному учреждению «Российский центр научной информации» (РЦНИ), далее – «Оператор», расположенному по адресу: 119991, г. Москва, Ленинский просп., д.32А, со следующими условиями.

2. Категории обрабатываемых данных: файлы «cookies» (куки-файлы). Файлы «cookie» – это небольшой текстовый файл, который веб-сервер может хранить в браузере Пользователя. Данные файлы веб-сервер загружает на устройство Пользователя при посещении им Сайта. При каждом следующем посещении Пользователем Сайта «cookie» файлы отправляются на Сайт Оператора. Данные файлы позволяют Сайту распознавать устройство Пользователя. Содержимое такого файла может как относиться, так и не относиться к персональным данным, в зависимости от того, содержит ли такой файл персональные данные или содержит обезличенные технические данные.

3. Цель обработки персональных данных: анализ пользовательской активности с помощью сервиса «Яндекс.Метрика».

4. Категории субъектов персональных данных: все Пользователи Сайта, которые дали согласие на обработку файлов «cookie».

5. Способы обработки: сбор, запись, систематизация, накопление, хранение, уточнение (обновление, изменение), извлечение, использование, передача (доступ, предоставление), блокирование, удаление, уничтожение персональных данных.

6. Срок обработки и хранения: до получения от Субъекта персональных данных требования о прекращении обработки/отзыва согласия.

7. Способ отзыва: заявление об отзыве в письменном виде путём его направления на адрес электронной почты Оператора: info@rcsi.science или путем письменного обращения по юридическому адресу: 119991, г. Москва, Ленинский просп., д.32А

8. Субъект персональных данных вправе запретить своему оборудованию прием этих данных или ограничить прием этих данных. При отказе от получения таких данных или при ограничении приема данных некоторые функции Сайта могут работать некорректно. Субъект персональных данных обязуется сам настроить свое оборудование таким способом, чтобы оно обеспечивало адекватный его желаниям режим работы и уровень защиты данных файлов «cookie», Оператор не предоставляет технологических и правовых консультаций на темы подобного характера.

9. Порядок уничтожения персональных данных при достижении цели их обработки или при наступлении иных законных оснований определяется Оператором в соответствии с законодательством Российской Федерации.

10. Я согласен/согласна квалифицировать в качестве своей простой электронной подписи под настоящим Согласием и под Политикой обработки персональных данных выполнение мною следующего действия на сайте: https://journals.rcsi.science/ нажатие мною на интерфейсе с текстом: «Сайт использует сервис «Яндекс.Метрика» (который использует файлы «cookie») на элемент с текстом «Принять и продолжить».