一种云环境中硬件安全模块的形式化验证配置
密码学与安全
2021-09-29 v1
摘要
硬件安全模块(HSM)是在关键生态系统中执行敏感操作的受信机器。金融与政府数字服务通常依法要求使用 HSM。HSM 最重要的特性是能在防篡改硬件内存储敏感凭证与密码学密钥,从而每个操作均通过合适的 API 在内部完成,且此类敏感数据从不暴露于设备之外。HSM 现便捷地以云形式提供,即物理机器由某供应商远程托管,客户可通过标准 API 访问。在此场景下,将敏感数据保留于设备内的性质更为重要,因为脆弱的应用可能将完整 API 暴露给攻击者。遗憾的是,过去 20 余年间已发现大量实用的 API 层攻击,并证明在真实设备中可行。PKCS#11(HSM 最流行的标准 API)的最新版本未解决这些问题,遗留了所有可能的缺陷。本文中,我们提出首个安全的 HSM 配置,其无需对 PKCS#11 API 做任何限制或修改,且适用于云 HSM 方案——其中对标准 API 的合规性至关重要。该配置依赖于在不同 HSM 用户间谨慎的职责分离,使得已知 API 缺陷无法被任何控制应用的攻击者利用。我们通过在最先进的 Tamarin 证明器中提供形式化模型证明了该配置的正确性,并展示了如何在真实云 HSM 方案中实施该配置。
引用
@article{arxiv.2109.13631,
title = {A Formally Verified Configuration for Hardware Security Modules in the Cloud},
author = {Riccardo Focardi and Flaminia L. Luccio},
journal= {arXiv preprint arXiv:2109.13631},
year = {2021}
}
备注
To appear at ACM CCS 2021