传感器攻击下信息物理系统的鲁棒性度量

本文利用微分动态逻辑的形式化方法，贡献了一个对信息物理系统上有界传感器攻击进行定量分析的形式化框架。给定系统的前置条件和后置条件，我们形式化了两种定量安全概念：定量前向安全性和后向安全性，它们分别表示（1）系统的最强后置条件相对于指定后置条件有多强，以及（2）为确保指定后置条件成立，指定的前置条件相对于系统所需的最弱前置条件有多强。我们引入了前向鲁棒性和后向鲁棒性两个概念，将系统抵御传感器攻击的鲁棒性刻画为安全性的损失。为了对鲁棒性进行推理，我们引入了前向和后向模拟距离两种模拟距离，它们基于原始系统与传感器受损系统之间的行为距离来定义。前向和后向距离分别刻画了由传感器攻击引起的前向和后向安全性损失程度的上界。我们通过将两种模拟距离表示为模态（即微分动态逻辑公式）来验证它们，并开发了一个专用证明系统来对此类公式进行推理。我们在两个非平凡的案例研究上展示了我们的形式化概念和推理技术：一个需要避免碰撞的自动驾驶车辆和一个水箱系统。