Provably Correct, Secure, and Leakage-Free Systems:
From Application Specification to Circuit-Level Implementation

by Anish Athalye

Thesis Defense · 15 July 2024, 2pm ET · MIT CSAIL + Zoom (registration required)


Abstract. Critical hardware and software systems such as hardware security modules (HSMs) are susceptible to bugs and timing side-channel vulnerabilities. Timing leakage is particularly hard to eliminate because leakage is an emergent property that can arise from subtle behaviors or interactions between hardware and software components in the entire system, with root causes such as non-constant-time code, compiler-generated timing variations, and microarchitectural side channels. This thesis contributes a new approach using formal verification to rule out such bugs and build provably correct, secure, and leakage-free systems.

The approach introduces a new theory called information-preserving refinement (IPR) for capturing non-leakage in addition to correctness and security, implements a verification approach for IPR in the K2 framework, and applies it to verifying hardware security modules. Using K2, a developer can verify that an HSM implementation leaks no more information than is allowed by a succinct application-level specification of the device’s intended behavior, with proofs covering the implementation’s hardware and software down to its cycle-precise wire-I/O-level behavior.

An evaluation using K2 verifies several HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of Ibex and PicoRV32-based hardware platforms. K2 provides strong guarantees for these HSMs: for example, it proves that the ECDSA-on-Ibex implementation—2,300 lines of code and 13,500 lines of Verilog—leaks nothing more than what is allowed by a 50-line specification of its behavior.


Attend

PhD thesis defense talks are open to the public, both in-person and over Zoom.

When: 15 July 2024, 2pm ET (Google Calendar, Outlook, ICS)

Where: MIT CSAIL, 32-G882 (RSVP appreciated but not required)

Zoom: RSVP required


Formal verification is a promising approach to building secure computer systems because it can systematically eliminate entire classes of bugs that can lead to compromises. The main contribution of this thesis is a new formalism and approach for proving the absence of bugs that leak information, such as timing side channels, in addition to preventing correctness bugs in hardware and software. The thesis applies this approach to verifying hardware security modules, with proofs covering their entire hardware and software stack down to the wire-I/O level.

Context: hardware security modules

Hardware security modules (HSMs) are widely used as a building block in computer systems where core security functionality is factored out onto this physically-separate device with special-purpose hardware and software. The figure below illustrates this setup: the HSM is an independent system—with its own CPU, firmware, RAM, and persistent memory—connected over an I/O interface (UART, in this example) to the host machine. The HSM interacts with the outside world solely through its I/O interface to the host.

Host-HSM setup

A certificate authority server connected to an ECDSA signing HSM over a UART interface.

The pseudocode below shows the application-level specification for this example—an ECDSA signing HSM.

ECDSA HSM spec pseudocode

Pseudocode specification for the ECDSA signing HSM. The specification exposes an operation to initialize internal state and to sign messages, but it does not expose an operation that returns the signing key.

