基于控制障碍函数的具有可证明保证的攻击恢复

本文研究信息物理系统（CPS）在执行器攻击下的可证明安全保证。具体而言，我们考虑CPS安全性，并提出了一种基于零化控制障碍函数（ZCBF）条件的新型攻击检测机制。此外，我们基于系统接近违反安全的程度设计了自适应恢复机制。我们证明在某些条件下，该攻击检测机制是可靠的，即对于对抗性攻击不存在漏报。我们提出了初始条件和输入约束的充分条件，使得所得到的CPS在设计上即安全。我们还提出了一种新型混合控制以应对攻击检测延迟并避免Zeno行为。接下来，为高效计算初始条件集合，我们提出了一种基于采样的方法来验证一个集合是否为生存域（viability domain）。具体地，我们设计了一种在有限点集上检验修正障碍函数条件的方法，以评估一个集合是否可保持前向不变（forward invariant）。然后，我们提出一种迭代算法来计算初始条件集合和输入约束集合，以限制攻击者在攻陷脆弱输入时的效果。最后，我们使用二次规划（QP）方法进行在线恢复（以及标称）控制综合。我们在一个涉及四旋翼电机受攻击的仿真案例研究中展示了所提方法的有效性。