Fuzzing (Fuzz testing) can effectively identify security vulnerabilities in software by providing a large amount of unexpected input to the target program. An important part of fuzzing test is the fuzzing data generation. Numerous traditional methods to generate fuzzing data have been developed, such as model-based fuzzing data generation and random fuzzing data generation. These techniques require the specification of the input data format or analyze the input data format by manual reverse engineering. In this paper, we introduce an approach using Wasserstein generative adversarial networks (WGANs), a deep adversarial learning method, to generate fuzzing data. This method does not require defining the input data format. To the best of our knowledge, this study is the first to use a WGAN-based method to generate fuzzing data. Industrial security has been an important and pressing issue globally. Network protocol fuzzing plays a significant role in ensuring the safety and reliability of industrial control systems (ICSs). Thus, the proposed method is significant for ICS testing. In the experiment, we use an industrial control protocol such as the Modbus-TCP protocol and EtherCAT protocol as our test target. Results indicate that this approach is more intelligent and capable than the methods used in previous studies. In addition, owing to its design, this model can be trained within a short time, which is computationally light and practical.

Programmable logic controllers (PLC), which are widely applied in modern industrial control systems (ICS), work as the controller of sensors and actuators in ICS. These systems require strict correctness, especially for safety-critical systems. Currently, increasingly ICS move to “come online” scenarios to enhance cyber-physical features, but it makes them more vulnerable due to acquiring increased interconnection accompanied by weakening physical isolation. Moreover, with the more complex controlling environment, such as hundreds of more I/O points and more diverse field buses, the incorrect executions of PLC might cause the failure of the overall ICS. In this article, we examine how the security and safety of running PLC could be enhanced in both developing and deploying stages of ICS. We propose a novel application of runtime verification to guarantee the security and safety of real-world ICS. As a variant of temporal logic, PLC past linear temporal logic (PPLTL) is proposed to specify the security and safety properties of PLC. Using PPLTL, we synthesize monitors to improve the PLC program’s security and safety as a partner of testing and static verification. Our monitors provide twofold processing in a nonintrusive manner: One is filtering abnormal input data before invading the original programs, the other is double-checking the output signals before driving the actuators. We use several case studies and benchmarks to demonstrate the efficiency of the approach. The empirical results show that the time overhead and memory occupation are tiny.

In the field of intelligent connected vehicles, as the rate of in-vehicle communication continues to increase, the importance of real-time and reliability requirements has been more prominent. The Time-Sensitive Networking (TSN) task group is dedicated to the amendments for meeting the urgent needs in the industrial field. In the implementation of TSN, time latency bounds of critical traffic, memory bounds of nodes and utilization of transmission resources are needed to evaluate the feasibility of TSNs. In this paper, we propose a framework called component-based analysis (CBA) to analyze these properties. In CBA, we use a data model, a resource model and a component model to construct an abstract model of TSNs with the system architecture and analyze the feasibility of this abstract model with real-time calculus. Moreover, we discuss the preemption mechanism mentioned in IEEE 802.1Qbu to handle the conflict of different priority queues, which has a serious influence on the resource model of TSNs. Finally, we validate this framework by performing an analysis on a synthetic case and compare the obtained properties with different conflict handling mechanisms.

Programmable logic controllers (PLCs) are special embedded computers that are widely used in industrial control systems. To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whether a PLC program conforms to its specifications, but the expertise requirements and the complexity make it hard to be mastered and widely applied. In this paper, we present a specification-mining-based verification approach for IEC 61131-3 PLC programs. It only requires users to review specifications mined from the program behaviors instead of model checking for specified specifications, which can greatly improve the efficiency of safety verification and is much easier for control system engineers to use. Moreover, we implement a proof-of-concept tool named PLCInspector that supports directly mining LTL specifications and data invariants from PLC programs. Two examples and one real-life case study are presented to illustrate its practicability and efficiency. In addition, a comparison with the existing verification approaches for PLC programs is discussed.

Programmable logic controllers (PLCs) are special purpose computers designed to perform industrial automation tasks. They require highly reliable control programs, particularly when used in safetycritical systems such as nuclear power stations. In the development of reliable control programs, formal methods are “highly recommended”because the correctness of intended programs can be mathematically proven. Formal methods generally require precise semantics indicating how the program behaves during execution. However, for PLC programming languages, formal semantics is not always available rendering the application of formal methods highly challenging. In this paper, we present formal operational semantics of structured text, a widely used PLC programming language. The semantics is based on the ST language specification provided by IEC 61131-3, a generally acknowledged international standard for PLCs. We define the formal semantics in K which is a rewriting-based semantic framework and has been successfully applied in defining the semantics of many general-purpose programming languages such as C [1] and, Java [2]. We validate our formal semantics by testing examples from the standard and then apply the semantics on the verification of control programs for PLCs.