暗中监控：面向网络-物理系统的隐私保护运行时验证

在分布式网络-物理系统和物联网应用中，系统节点将测量值发送给用于检查这些测量值是否满足给定正式规范的监控器。例如在城市空中交通领域，地方交通 authority 将监控无人机交通以评估其流量并检测新出现的异常模式。某些应用需要规范和测量值都保持私有——即仅由其所有者知晓。例子包括交通监控、集成电路设计测试以及通过可穿戴或植入式设备进行的医疗监控。在本文中，我们提出了一种协议，使隐私保护的鲁棒性监控成为可能。通过遵循我们的协议，系统（例如无人机）和监控器（例如交通 authority）仅学习测量轨迹相对于规范的鲁棒性。但系统对公式一无所知，监控器对被监控的信号也一无所知。我们利用 garbled circuits 实现这一点，针对以时序状态序列解释的 Signal Temporal Logic 规范。我们分析了隐私保护的运行时和内存开销、电路规模，以及在设计测试、离线监控和在线监控三个不同用例场景下的实际可行性。