There are billions of deployed HSMs across a variety of server-side and client-side applications. For example, on the server side, certificate authorities like Let’s Encrypt use HSMs to store their signing key and sign certificates [1]; cloud providers including Apple, Google, and WhatsApp use HSMs to enforce guess limits for cloud backup keys protected by low-entropy PINs [2, 3, 4]; and credit card networks use HSMs for PIN translation [5]. On the client side, the iPhone uses its secure enclave processor to safeguard data encryption keys [6] and users rely on USB security keys to protect their authentication keys in the face of a compromised computer [7]. While the term hardware security module traditionally refers to devices used on the server side (and often specifically to HSMs implementing the PKCS#11 API [8]), this thesis uses the term to refer to all such special-purpose hardware/software systems that factor out core security functionality.

HSMs defend against a class of attacks where an adversary gains access to the host machine that the HSM is connected to: even if the adversary compromises the host machine, the adversary only gains query access to the HSM, not direct access to its internal state. Protecting secret state behind a carefully-designed API enables the HSM to enforce key security properties. For example, with the ECDSA signing HSM specified in the pseudocode above, an adversary that compromises the server cannot extract the signing key because the HSM API does not expose an operation that returns the key. As another example, in cloud backup systems, an adversary that compromises the backup server cannot bypass the PIN guess limits or extract the decryption key because the HSM API enforces guess limits and only returns the decryption key when provided the correct PIN.

Motivation

Although HSMs are relatively simple, any vulnerability in their hardware or software can undermine their security. HSMs have suffered from bugs throughout the hardware/software stack, such as logic bugs, memory corruption, hardware bugs, and timing side channels [9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22], motivating the need for a systematic approach to eliminating such bugs.

Mechanized proofs, which connect an implementation to a mathematical specification through a computer-checked proof, have shown promise in eliminating entire classes of bugs in both hardware [23] and software [24, 25, 26, 27]. Empirically, such systems are effective in eliminating bugs in their verified components [28].

Information leakage, such as timing side-channel leakage [29], is one important class of security vulnerability that has proven to be particularly hard to eliminate [30, 31, 32, 33, 34, 35]. Much work in verified systems has focused on eliminating correctness bugs. However, proving the absence of bugs that leak information has been particularly challenging. Traditional approaches that focus on verifying correctness at a particular level of abstraction (e.g., C code) have a hard time capturing information leakage, because lower layers of abstraction (e.g., execution at the hardware level) introduce new observables (e.g., cycle-precise timing behavior) that do not even exist at higher levels but can leak information.

HSMs are an ideal proving ground for a new approach to systematically ruling out correctness, security, and leakage bugs because they (1) are widely-used devices for which security is critical, warranting the effort required for formal verification, (2) suffer from security bugs in practice, and (3) are complete but simple enough computer systems to be amenable to an experimental verification effort.

Threat model

This thesis considers an adversary that gains direct access to the wire-level digital I/O of the HSM, with the ability to set logic levels on the input wires and read logic levels on the output wires at every cycle. This captures many realistic attacks, such as an adversary that compromises the host machine and is able to send malformed commands or observe all wire-level outputs at every clock cycle. Such an adversary may be able to extract secrets from an HSM, even if that HSM operates correctly when the host machine is well-behaved.

This threat model is focused on remote compromise of the host machine, one of the primary attacks that HSMs aim to defend against. It does not include physical attacks on the HSM. While the threat model includes (digital) timing side channels, it does not include arbitrary side channels [36] such as electromagnetic radiation [37], temperature [38], and power [39].

State of the art

The security community has long been aware of the importance and practical impact of timing vulnerabilities in cryptography [40, 41], and more broadly, unintended leakage by computer systems. However, prior to this thesis, there were no results verifying non-leakage end-to-end from an application-level specification down to the cycle-accurate level in hardware.

Some production libraries including BoringSSL, Mbed TLS, and Amazon s2n use approaches based on software testing to validate constant-time execution of cryptographic routines [42, 43, 44]. Several systems, including some like HACL* that are used in production, provide formal guarantees about side-channel resistance at the software level [27, 45, 46], but the guarantees do not extend down to the hardware level. Recent work on leakage models [47, 48, 49, 50, 51, 52] focuses on software or hardware but also does not yet provide end-to-end guarantees. Prior work on end-to-end verified hardware/software systems [53, 54, 55, 56, 57] focuses on correctness, not security and non-leakage.

Approach

This thesis presents K2, a new approach using formal verification to systematically eliminate leakage bugs in addition to correctness and security bugs in hardware/software systems. The K2 approach relates the behavior of the physical implementation at the wire level interface—the ground truth of what the host machine controls and observes at the digital level, which captures timing channels at a cycle-accurate level—to a functional specification of the methods that the HSM exposes. In the example ECDSA HSM implementation: the host connects to the HSM via two input wires and two output wires, which the host can read/write at every cycle. The ECDSA pseudocode above showed the functional specification for this HSM. It exposes two operations, initialize and sign. The specification ensures unique nonces across operations, prevents nonce reuse, and does not have an operation for reading back the PRF key or signing key.

K2 relates a physical implementation to a functional specification with a new definition called information-preserving refinement (IPR), illustrated in the figure below. IPR is inspired by formalizations of zero knowledge in cryptography [58, 59, 60] and uses the real/ideal paradigm to define security.

IPR illustration

An illustration of the definition of IPR, an indistinguishability between a real world and an ideal world, applied to HSMs.

IPR defines a real world that models the host’s view of the HSM in the real world under our threat model, and it defines an ideal world that is set up to be correct and secure by construction. The IPR definition states that the real world and ideal world must be indistinguishable, capturing the notion that the implementation implements the spec and that its wire-level I/O behavior leaks no additional information.

In IPR, a driver describes the I/O protocol that a host machine can follow to get correct results from the HSM, describing how each spec-level operation translates to wire-level I/O with the HSM. The driver is a part of the specification (and is trusted). Its dual, an emulator, is a proof artifact that describes how wire-level behavior can be explained in terms of spec-level operations. The existence of an emulator shows that no matter what wire-level inputs are given to the device (including inputs that violate the I/O protocol), its outputs reveal no more information than the specification.

To verify HSMs with IPR, K2 introduces a new HSM software architecture to enable separate proofs of software and hardware, an approach to verifying IPR for HSMs that follow this design, frameworks to support mechanical proofs of IPR for software and hardware, and metatheory tying everything together. The figure below summarizes the developer workflow for implementing and verifying an HSM with K2.

K2 workflow

The K2 developer workflow. The app developer writes the components in blue, and the platform developer writes the components in red. The developer uses tools and frameworks provided by K2 to verify IPR.

The application developer writes a top-level functional specification, an implementation (at roughly the C code level), and a computer-checked proof of IPR between the app spec and the app implementation, supported by K2’s Starling framework for verifying IPR for software. The platform developer writes system software and the hardware implementation, along with a computer-checked proof of IPR between the app implementation and the complete system-on-a-chip (SoC), supported by K2’s Knox framework for verifying IPR for hardware. Formally-verified metatheory supplied by K2 ties these proofs together to yield the final IPR between the functional specification and the SoC.

Contributions

This thesis contributes:

A new formalism for modeling and reasoning about leakage. We introduce information-preserving refinement (IPR) to relate implementations to specifications and capture the notion that the implementation leaks no more information than the specification. Using the Coq proof assistant, we formalize the theory of IPR, including four verified proof strategies for IPR used in different parts of K2.

A framework for verifying non-leakage for hardware security modules. We develop the K2 framework, which introduces a new software architecture for HSMs that enables a modular proof approach. K2 consists of two frameworks that implement the proof strategies we have verified in Coq: the Starling framework for reasoning about software and the Knox framework for reasoning about hardware. The Knox framework introduces two artifacts that are usable outside the context of K2: the Rosys Verilog-to-Rosette toolchain and the Riscette executable Rosette semantics for CompCert RISC-V assembly.

Verified HSMs. To evaluate the IPR definition and the K2 framework, we implement and verify several HSMs. This includes an ECDSA signing HSM, where we use K2 to prove that an implementation (written in 2,300 lines of code and 13,500 lines of Verilog) satisfies a concise specification written in 50 lines of code.

This thesis applies IPR to HSMs, but we believe the definition is broadly applicable to other contexts for capturing non-leakage properties. Furthermore, we believe that many ideas introduced in Knox and its constituent components like Rosys and Riscette are generally applicable for formal reasoning about hardware/software systems.

Prior publications

This thesis expands upon work covered in three papers:


The above is a preview of the thesis — the complete document will be published in early August. Follow me to stay up-to-date on the thesis document release, associated blog posts, open-source code release, and more.