桥接威胁模型与检测：通过 CADP 进行形式化验证

威胁检测系统依赖基于规则的逻辑来识别对抗行为，但这些规则与高层威胁模型的一致性很少得到形式化验证。我们提出一个形式化验证框架，将检测逻辑和攻击树均建模为标记迁移系统（LTS），从而通过互模拟和弱迹包含实现自动化一致性检查。以通用威胁检测语言（GTDL，我们在本工作中形式化的一种通用检测语言）指定的检测规则被赋予组合操作语义，而以攻击树形式表达的威胁模型则通过结构化迹语义解释为 LTS。两种表示都被转换为 LNT，这是一种由 CADP 工具箱支持的建模语言。这一共同的语义域使得对检测覆盖率的系统化、自动化验证成为可能。我们在 LokiBot 和 Emotet 等真实恶意软件场景上评估了我们的方法，并通过参数化合成模型提供了可扩展性分析。结果证实，我们的方法能够识别威胁模型与检测规则之间的语义不匹配，支持迭代细化，并可扩展到现实的威胁环境。