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.