云中硬件安全模块的正式验证配置
A Formally Verified Configuration for Hardware Security Modules in the Cloud
摘要：
硬件安全模块（HSM）是在关键生态系统中执行敏感操作的可信机器。它们通常是金融和政府数字服务中的法律要求。HSM最重要的功能是它能够将敏感凭据和加密密钥存储在防篡改硬件中，因此每个操作都是通过合适的API在内部完成的，并且这些敏感数据永远不会暴露在设备之外。HSM现在可以方便地在云中提供，这意味着物理机由某些提供商远程托管，客户可以通过标准API访问它们。在此设置中，将敏感数据保存在设备内的属性更为重要，因为易受攻击的应用程序可能会将完整的API暴露给攻击者。不幸的是，在过去的20多年里，已经发现了大量实用的API级攻击，并在实际设备中证明是可行的。最新版本的PKCS#11是最流行的HSM标准API，它没有解决这些问题，可能会留下所有缺陷。在本文中，我们提出了第一个安全的HSM配置，不需要对PKCS#11 API进行任何限制或修改，并且适用于云HSM解决方案，其中遵守标准API至关重要。该配置依赖于不同HSM用户之间的角色的仔细分离，以便已知的API漏洞不会被任何控制应用程序的攻击者利用。我们通过在最先进的Tamarin证明器中提供正式模型来证明配置的正确性，并展示如何在真正的云HSM解决方案中实现配置。
英文摘要：
Hardware Security Modules (HSMs) are trusted machines that perform sensitive operations in critical ecosystems. They are usually required by law in financial and government digital services. The most important feature of an HSM is its ability to store sensitive credentials and cryptographic keys inside a tamper-resistant hardware, so that every operation is done internally through a suitable API, and such sensitive data are never exposed outside the device. HSMs are now conveniently provided in the cloud, meaning that the physical machines are remotely hosted by some provider and customers can access them through a standard API. The property of keeping sensitive data inside the device is even more important in this setting as a vulnerable application might expose the full API to an attacker. Unfortunately, in the last 20+ years a multitude of practical API-level attacks have been found and proved feasible in real devices. The latest version of PKCS#11, the most popular standard API for HSMs, does not address these issues leaving all the flaws possible. In this paper, we propose the first secure HSM configuration that does not require any restriction or modification of the PKCS#11 API and is suitable to cloud HSM solutions, where compliance to the standard API is of paramount importance. The configuration relies on a careful separation of roles among the different HSM users so that known API flaws are not exploitable by any attacker taking control of the application. We prove the correctness of the configuration by providing a formal model in the state-of-the-art Tamarin prover and we show how to implement the configuration in a real cloud HSM solution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
