6.7 How Secure and Verified is your Cyber-Physical System?

Printer-friendly version PDF version

Date: Wednesday 27 March 2019
Time: 11:00 - 12:30
Location / Room: Room 7

Chair:
Wanli Chang, University of York, UK

Co-Chair:
Mingsong Chen, East China Normal University, CN

The session addresses security and verification aspects for the design of modern cyber-physical systems. Conditional Generative Adversarial Networks are used to increase security. Lightweight machine learning is used to detect malware at network node level. Stochastic model predictive control is used to limit malware diffusion in the network. Bounded model checking with linear programming is used for on-line verification of the cyber-physical system.

TimeLabelPresentation Title
Authors
11:006.7.1GAN-SEC: GENERATIVE ADVERSARIAL NETWORK MODELING FOR THE SECURITY ANALYSIS OF CYBER-PHYSICAL PRODUCTION SYSTEMS
Speaker:
Mohammad Al Faruque, University of California, Irvine, US
Authors:
Sujit Rokka Chhetri, Anthony Bahadir Lopez, Jiang Wan and Mohammad Al Faruque, University of California, Irvine, US
Abstract
Cyber-Physical Production Systems (CPPS) will usher a new era of smart manufacturing. However, CPPS will be vulnerable to cross-domain attacks due to the interactions between the cyber and physical domains. To address the challenges of modeling cross-domain security in CPPS, we are proposing GAN-Sec, a novel conditional Generative Adversarial Network based modeling approach to abstract and estimate the relations between the cyber and physical domains. Using GAN-Sec, we are able to determine if various security requirements such as confidentiality, availability, and integrity are met. We provide a security analysis of an additive manufacturing system to demonstrate the applicability of GAN-Sec.

Download Paper (PDF; Only available from the DATE venue WiFi)
11:306.7.2LIGHTWEIGHT NODE-LEVEL MALWARE DETECTION AND NETWORK-LEVEL MALWARE CONFINEMENT IN IOT NETWORKS
Speaker:
Sai Manoj Pudukotai Dinakarrao, George Mason University, US
Authors:
Sai Manoj Pudukotai Dinakarrao1, Hossein Sayadi1, Hosein Mohammadi Makrani2, Cameron Nowzari1, Setareh Rafatirad1 and Houman Homayoun1
1George Mason University, US; 2George Mason university, US
Abstract
The sheer size of IoT networks being deployed today presents an "attack surface'' and poses significant security risks at a scale never before encountered. In other words, a single device/node in a network that becomes infected with Malware has the potential to spread Malware across the network, eventually ceasing the network functionality. Simply detecting and quarantining the Malware in IoT networks does not guarantee to prevent Malware propagation. On the other hand, use of traditional control theory for Malware confinement is not effective, as most of the existing works do not consider real-time Malware control strategies that can be implemented using uncertain infection information of the nodes in the network or have the containment problem decoupled from network performance. In this work, we propose a two-pronged approach, where a runtime malware detector (HMD) that employs Hardware Performance Counter (HPC) values to detect the Malware and benign applications is devised. This information is fed during runtime to a stochastic model predictive controller to confine the malware propagation without hampering the network performance. With the proposed solution, a runtime Malware detection accuracy of 80% with a runtime of 10ns is achieved, which is an order of magnitude faster than existing Malware detection solutions. Synthesizing this output with the model predictive containment strategy lead to achieving an average network throughput of nearly 200% of that of IoT networks without any embedded defense.

Download Paper (PDF; Only available from the DATE venue WiFi)
12:006.7.3INCREMENTAL ONLINE VERIFICATION OF DYNAMIC CYBER-PHYSICAL SYSTEMS
Speaker:
Lei Bu, Nanjing University, CN
Authors:
Lei Bu1, Shaopeng Xing1, Xinyue Ren1, Yang Yang1, Qixin Wang2 and Xuandong Li1
1Nanjing University, CN; 2Dept. of Computing, The Hong Kong Polytechnic Univ., HK
Abstract
Periodically online verification has been widely recognized as a practical and promising method to handle the non-deterministic and unpredictable behavior of dynamic CPS systems. However, it is a challenge to keep the online verification of CPS systems finishing quickly in time to give enough time for the running system to respond, if any error is detected. Nevertheless, the problems under verification for each cycle are highly similar to each other. Most of the differences are caused by run-time factors like changing of parameters' values or the reorganization of active components in the system. Under this investigation, this paper presents an incremental verification technique for online verification of CPS systems. A method is given to distinguish the differences between the problem under verification and the previous verified problem. Then, by reusing the problem space of the previous verified problem as a warm-start base, the modified part can be introduced into the base, which can be solved incrementally and efficiently. A set of case studies on a real-case train control system is presented in this paper to demonstrate the performance of the incremental online verification technique.

Download Paper (PDF; Only available from the DATE venue WiFi)
12:156.7.4SELF-SECURED CONTROL WITH ANOMALY DETECTION AND RECOVERY IN AUTOMOTIVE CYBER-PHYSICAL SYSTEMS
Speaker:
Korosh Vatanparvar, University of California, Irvine, US
Authors:
Korosh Vatanparvar and Mohammad Al Faruque, University of California, Irvine, US
Abstract
Cyber-Physical Systems (CPS) are growing with added complexity and functionality. Multidisciplinary interactions with physical systems are the major keys to CPS. However, sensors, actuators, controllers, and wireless communications are prone to attacks that compromise the system. Machine learning models have been utilized in controllers of automotive to learn, estimate, and provide the required intelligence in the control process. However, their estimation is also vulnerable to the attacks from physical or cyber domains. They have shown unreliable predictions against unknown biases resulted from the modeling. In this paper, we propose a novel control design using conditional generative adversarial networks that will enable a self-secured controller to capture the normal behavior of the control loop and the physical system, detect the anomaly, and recover from them. We experimented our novel control design on a self-secured BMS by driving a Nissan Leaf S on standard driving cycles while under various attacks. The performance of the design has been compared to the state-of-the-art; the self-secured BMS could detect the attacks with 83% accuracy and the recovery estimation error of 21% on average, which have improved by 28% and 8%, respectively.

Download Paper (PDF; Only available from the DATE venue WiFi)
12:30End of session
Lunch Break in Lunch Area



Coffee Breaks in the Exhibition Area

On all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area.

Lunch Breaks (Lunch Area)

On all conference days (Tuesday to Thursday), a seated lunch (lunch buffet) will be offered in the Lunch Area to fully registered conference delegates only. There will be badge control at the entrance to the lunch break area.

Tuesday, March 26, 2019

Wednesday, March 27, 2019

Thursday, March 28, 2019