SpecMon: 安全协议的模块化黑盒运行时监控
密码学与安全
2024-09-05 v1
摘要
形式化协议规范与其实际实现之间存在验证鸿沟，本工作旨在通过监控其是否符合形式化规范来弥合这一鸿沟。我们对应用程序使用的网络与密码学库进行插桩，以获取事件流。即使在没有源代码访问权限的情况下，这也是可行的。随后，我们使用一种高效算法将这些观测结果与规范模型中的有效迹相匹配。与以往工作不同，我们的算法能够处理非确定性，从而支持多会话。它还实现了低开销，我们在WireGuard参考实现和以往工作的案例研究中对此进行了证明。我们发现WireGuard的参考Tamarin模型几乎无需修改即可使用：我们只需指定线路格式，并纠正了在开展案例研究时发现的一些小误差。我们还为我们的算法提供了可靠性证明，确保其仅接受根据规范模型有效的事件流。
引用
@article{arxiv.2409.02918,
title = {SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols},
author = {Kevin Morio and Robert Künnemann},
journal= {arXiv preprint arXiv:2409.02918},
year = {2024}
}
备注
21 pages, Full version of the corresponding ACM CCS '24 paper