Paper Info
Title
Formal security assessment of Modbus protocol
Abstract
Critical infrastructures as water treatment, power distribution, or telecommunications, provide daily services essential to our lifestyle. Any service discontinuity can have a high impact into our society and even into 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, the original contribution of this paper is the formal demonstration of the existence of man-in-the-middle attacks in Modbus-based systems. Our approach also allows to formally evaluate security properties in future extensions of Modbus protocols.
Year
DOI
Venue
2016
10.1109/ICITST.2016.7856685
2016 11th International Conference for Internet Technology and Secured Transactions (ICITST)
Keywords
Field
DocType
SCADA control systems,Dynamic State Machines,Model checking,Cyber-Physical Security,Modbus
Model checking,Spoofing attack,Unified Modeling Language,Computer science,Computer security,Computer network,Control system,Modbus,Promela,Security assessment,The Internet
Conference
ISSN
ISBN
Citations 
2164-7046
978-1-5090-4852-6
0
PageRank 
References 
Authors
0.34
6
3
Name
Order
Citations
PageRank
Roberto Nardone110815.07
Ricardo J. Rodríguez27012.60
Stefano Marrone317425.49