This paper contributes a formal framework for quantitative analysis of bounded sensor attacks on cyber-physical systems, using the formalism of differential dynamic logic. Given a precondition and postcondition of a system, we formalize two quantitative safety notions, quantitative forward and backward safety, which respectively express (1) how strong the strongest postcondition of the system is with respect to the specified postcondition, and (2) how strong the specified precondition is with respect to the weakest precondition of the system needed to ensure the specified postcondition holds. We introduce two notions, forward and backward robustness, to characterize the robustness of a system against sensor attacks as the loss of safety. To reason about robustness, we introduce two simulation distances, forward and backward simulation distances, which are defined based on the behavioral distances between the original system and the system with compromised sensors. Forward and backward distances, respectively, characterize upper bounds of the degree of forward and backward safety loss caused by the sensor attacks. We verify the two simulation distances by expressing them as modalities, i.e., formulas of differential dynamic logic, and develop an ad-hoc proof system to reason with such formulas. We showcase our formal notions and reasoning techniques on two non-trivial case studies: an autonomous vehicle that needs to avoid collision and a water tank system.

翻译：本文提出一种形式化框架，用于定量分析信息物理系统中受限传感器攻击，该框架基于微分动态逻辑的形式化方法。给定系统前置条件与后置条件，我们形式化定义两种量化安全概念：前向量化安全与后向量化安全。前者表征系统最强后置条件相对于指定后置条件的强度，后者表征指定前置条件相对于确保后置条件成立所需最弱前置条件的强度。为刻画系统应对传感器攻击的鲁棒性，我们引入前向鲁棒性与后向鲁棒性两个概念，将鲁棒性定义为安全性的损失量。基于原始系统与传感器受损系统之间的行为距离，我们定义两种模拟距离——前向模拟距离与后向模拟距离，分别表征传感器攻击导致的前向安全性损失与后向安全性损失的上界。通过将这两种模拟距离表达为模态（即微分动态逻辑公式），我们建立专门的证明系统对这些公式进行推理。最后通过两个非平凡案例验证所提形式化概念与推理技术：需避免碰撞的自主驾驶车辆系统与水箱系统。