Specification-based Attacks and Defenses in Sequential Control Systems

Open Access
McLaughlin, Stephen Elliot
Graduate Program:
Computer Science and Engineering
Doctor of Philosophy
Document Type:
Date of Defense:
February 05, 2014
Committee Members:
  • Patrick Drew Mcdaniel, Dissertation Advisor
  • Trent Ray Jaeger, Committee Member
  • Thomas F Laporta, Committee Member
  • Seth Adam Blumsack, Special Member
  • Security
  • Cyber-Physical
  • Control
Cyber physical systems, such as control systems use general purpose computation to govern the behavior of physical systems in the manufacturing, transportation, and energy sectors. These systems are increasingly vulnerable to software-based exploits that have physical consequences. In modern control systems, Programmable Logic Controllers (PLCs) drive the physical machinery in a plant according to control logic programs. For ease of modification, control logic is uploaded to the PLC from the local network, the Internet, or other external network, making them vulnerable to malicious code injection. PLCs are unique within the control system, in that they form the last step of computation between the computer and the physical infrastructures. If they are compromised by an adversary, the entire physical system will be under malicious control. If they can be regulated by defenders, then adversarial influence over any other part of the system is nullified. In short, whoever owns the PLC owns the critical infrastructure. In this work, we look at a novel approach to both attacking and securing automated cyber physical control systems: em specification-based attacks and defenses. The vast body of existing work in computer security focuses on protecting information. In a control system, on the other hand, the most critical asset is not information, but the physical machinery, processes, and personnel, whose safety must be guaranteed. Due to the sheer complexity of modern information processing systems, it is impossible to completely secure the computer and network perimeters of automated control systems. Thus, instead of trying to harden perimeter security, we instead aim at directly regulating the physical behavior of the control system through behavioral specifications. This dissertation covers three different systems that demonstrate specification-based attacks and defenses. The attack, called SABOT, allows adversaries to attack control systems knowing only their physical behavior. SABOT takes the adversary's idea of how the victim physical system works, and automatically instantiates it into runnable PLC code that executes the desired attack measures. The second system is a Trusted Safety Verifier (TSV). TSV prevents any malicious code from being uploaded to PLCs. This is done by performing a novel analysis technique on the PLC code to determine if it violates any engineer-supplied safety properties. Finally, we consider a Controller Controller (C2). C2 monitors the commands sent from PLCs to physical machinery to block any malicious device usage. C2 is the most minimal of all these security mechanisms, as even the PLC can be fully compromised, and the security guarantees will still hold. These works are built on early experiences in directed penetration testing of smart electric meters, which found vulnerabilities based on the adversarial goals they achieved. Throughout, the case will be made that specification-based control of physical system behavior is a promising approach for securing control systems in modern critical infrastructure.