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 (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.

With the development of the industrial control system, Programmable Logic Controllers (PLCs) are increasingly adopted in the process automation. Moreover, many PLCs play key roles in safety-critical systems like nuclear power plants, where robust and reliable control programs are required. To ensure the quality of programs, testing and verification methods are necessary. In this paper, we present a novel methodology which applies model checking to verifying PLC programs. Specifically, we focus on the Structured Text (ST) language which is a widely-used, high-level programming language defined in the IEC 61131-3 standard. A formal model named Behaviour Model (BM) is defined to specify the behaviour of ST programs. An algorithm based on variable state analysis for automatically extracting the BM from an ST program is given. An algorithm based on the automata-theoretic approach is proposed to verify Linear Temporal Logic (LTL) properties on the BM. Finally, a real-life case study is presented.

Industrial control systems (ICSs), especially distributed control systems (DCSs), are usually composed of several subsystems. Each subsystem is controlled by a control unit such as a programmable logic controller (PLC) or a micro-controller and collaborates with other subsystems via the field bus, Ethernet, or other communication links. In the traditional development process, engineers program for each PLC separately and skillfully orchestrate the collaboration among subsystems, which is difficult and error-prone. The larger the scale of the ICS is, the higher the complexity of the collaboration is, and the more error-prone the development process is. In this paper, we propose a decomposition-based development method for distributed ICSs to reduce the difficulty of developing distributed ICSs whose subsystems cooperate with each other. First, we present a general event-triggered specification language named Industrial Modeling Collaboration Language (IMCL) for modeling ICSs; the language allows describing system functions and physical resources in one unified model. Second, we provide an approach for decomposing the complex system model into multiple fine-grained and interactive subsystem models. Specifically, under given resource constraints, we propose an automatic decomposition and collaboration algorithm based on the IMCL model to meet the original functional requirements. In this way, engineers can develop distributed control systems without considering the underlying complex interaction mechanisms. We present a case study to demonstrate it.