Showing 1–8 of 8 results for author: Cauligi, S

Testing side-channel security of cryptographic implementations against future microarchitectures

Authors: Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom

Abstract: How will future microarchitectures impact the security of existing cryptographic implementations? As we cannot keep reducing the size of transistors, chip vendors have started develo** new microarchitectural optimizations to speed up computation. A recent study (Sanchez Vicarte et al., ISCA 2021) suggests that these optimizations might open the Pandora's box of microarchitectural attacks. Howeve… ▽ More How will future microarchitectures impact the security of existing cryptographic implementations? As we cannot keep reducing the size of transistors, chip vendors have started develo** new microarchitectural optimizations to speed up computation. A recent study (Sanchez Vicarte et al., ISCA 2021) suggests that these optimizations might open the Pandora's box of microarchitectural attacks. However, there is little guidance on how to evaluate the security impact of future optimization proposals. To help chip vendors explore the impact of microarchitectural optimizations on cryptographic implementations, we develop (i) an expressive domain-specific language, called LmSpec, that allows them to specify the leakage model for the given optimization and (ii) a testing framework, called LmTest, to automatically detect leaks under the specified leakage model within the given implementation. Using this framework, we conduct an empirical study of 18 proposed microarchitectural optimizations on 25 implementations of eight cryptographic primitives in five popular libraries. We find that every implementation would contain secret-dependent leaks, sometimes sufficient to recover a victim's secret key, if these optimizations were realized. Ironically, some leaks are possible only because of coding idioms used to prevent leaks under the standard constant-time model. △ Less

Submitted 1 February, 2024; originally announced February 2024.

Robust Constant-Time Cryptography

Authors: Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan

Abstract: The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory accesses, and thus avoids leaking secrets through cache and timing side-channels. The constant-time property makes a number of implicit assumptions that are fundamentally at odds with the reality of cryptographic code.… ▽ More The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory accesses, and thus avoids leaking secrets through cache and timing side-channels. The constant-time property makes a number of implicit assumptions that are fundamentally at odds with the reality of cryptographic code. Constant-time is not robust. The first issue with constant-time is that it is a whole-program property: It relies on the entirety of the code base being constant-time. But, cryptographic developers do not generally write whole programs; rather, they provide libraries and specific algorithms for other application developers to use. As such, developers of security libraries must maintain their security guarantees even when their code is operating within (potentially untrusted) application contexts. Constant-time requires memory safety. The whole-program nature of constant-time also leads to a second issue: constant-time requires memory safety of all the running code. Any memory safety bugs, whether in the library or the application, will wend their way back to side-channel leaks of secrets if not direct disclosure. And although cryptographic libraries should (and are) written to be memory-safe, it is unfortunately unrealistic to expect the same from every application that uses each library. We formalize robust constant-time and build a RobustIsoCrypt compiler that transforms the library code and protects the secrets even when they are linked with untrusted code. Our evaluation with SUPERCOP benchmarking framework shows that the performance overhead is less than five percent on average. △ Less

Submitted 9 November, 2023; originally announced November 2023.

A Turning Point for Verified Spectre Sandboxing

Authors: Sunjay Cauligi, Marco Guarnieri, Daniel Moghimi, Deian Stefan, Marco Vassena

Abstract: Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to block Spectre attacks, but to date, very few have been formally vetted; most are "best effort" strategies. Formal guarantees are particularly crucial for protecting isolated environments like sandboxing against Spectre atta… ▽ More Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to block Spectre attacks, but to date, very few have been formally vetted; most are "best effort" strategies. Formal guarantees are particularly crucial for protecting isolated environments like sandboxing against Spectre attacks. In such environments, a subtle flaw in the mitigation would allow untrusted code to break out of the sandbox and access trusted memory regions. In our work, we develop principled foundations to build isolated environments resistant against Spectre attacks. We propose a formal framework for reasoning about sandbox execution and Spectre attacks. We formalize properties that sound mitigation strategies must fulfill and we show how various existing mitigations satisfy (or fail to satisfy!) these properties. △ Less

Submitted 2 August, 2022; originally announced August 2022.

SoK: Practical Foundations for Software Spectre Defenses

Authors: Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan

