SaTC: CORE: Medium: Verifying Hardware Security Modules with Information-Preserving Refinement

硬件安全模块（hsm）广泛用于保护系统的关键部分免受强大的攻击，例如获得对主机的完全控制。例如，用于通过双因素身份验证登录web应用程序的USB安全密钥存储了一个秘密密钥，即使攻击者破坏了用户的计算机也无法获得该密钥。然而，在hms实施过程中出现的错误可能会破坏其安全性；例如，运行在HSM上的软件中的错误或HSM硬件中的错误可能会无意中泄露HSM的密钥。该项目的新颖之处在于支持hsm的开发，这些hsm的实现保证满足精确的安全规范，从而排除了上述错误的可能性。该项目旨在生产一个原型验证HSM，类似于证书颁发机构用于签署网站证书或加密货币硬件钱包的HSM。该项目更广泛的意义和重要性在于显著提高hsm的可信度。本项目采用的技术方法是使用形式化验证从数学上证明高速切削机床的正确性和安全性，包括其硬件和软件。该项目旨在确保安全性，即使是针对可能试图利用定时通道的对手——也就是说，根据执行某些操作所需的时间从HSM中提取信息。一个关键的挑战在于提出一种精确指定HSM预期行为的方法，以及在存在定时通道的情况下，将HSM实现与这样的规范关联起来的相应的安全性定义。另一个挑战在于减少证明工作量；该项目使用符号执行来自动化证明的重要部分，但也结合了开发人员提供的提示来处理自动化工具无法处理的复杂步骤。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Hardware security modules (HSMs) are widely used for protecting critical parts of a system against powerful attacks, such as gaining complete control of the host computer. For example, USB security keys used for logging into web applications with two-factor authentication store a secret key that cannot be obtained even by an adversary that compromises the user's computer. However, mistakes in the implementation of HSMs can undermine their security; for example, bugs in the software running on the HSM or bugs in the HSM hardware can inadvertently disclose the HSM's secret key. The project's novelty is in enabling the development of HSMs whose implementations are guaranteed to meet a precise security specification, ruling out the possibility of bugs like the ones mentioned above. The project aims to produce a prototype verified HSM similar to an HSM used by certificate authorities to sign certificates for web sites, or a cryptocurrency hardware wallet. The project's broader significance and importance is in significantly increasing the trustworthiness of HSMs.The technical approach taken by this project is to use formal verification to mathematically prove the correctness and security of an HSM, including both its hardware and software. This project aims to ensure security even against adversaries that may attempt to take advantage of timing channels---that is, extracting information from an HSM based on how long it takes to perform certain operations. A key challenge lies in coming up with a way of precisely specifying the expected behavior of an HSM, and a corresponding definition of security that relates an HSM implementation to such a specification, in the presence of timing channels. Another challenge lies in reducing the proof effort; this project uses symbolic execution to automate significant parts of the proof, but also incorporate developer-provided hints to handle complex steps that cannot be handled by automated tools.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.