Control systems used in manufacturing, transportation, and energy delivery connect embedded controllers to IT networks. Recently, such systems have been gaining increasing attention from attackers, e.g., the well known Stuxnet attack. The majority of efforts both in attacking and defending control systems have focussed solely on the IT perimeter. We argue that this is insufficient. We first show that compromise of the IT perimeter does not necessarily allow an adversary to execute a Stuxnet-like targeted attack. In response, we introduce our tool SABOT, which incrementally model checks embedded controller code against an adversary-supplied specification. The result is an automatically generated attack program for the victim control system. Our results show that SABOT can instantiate malicious payloads in 4 out of 5 systems tested, even when the adversary does not know the full system behavior.
As a response to SABOT-style attacks, we then present a Trusted Safety Verifier (TSV). TSV uses a combination of symbolic execution and model checking to ensure that all controller code satisfies engineer-provided safety specifications. We show that TSV can verify the safety of controller code from a representative set of control systems in under two minutes, a small overhead in the control system lifecycle.
Speaker Biography
Stephen McLaughlin recently defended his thesis in Computer Science and Engineering at Penn State. His past work has identified vulnerabilities in electronic voting machines and smart electric meters. His current work on specification-based control system security has been presented at CCS 2012, ACSAC 2013, and NDSS 2014. He is a two-year recipient of the Diefenderfer graduate fellowship in Penn State’s College of Engineering.