skip to main content


Title: An Ontology-Based Framework for Formal Verification of Safety and Security Properties of Control Logics
Any safety issues or cyber attacks on an Industrial Control Systems (ICS) may have catastrophic consequences on human lives and the environment. Hence, it is imperative to have resilient tools and mechanisms to protect ICS. To verify the safety and security of the control logic, complete and consistent specifications should be defined to guide the testing process. Second, it is vital to ensure that those requirements are met by the program control algorithm. In this paper, we proposed an approach to formally define the system specifications, safety, and security requirements to build an ontology that is used further to verify the control logic of the PLC software. The use of ontology allowed us to reason about semantic concepts, check the consistency of concepts, and extract specifications by inference. For the proof of concept, we studied part of an industrial chemical process to implement the proposed approach. The experimental results in this work showed that the proposed approach detects inconsistencies in the formally defined requirements and is capable of verifying the correctness and completeness of the control logic. The tools and algorithms designed and developed as part of this work will help technicians and engineers create safer and more secure control logic for ICS processes.  more » « less
Award ID(s):
1846493
NSF-PAR ID:
10407355
Author(s) / Creator(s):
;
Date Published:
Journal Name:
2022 14th International Conference on Electronics, Computers and Artificial Intelligence (ECAI)
Page Range / eLocation ID:
1 to 8
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. As part of Industrial Control Systems (ICS), the control logic controls the physical processes of critical infrastructures such as power plants and water and gas distribution. The Programmable Logic Controller (PLC) commonly manages these processes through actuators based on information received from sensor readings. Therefore, boundary checking is essential in ICS because sensor readings and actuator values must be within the safe range to ensure safe and secure ICS operation. In this paper, we propose an ontology-based approach to provide the knowledge required to verify the boundaries of ICS components with respect to their safety and security specifications. For the proof of concept, the formal model of the Programmable Logic Controller (PLC) is created in UPPAAL and validated in UPPAAL-API. Then, the proposed boundary verification algorithm is used to import the required information from the safety/security ontology 
    more » « less
  2. Safety and security are the two most important properties of industrial control systems (ICS), and their integration is necessary to ensure that safety goals do not undermine security goals and vice versa. Sometimes, safety and security co-engineering leads to conflicting requirements or violations capable of impacting the normal behavior of the system. Identification, analysis, and resolution of conflicts arising from safety and security co-engineering is a major challenge, an under-researched area in safety-critical systems(ICS). This paper presents an STPA-SafeSec-CDCL approach that addresses the challenge. Our proposed methodology combines the STPA-SafeSec approach for safety and security analysis and the Conflict-Driven Clause Learning (CDCL) approach for the identification, analysis, and resolution of conflicts where conflicting constraints are encoded in satisfiability (SAT) problems. We apply our framework to the Tennessee Eastman Plant process model, a chemical process model developed specifically for the study of industrial control processes, to demonstrate how to use the proposed method. Our methodology goes beyond the requirement analysis phase and can be applied to the early stages of system design and development to increase system reliability, robustness, and resilience. 
    more » « less
  3. Industrial control systems (ICS) include systems that control industrial processes in critical infrastructure such as electric grids, nuclear power plants, manufacturing plans, water treatment systems, pharmaceutical plants, and building automation systems. ICS represent complex systems that contain an abundance of unique devices all of which may hold different types of software, including applications, firmware and operating systems. Due to their ability to control physical infrastructure, ICS have more and more become targets of cyber-attacks, increasing the risk of serious damage, negative financial impact, disruption to business operations, disruption to communities, and even the loss of life. Ethical hacking represents one way to test the security of ICS. Ethical hacking consists of using a cyber-attacker's perspective and a variety of cybersecurity tools to actively discover vulnerabilities and entry points for potential cyber-attacks. However, ICS ethical hacking represents a difficult task due to the wide variety of devices found on ICS networks. Most ethical hackers do not hold expertise or knowledge about ICS hardware, device computing elements, protocols, vulnerabilities found on these elements, and exploits used to exploit these vulnerabilities. Effective approaches are needed to reduce the complexity of ICS ethical hacking tasks. In this study, we use ontology modeling, a knowledge representation approach in artificial intelligence (AI), to model data that represent ethical hacking tasks of building automation systems. With ontology modeling, information is stored and represented in the form of semantic graphs that express individuals, their properties, and the relations between multiple individuals. Data are drawn from sources such as the National Vulnerability Database, ExploitDB, Common Weakness Enumeration (CWE), the Common Attack Pattern and Enumeration Classification (CAPEC), and others. We show, through semantic queries, how the ontology model can automatically link together entities such as software names and versions of ICS software, vulnerabilities found on those software instances, vulnerabilities found on the protocols used by the software, exploits found on those vulnerabilities, weaknesses that represent those vulnerabilities, and attacks that can exploit those weaknesses. The ontology modeling of ICS ethical hacking and the semantic queries run over the model can reduce the complexity of ICS hacking tasks. 
    more » « less
  4. Due to the critical importance of Industrial Control Systems (ICS) to the operations of cities and countries, research into the security of critical infrastructure has become increasingly relevant and necessary. As a component of both the research and application sides of smart city development, accurate and precise modeling, simulation, and verification are key parts of a robust design and development tools that provide critical assistance in the prevention, detection, and recovery from abnormal behavior in the sensors, controllers, and actuators which make up a modern ICS system. However, while these tools have potential, there is currently a need for helper-tools to assist with their setup and configuration, if they are to be utilized widely. Existing state-of-the-art tools are often technically complex and difficult to customize for any given IoT/ICS processes. This is a serious barrier to entry for most technicians, engineers, researchers, and smart city planners, while slowing down the critical aspects of safety and security verification. To remedy this issue, we take a case study of existing simulation toolkits within the field of water management and expand on existing tools and algorithms with simplistic automated retrieval functionality using a much more in-depth and usable customization interface to accelerate simulation scenario design and implementation, allowing for customization of the cyber-physical network infrastructure and cyber attack scenarios. We additionally provide a novel in tool assessment of network’s resilience according to graph theory path diversity. Further, we lay out a roadmap for future development and application of the proposed tool, including expansions on resiliency and potential vulnerability model checking, and discuss applications of our work to other fields relevant to the design and operation of smart cities. 
    more » « less
  5. null (Ed.)
    Industrial Control Systems (ICS) are used to control physical processes in critical infrastructure. These systems are used in a wide variety of operations such as water treatment, power generation and distribution, and manufacturing. While the safety and security of these systems are of serious concern, recent reports have shown an increase in targeted attacks aimed at manipulating physical processes to cause catastrophic consequences. This trend emphasizes the need for algorithms and tools that provide resilient and smart attack detection mechanisms to protect ICS. In this paper, we propose an anomaly detection framework for ICS based on a deep neural network. The proposed methodology uses dilated convolution and long short-term memory (LSTM) layers to learn temporal as well as long term dependencies within sensor and actuator data in an ICS. The sensor/actuator data are passed through a unique feature engineering pipeline where wavelet transformation is applied to the sensor signals to extract features that are fed into the model. Additionally, this paper explores four variations of supervised deep learning models, as well as an unsupervised support vector machine (SVM) model for this problem. The proposed framework is validated on Secure Water Treatment testbed results. This framework detects more attacks in a shorter period of time than previously published methods. 
    more » « less