Leveraging Physical Models for Attacking and Defending PLCs

Presenter

Luis Garcia, Graduate Research Assistant, Department of Electrical and Computer Engineering, Rutgers University

Date

January 27, 2017

Description

Download PDF of Slides

This is a presentation of CREDC Affiliated Research.

In this CREDC Affiliate presentation we will discuss potential attacks and practical real-world defenses against cyber-physical systems. We will focus on the verification of programmable logic controllers (PLCs) with respect to the underlying physical models. We will first present HARVEY, a PLC rootkit that implements a physics-aware stealthy attack against cyber physical power grid control systems. HARVEY sits within the PLC’s firmware below the control logic and modifies control commands before they are sent out by the PLC’s output modules to the physical plant’s actuators. HARVEY replaces legitimate control commands with malicious, adversary-optimal commands to the physical power equipment. To ensure system safety, the operators observe the status of the power system by fetching system parameter values from PLC devices. To conceal the maliciously caused anomalous behavior from operators, HARVEY intercepts the sensor measurement inputs to the PLC device. HARVEY simulates the power system with the legitimate control commands (which were intercepted/replaced with malicious ones), and calculates/injects the sensor measurements that operators would expect to see. We implemented HARVEY on the widely spread Allen Bradley PLC and evaluated it on a real-world electric power grid test-bed. The results empirically prove HARVEY’s deployment feasibility in practice nowadays. In light of these new threats, we will present our current approaches to device-oriented verification of cyber-physical systems. In particular, we provide an alternative method to proving the transient stability of an industrial control system with a synchronous machine using the invariant properties of the physical system. The safety of the system is modeled and verified as a hybrid cyber-physical system using KeymaeraX, a hybrid systems theorem prover for analyzing the control program and the physical behavior of the controlled system together.

Related Research Activities

Related Publications

  • Video Category
    • Research
  • Related People