Learn, Check, Test —— 使用自动机学习与模型检验进行安全测试

摘要

信息物理系统是工业系统和关键基础设施的重要组成部分。因此，需要以全面方式检查其正确性和安全性。同时，此类系统的复杂性要求检查过程系统化，并尽可能实现自动化以提高效率和准确性。模型检验是在此背景下有用的方法，但需要能忠实表示被检系统行为的模型。由于长供应链或保密性等原因，许多系统只能在黑盒设置下进行检查，因此获取此类模型并非易事。

我们利用主动黑盒学习技术，以Mealy机形式推断此类系统的行为模型，并将其转换为可由模型检验器评估的形式。为此，我们将信息物理系统作为黑盒，通过其外部通信接口进行研究。首先使用上下文命题映射（CPMs）将相应协议的上下文信息映射到模型，从而为模型添加命题。我们获得类似于Kripke结构的带标注Mealy机。然后正式定义模板，将结构转换为模型检验器兼容的格式。

我们基于基本安全需求定义通用安全属性。由于使用了CPMs，我们可以用有意义的上下文实例化这些属性来检查特定协议，这使得方法具有灵活性和可扩展性。获得的模型可以轻松修改以引入非确定性行为（如超时）或故障，并检查属性是否仍然满足。最后，我们通过不同通信协议（NFC和UDS）的案例研究展示了该方法的通用性，这些案例使用相同的工具链和相同的安全属性进行检查。

技术细节

研究领域：密码学与安全（cs.CR）、形式语言与自动机理论（cs.FL）
方法特点：结合自动机学习与模型检验的黑盒安全测试
技术组件：Mealy机、Kripke结构、上下文命题映射（CPMs）
验证协议：近场通信（NFC）、统一诊断服务（UDS）
工具支持：完整的工具链支持

元数据

页数：19页
图表：5张图，2个表格
提交状态：预印本，已提交至Elsevier Computers & Security
DOI：https://doi.org/10.48550/arXiv.2509.22215