A Trusted Safety Verifier for Cyber-Physical Control Systems
Download PDF of Slides
Attackers can leverage security vulnerabilities in control systems to make physical processes behave unsafely. Currently, the safe behavior of a control system relies on a Trusted Computing Base (TCB) of commodity machines, firewalls, networks, and embedded systems. These large TCBs, often containing known vulnerabilities, expose many attack vectors that can impact process safety. We present the Trusted Safety Verifier (TSV), a minimal TCB for the verification of safety-critical code executed on programmable controllers. No controller code is allowed to execute before it passes physical safety checks by TSV. If a safety violation is found, TSV provides a demonstrative test case to system operators. TSV works by first translating assembly-level controller code into an intermediate language, ILIL. ILIL allows us to check code containing more instructions and features than previous controller code safety verification techniques. TSV efficiently mixes symbolic execution and model checking by transforming an ILIL program into a novel temporal execution graph that lumps together safety- equivalent controller states. We implemented TSV on a Raspberry Pi computer as a bump-in-the-wire that intercepts all controller- bound code. Our evaluation shows that it can test a variety of programs for common safety properties in an average of less than three minutes, and under six minutes in the worst case — a small one-time addition to the process engineering life cycle. TSV will be presented at Network and Distributed System Security Symposium (NDSS) 2014.
Saman Zonouz is an Assistant Professor in the Electrical and Computer Engineering Department at the University of Miami since August 2011, and the Director of the 4N6 Cyber Security and Forensics Laboratory. He has been awarded the, Faculty Fellowship Award by the Air Force Office of Scientific Research in 2013, Best Student Paper Award at IEEE SmartGridComm 2013, UM Provost Research award in 2011, as well as EARLY CAREER Research award from the University of Miami in 2012. 4N6 research group consists of 21 members including 8 Ph.D. students and their research projects have been funded by NSF, ONR, DOE/ARPA-E, and Fortinet Corporation. The group’s current research focuses on Systems Security and Privacy, Binary and Malware Analysis, Intrusion Forensics and Response, as well as Trustworthy Critical Cyber-Physical Power-Grid Infrastructures. Saman Zonouz is an IEEE and ACM member, and has served as the Chair, Program Committee member, and a reviewer for international conferences and journals such as IEEE Transactions on Smart Grid. He obtained his Ph.D. in Computer Science, specifically, Intrusion Tolerance Solutions for the Power-Grid, from University of Illinois at Urbana-Champaign in 2011.
The seminar series is presented by the Trustworthy Cyber Infrastructure for the Power Grid (TCIPG) Project, an $18 million multi-university research effort whose partner institutions include the University of Illinois at Urbana-Champaign, Arizona State University, Dartmouth, and Washington State University. The TCIPG Project, a successor to the earlier NSF-funded TCIP Center, was founded in 2009 with support from the U.S. Department of Energy and the U.S. Department of Homeland Security. It is housed in the Information Trust Institute, University of Illinois at Urbana-Champaign.
