Methods of Formal Analysis for ICS Protocols and HART - IP CPN modelling

Industrial Control System (ICS) used in critical infrastructure like energy sector, oil and natural gas, chemical processing, waste water treatment etc. are of great importance since it serves to a larger population and hence termed as National Critical Infrastructure (NCI). Security of such infrastructures is essential from physical as well as from cyber point of view. Traditional approach for the security was only physical consisting of creating SOP, access control, physical verification, etc. But due past cyber disturbing events like Stuxnet, Blackenergy-3, Turkey pipeline explosion, Havex, New York dam attack, etc. it is realized that the network security of the connected devices within the infrastructure is also of same importance. Various researches in this field have helped to make the NCI immune to a certain extent as well as resilient against cyber-attacks. One such approach is using Formal Analysis for performing security analysis of the communication protocols used in ICS domain. In this paper a compressive review of all available methods for formal analysis along with CPN modelling is done for analysis of valid as well as invalid states of HART protocol. The Modelling shows various states that the protocol can take during one transaction of communication. Further this analysis can be extended for other Fieldbus protocols for security analysis.