TSV: Trusted Safety Verifier

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 which can impact process safety. Our solution, Trusted Safety Verifier (TSV), is a minimal TCB for the verification of safety-critical code executed on programmable controllers. No controller code is allowed to be executed 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. 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.

Note: this research is joingtly funded by DOE and NSF.

For more information about this technology or opportunities for industrial collaboration, contact Saman Zonouz. More information is also available on the Related Research Activity page.