Abstract: Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with th… ▽ More Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with these attacks in a principled way, the research community has sought formal foundations for speculative execution upon which to rebuild provable security guarantees. This paper systematizes the community's current knowledge about software verification and mitigation for Spectre. We study state-of-the-art software defenses, both with and without associated formal models, and use a cohesive framework to compare the security properties each defense provides. We explore a wide variety of tradeoffs in the expressiveness of formal frameworks, the complexity of defense tools, and the resulting security guarantees. As a result of our analysis, we suggest practical choices for developers of analysis and mitigation tools, and we identify several open problems in this area to guide future work on grounded software defenses. △ Less

Submitted 8 April, 2022; v1 submitted 12 May, 2021; originally announced May 2021.

Comments: To appear at Oakland '22

Swivel: Hardening WebAssembly against Spectre

Authors: Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang, Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, Deian Stefan

Abstract: We describe Swivel, a new compiler framework for hardening WebAssembly (Wasm) against Spectre attacks. Outside the browser, Wasm has become a popular lightweight, in-process sandbox and is, for example, used in production to isolate different clients on edge clouds and function-as-a-service platforms. Unfortunately, Spectre attacks can bypass Wasm's isolation guarantees. Swivel hardens Wasm agains… ▽ More We describe Swivel, a new compiler framework for hardening WebAssembly (Wasm) against Spectre attacks. Outside the browser, Wasm has become a popular lightweight, in-process sandbox and is, for example, used in production to isolate different clients on edge clouds and function-as-a-service platforms. Unfortunately, Spectre attacks can bypass Wasm's isolation guarantees. Swivel hardens Wasm against this class of attacks by ensuring that potentially malicious code can neither use Spectre attacks to break out of the Wasm sandbox nor coerce victim code-another Wasm client or the embedding process-to leak secret data. We describe two Swivel designs, a software-only approach that can be used on existing CPUs, and a hardware-assisted approach that uses extension available in Intel 11th generation CPUs. For both, we evaluate a randomized approach that mitigates Spectre and a deterministic approach that eliminates Spectre altogether. Our randomized implementations impose under 10.3% overhead on the Wasm-compatible subset of SPEC 2006, while our deterministic implementations impose overheads between 3.3% and 240.2%. Though high on some benchmarks, Swivel's overhead is still between 9x and 36.3x smaller than existing defenses that rely on pipeline fences. △ Less

Submitted 19 March, 2021; v1 submitted 25 February, 2021; originally announced February 2021.

Comments: Accepted at USENIX 21

MSC Class: D.4.6 ACM Class: D.4.6

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.

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.

Comments: To appear at PLDI '20

CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem

Authors: Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, Deian Stefan

Abstract: A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the "web ecosystem" - the wide variety of technologies that collectively underpins the modern World Wide Web. With the new introduction of the WebAssembly byt… ▽ More A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the "web ecosystem" - the wide variety of technologies that collectively underpins the modern World Wide Web. With the new introduction of the WebAssembly bytecode language (Wasm) into the web ecosystem, we have a unique opportunity to advance a principled alternative to existing JavaScript cryptography use cases which does not compromise this convenience. We present Constant-Time WebAssembly (CT-Wasm), a type-driven strict extension to WebAssembly which facilitates the verifiably secure implementation of cryptographic algorithms. CT-Wasm's type system ensures that code written in CT-Wasm is both information flow secure and resistant to timing side channel attacks; like base Wasm, these guarantees are verifiable in linear time. Building on an existing Wasm mechanization, we mechanize the full CT-Wasm specification, prove soundness of the extended type system, implement a verified type checker, and give several proofs of the language's security properties. We provide two implementations of CT-Wasm: an OCaml reference interpreter and a native implementation for Node.js and Chromium that extends Google's V8 engine. We also implement a CT-Wasm to Wasm rewrite tool that allows developers to reap the benefits of CT-Wasm's type system today, while develo** cryptographic algorithms for base Wasm environments. We evaluate the language, our implementations, and supporting tools by porting several cryptographic primitives - Salsa20, SHA-256, and TEA - and the full TweetNaCl library. We find that CT-Wasm is fast, expressive, and generates code that we experimentally measure to be constant-time. △ Less

Submitted 17 December, 2018; v1 submitted 3 August, 2018; originally announced August 2018.

Comments: 29 pages, 9 figures