Cyber-physical systems (CPS) are vulnerable to attacks targeting outgoing actuation commands that modify their physical behaviors. The limited resources in such systems, coupled with their stringent timing constraints, often prevents the checking of every outgoing command. We present a "selective checking" mechanism that uses game-theoretic modeling to identify the right subset of commands to be checked in order to deter an adversary. This mechanism is coupled with a "delay-aware" trusted execution environment (TEE) to ensure that only verified actuation commands are ever sent to the physical system, thus maintaining their safety and integrity. The selective checking and trusted execution (SCATE) framework is implemented on an off-the-shelf ARM platform running standard embedded Linux. We demonstrate the effectiveness of SCATE using four realistic cyber-physical systems (a ground rover, a flight controller, a robotic arm and an automated syringe pump) and study design trade-offs. Not only does SCATE provide a high level of security and high performance, it also suffers from significantly lower overheads (30.48%-47.32% less) in the process. In fact, SCATE can work with more systems without negatively affecting the safety of the system. Considering that most CPS do not have any such checking mechanisms, and SCATE is guaranteed to meet all the timing requirements (i.e., ensure the safety/integrity of the system), our methods can significantly improve the security (and, hence, safety) of the system.

翻译：信息物理系统易受针对改变物理行为的输出执行命令的攻击。此类系统中有限的资源以及严格的时间约束，往往导致无法检查每一条输出命令。我们提出一种"选择性检查"机制，利用博弈论建模识别需检查的正确命令子集以威慑对手。该机制与"时延感知"可信执行环境相结合，确保只有经过验证的执行命令才会被发送至物理系统，从而维护其安全性和完整性。选择性检查与可信执行框架在运行标准嵌入式Linux的商用ARM平台上实现。我们通过四个真实信息物理系统（地面巡视器、飞行控制器、机械臂以及自动注射泵）验证了SCATE的有效性，并研究了设计权衡。SCATE不仅提供高水平的安全性和高性能，而且在运行过程中显著降低了开销（减少30.48%-47.32%）。事实上，SCATE可在不影响系统安全性的前提下适用于更多系统。考虑到大多数信息物理系统缺乏此类检查机制，而SCATE能够保证满足所有时间约束（即确保系统的安全性与完整性），我们的方法可显著提升系统的安全性（进而保证物理安全性）。