-
Solver-Aided Constant-Time Circuit Verification
Authors:
Rami Gokhan Kici,
Klaus v. Gleissenthall,
Deian Stefan,
Ranjit Jhala
Abstract:
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verification failures via a new notion of constant-time counterexamples, which Xenon uses to automatically synthesize a minimal set of secrecy assumptions. Xenon further exp…
▽ More
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verification failures via a new notion of constant-time counterexamples, which Xenon uses to automatically synthesize a minimal set of secrecy assumptions. Xenon further exploits modularity in Verilog code via a notion of module summaries, thereby avoiding duplicate work across multiple module instantiations. We show how Xenon's assumption synthesis and summaries enable the verification of a variety of circuits including AES, a highly modular AES-256 implementation where modularity cuts verification from six hours to under three seconds, and ScarV, a timing channel hardened RISC-V micro-controller whose size exceeds previously verified designs by an order of magnitude.
△ Less
Submitted 1 April, 2021;
originally announced April 2021.
-
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Authors:
Marco Vassena,
Craig Disselkoen,
Klaus V. Gleissenthall,
Sunjay Cauligi,
Rami Gökhan Kici,
Ranjit Jhala,
Dean Tullsen,
Deian Stefan
Abstract:
We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via speculation, it suffices to $\textit{cut}$ the dataflow from expressions that speculatively introduce secrets ($\textit{sources}$) to those that leak them through the cache ($\textit{sinks}$), rather than prohibit speculation…
▽ More
We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via speculation, it suffices to $\textit{cut}$ the dataflow from expressions that speculatively introduce secrets ($\textit{sources}$) to those that leak them through the cache ($\textit{sinks}$), rather than prohibit speculation altogether. We formalize this insight in a $\textit{static type system}$ that (1) types each expression as either $\textit{transient}$, i.e., possibly containing speculative secrets or as being $\textit{stable}$, and (2) prohibits speculative leaks by requiring that all $\textit{sink}$ expressions are stable. BLADE relies on a new new abstract primitive, $\textbf{protect}$, to halt speculation at fine granularity. We formalize and implement $\textbf{protect}$ using existing architectural mechanisms, and show how BLADE's type system can automatically synthesize a $\textit{minimal}$ number of $\textbf{protect}$s to provably eliminate speculative leaks. We implement BLADE in the Cranelift WebAssembly compiler and evaluate our approach by repairing several verified, yet vulnerable WebAssembly implementations of cryptographic primitives. We find that Blade can fix existing programs that leak via speculation $\textit{automatically}$, without user intervention, and $\textit{efficiently}$ even when using fences to implement $\textbf{protect}$.
△ Less
Submitted 7 December, 2020; v1 submitted 1 May, 2020;
originally announced May 2020.
-
Iodine: Verifying Constant-Time Execution of Hardware
Authors:
Klaus v. Gleissenthall,
Rami Gökhan Kıcı,
Deian Stefan,
Ranjit Jhala
Abstract:
To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing channels are ubiquitous in modern hardware, due to its labyrinthine fast-paths and optimizations. A promising way to avoid timing vulnerabilities is to devise --- and verify --- conditions under which a hardware design is…
▽ More
To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing channels are ubiquitous in modern hardware, due to its labyrinthine fast-paths and optimizations. A promising way to avoid timing vulnerabilities is to devise --- and verify --- conditions under which a hardware design is free of timing variability, i.e., executes in constant-time. In this paper, we present Iodine: a clock precise, constant-time approach to eliminating timing side channels in hardware. Iodine succeeds in verifying various open source hardware designs in seconds and with little developer effort. Iodine also discovered two constant-time violations: one in a floating-point unit and another one in an RSA encryption module.
△ Less
Submitted 7 October, 2019;
originally announced October 2019.
-
Constant-Time Foundations for the New Spectre Era
Authors:
Sunjay Cauligi,
Craig Disselkoen,
Klaus v. Gleissenthall,
Dean Tullsen,
Deian Stefan,
Tamara Rezk,
Gilles Barthe
Abstract:
The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time a…
▽ More
The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time as it exists today far less useful.
This paper lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries.
△ Less
Submitted 8 May, 2020; v1 submitted 3 October, 2019;
originally announced October 2019.
-
An Epistemic Perspective on Consistency of Concurrent Computations
Authors:
Klaus v. Gleissenthall,
Andrey Rybalchenko
Abstract:
Consistency properties of concurrent computations, e.g., sequential consistency, linearizability, or eventual consistency, are essential for devising correct concurrent algorithms. In this paper, we present a logical formalization of such consistency properties that is based on a standard logic of knowledge. Our formalization provides a declarative perspective on what is imposed by consistency req…
▽ More
Consistency properties of concurrent computations, e.g., sequential consistency, linearizability, or eventual consistency, are essential for devising correct concurrent algorithms. In this paper, we present a logical formalization of such consistency properties that is based on a standard logic of knowledge. Our formalization provides a declarative perspective on what is imposed by consistency requirements and provides some interesting unifying insight on differently looking properties.
△ Less
Submitted 10 May, 2013;
originally announced May 2013.
