Проверка модели для обнаружения атак в реальном времени в системах распределения воды

Обложка

Цитировать

Полный текст

Аннотация

Системы распределения воды представляют собой критическую инфраструктуру. Эти архитектуры очень важны, и нестандартное поведение может отразиться на безопасности человека. Фактически, злоумышленник, получивший контроль над такой архитектурой, может нанести множество повреждений как инфраструктуре, так и людям. В этой статье мы предлагаем подход к выявлению нестандартного поведения, ориентированного на системы распределения воды. Разработанный подход рассматривает формальную среду проверки. Журналы, полученные из систем распределения воды, анализируются в формальную модель, и, используя временную логику, мы характеризуемповедение системы распределения воды во время атаки. Оценка, относящаяся к системе распределения воды, подтвердила эффективность разработанного подхода при выявлении трех различных нестандартных режимов работы.

Об авторах

Ф. Меркальдо

Университет Молизе

Автор, ответственный за переписку.
Email: francesco.mercaldo@iit.cnr.it
Виа Франческо де Санктис 1

Ф. Мартинелли

Национальный исследовательский совет Италии

Email: fabio.martinelli@iit.cnr.it
Виа Джузеппе Моруцци 1

А. Сантоне

Университет Молизе

Email: antonella.santone@unimol.it
Виа Франческо де Санктис 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») на элемент с текстом «Принять и продолжить».