Rodríguez, Ricardo J.; Marrone, Stefano; Marcos, Ibai; Porzio, Giuseppe
MOSTO: A Toolkit to Facilitate Security Auditing of ICS Devices using Modbus/TCP Journal Article
In: Computers & Security, vol. 132, pp. 103373, 2023.
Abstract | Links | BibTeX | Tags: Industrial Control Systems, Modbus, Penetration Testing, Security Auditing
@article{RMMP-COSE-23,
title = {MOSTO: A Toolkit to Facilitate Security Auditing of ICS Devices using Modbus/TCP},
author = {Ricardo J. Rodríguez and Stefano Marrone and Ibai Marcos and Giuseppe Porzio},
url = {http://webdiis.unizar.es/~ricardo/files/papers/RMMP-COSE-23.pdf},
doi = {10.1016/j.cose.2023.103373},
year = {2023},
date = {2023-01-01},
urldate = {2023-01-01},
journal = {Computers & Security},
volume = {132},
pages = {103373},
abstract = {The integration of the Internet into industrial plants has connected Industrial Control Systems (ICS) worldwide, resulting in an increase in the number of attack surfaces and the exposure of software and devices not originally intended for networking. In addition, the heterogeneity and technical obsolescence of ICS architectures, legacy hardware, and outdated software pose significant challenges. Since these systems control essential infrastructure such as power grids, water treatment plants, and transportation networks, security is of the utmost importance. Unfortunately, current methods for evaluating the security of ICS are often ad-hoc and difficult to formalize into a systematic evaluation methodology with predictable results. In this paper, we propose a practical method supported by a concrete toolkit for performing penetration testing in an industrial setting. The primary focus is on the Modbus/TCP protocol as the field control protocol. Our approach relies on a toolkit, named MOSTO, which is licensed under GNU GPL and enables auditors to assess the security of existing industrial control settings without interfering with ICS workflows. Furthermore, we present a model-driven framework that combines formal methods, testing techniques, and simulation to (formally) test security properties in ICS networks.},
keywords = {Industrial Control Systems, Modbus, Penetration Testing, Security Auditing},
pubstate = {published},
tppubtype = {article}
}
The integration of the Internet into industrial plants has connected Industrial Control Systems (ICS) worldwide, resulting in an increase in the number of attack surfaces and the exposure of software and devices not originally intended for networking. In addition, the heterogeneity and technical obsolescence of ICS architectures, legacy hardware, and outdated software pose significant challenges. Since these systems control essential infrastructure such as power grids, water treatment plants, and transportation networks, security is of the utmost importance. Unfortunately, current methods for evaluating the security of ICS are often ad-hoc and difficult to formalize into a systematic evaluation methodology with predictable results. In this paper, we propose a practical method supported by a concrete toolkit for performing penetration testing in an industrial setting. The primary focus is on the Modbus/TCP protocol as the field control protocol. Our approach relies on a toolkit, named MOSTO, which is licensed under GNU GPL and enables auditors to assess the security of existing industrial control settings without interfering with ICS workflows. Furthermore, we present a model-driven framework that combines formal methods, testing techniques, and simulation to (formally) test security properties in ICS networks.
Nardone, Roberto; Rodríguez, Ricardo J; Marrone, Stefano
Formal Security Assessment of Modbus Protocol Proceedings Article
In: Proceedings of the 11th International Conference for Internet Technology and Secured Transactions, pp. 142–147, IEEE, 2016.
Abstract | Links | BibTeX | Tags: Cyber-Physical Security, Dynamic State Machines, Modbus, Model checking, SCADA control systems
@inproceedings{NRM-ITST-16,
title = {Formal Security Assessment of Modbus Protocol},
author = {Roberto Nardone and Ricardo J Rodríguez and Stefano Marrone},
url = {http://webdiis.unizar.es/~ricardo/files/papers/NRM-ICITST-16.pdf},
doi = {10.1109/ICITST.2016.7856685},
year = {2016},
date = {2016-12-01},
booktitle = {Proceedings of the 11th International Conference for Internet Technology and Secured Transactions},
pages = {142--147},
publisher = {IEEE},
abstract = {Critical infrastructures as water treatment, power distribution, or telecommunications provide essential services to our day-to-day basis. Any service discontinuity may have a high impact into our society and even our safety. Thus, security of these systems against intentional threats must be guaranteed. However, many of these systems are based on protocols initially designed to operate on closed, unroutable networks, making them an easy target for cybercriminals. In this regard, Modbus is a widely adopted protocol in control systems. Modbus protocol, however, lacks for security properties and is vulnerable to plenty of attacks (as spoofing, flooding, or replay to name a few). In this paper, we propose a formal modeling of Modbus protocol using an extension of hierarchical state-machines that is automatically transformed to a Promela model. This model allows us to find counterexamples of security properties by model-checking. In particular, in this paper we prove the existence of man-in-the-middle attack in Modbus protocol. Our approach also allows to formally evaluate security properties in future extensions of Modbus protocols.},
keywords = {Cyber-Physical Security, Dynamic State Machines, Modbus, Model checking, SCADA control systems},
pubstate = {published},
tppubtype = {inproceedings}
}
Critical infrastructures as water treatment, power distribution, or telecommunications provide essential services to our day-to-day basis. Any service discontinuity may have a high impact into our society and even our safety. Thus, security of these systems against intentional threats must be guaranteed. However, many of these systems are based on protocols initially designed to operate on closed, unroutable networks, making them an easy target for cybercriminals. In this regard, Modbus is a widely adopted protocol in control systems. Modbus protocol, however, lacks for security properties and is vulnerable to plenty of attacks (as spoofing, flooding, or replay to name a few). In this paper, we propose a formal modeling of Modbus protocol using an extension of hierarchical state-machines that is automatically transformed to a Promela model. This model allows us to find counterexamples of security properties by model-checking. In particular, in this paper we prove the existence of man-in-the-middle attack in Modbus protocol. Our approach also allows to formally evaluate security properties in future extensions of Modbus protocols.