A Formally Verified Configuration for Hardware Security Modules in the Cloud

TL;DR

This paper presents a formally verified configuration for cloud-based Hardware Security Modules that enhances security without modifying existing APIs, addressing longstanding API-level vulnerabilities.

Contribution

It introduces the first secure HSM configuration compatible with standard APIs like PKCS#11, verified with formal methods, and applicable to real cloud HSM implementations.

Findings

The configuration prevents known API-level attacks.

Formal proof of correctness using Tamarin prover.

Implementation guidance for real cloud HSMs.

Abstract

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.