Testing and Validation of Modbus/TCP Protocol for Secure SCADA Communication in CPS using Formal Methods

Cyber-Physical Systems (CPS's) evident representation is Supervisory Control, and Data Acquisition (SCADA). As SCADA is being refurbished with advanced computing and communication technologies, the risk involved in adopting/updating to new technology needs to be validated and verified thoroughly. One of the greatest challenges is security testing of protocols. All CPS systems being live and attached to physical process can not be scheduled for penetration testing and verification. This paper presents design and implementation of industrial compliant SCADA test bed, the formal analysis of semantics and security of Modbus/TCP protocol using Coloured Petri Nets(CPN) tool. A novel method is proposed to differentiate attack vector by identifying influential nodes using formal concept analysis. Modbus/TCP conceptualized attack from analysis is tested and verified on the test bed.