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

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

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.