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

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

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.