Formal Modeling and Analysis of Industrial Control System Network Protocols
Event Type
DescriptionIndustrial Control Systems (ICSs) constitute a germane class of cyber-physical systems. ICSs are increasingly employed to control and manage various critical infrastructure around the world. For instance, to control scientific instruments, most major national laboratories rely on Experimental Physics Industrial Control System (EPICS). With
the emergence of Industrial Internet of Things, ICSs have become more complex . However, due to the typical perimeter protection used on most ICS sites, these systems are vulnerable to various types of threats. The exploitation of these security flaws can potentially cause a nation-state damage. In the case of EPICS, the consequences of these attacks can range from the loss of integrity of scientific
data to severe damage to the entire EPICS site.Formal methods use mathematical rigor and techniques to specify and verify systems and processes. Although such
methods do not apriori guarantee correctness, they can greatly
improve our understanding of a system behavior by revealing
inconsistencies, ambiguities and incompleteness that might
otherwise go unnoticed during design, specification and implementation. Due to the safety-critical nature and complexity in designs of some of these systems, we proposed an
approach that leverages the use of a Symbolic Model Verifier
(SMV) tool to discover bugs, vulnerabilities and attack holes. Recent work
have proposed the use of formal methods to discover potential attacks in ICS. However, their analysis and comparison
of results is limited by human judgement. In this paper, we
specifically propose the use of SMV as a model tool to analyse the EPICS PV Gateway.