Vulnerability Identification of Operational Technology Protocols

Organisation:	University of Nebraska-Lincoln (USA)
Method:	NFA LNT
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2023
Size:	787 states and 17184 transitions
Description:	The integration and convergence of Information Technology (IT) and Operational Technology (OT) systems has created challenges for securing communications on OT systems. However, currently implemented protocols were not designed with security in mind, and the requirement for constant availability often discourages adding supplementary security measures to the protocols. Despite that current security methods (firewalls, intrusion detection systems, and anomaly detection schemes) improve overall cybersecurity posture, the protocols are still vulnerable to various attacks. The Modbus protocol has been widely adopted for use within Industrial Control Systems (ICS). While the protocol specification outlines the packet formation and exception handling requirements, the device-specific implementation requirements are not. This allows for significantly different performance and behavior of devices with seemingly identical protocol capabilities. There is currently no standard to identify the causes of diverging performance due to differences between protocol implementations. This work proposes a method to identify critical transitions within protocols and their implementations to enable improved robustness and compliance through formal modeling. The packets associated to each of the 19 function codes of Modbus were organized and represented as hierarchical structures. Then, the protocol itself was translated into NFA (Nondeterministic Finite Automata) diagrams, which were in turn translated to LNT. This enabled the use of CADP tools to search for deadlocks and livelocks, as well as to identify critical transitions (originating from states where the server address or error check field is incorrect).
Conclusions:	Even though Modbus is a widely adopted protocol due to its open standard and simplicity, many critical transitions can still negatively impact device implementations, especially during cyberattacks. These transitions can be especially difficult to identify in distributed systems, as each device’s requirements and target applications can differ significantly. The use of LNT (which was found well-suited for modeling communication protocols) and CADP enables to identify various issues (critical transitions, deadlocks, and livelocks) and thus to create a more robust and compliant protocol ecosystem.
Publications:	[Boeding-Hempel-Sharif-23] Matthew Boeding, Michael Hempel, and Hamid Sharif. "Vulnerability Identification of Operational Technology Protocol Specifications Through Formal Modeling". Proc. of the 16th International Conference on Signal Processing and Communication System (ICSPCS'2023), Bydgoszcz, Poland, pp. 1-6. IEEE CS Press, 2023. Available on-line at: https://doi.org/10.1109/ICSPCS58109.2023.10261127 or from the CADP Web site in PDF or PostScript
Contact:	Hamid Sharif Electrical and Computer Engineering University of Nebraska-Lincoln Scott Campus (Omaha) USA PKI 200C Email: hsharif@unl.edu
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page