Publications

Analyzing and Exploiting Branch Mispredictions in Microcode

Published in arXiv preprint, 2025

We present µSpectre, a new class of transient execution attacks that exploit microcode branch mispredictions to transiently leak sensitive data. We find that many long-known and recently-discovered transient execution attacks, which were previously categorized as Spectre or Meltdown variants, are actually instances of µSpectre on some Intel microarchitectures. Based on our observations, we discover multiple new µSpectre attacks and present a defense against µSpectre vulnerabilities, called µSLH.

Recommended citation: Nicholas Mosier, Hamed Nemati, John C. Mitchell, Caroline Trippel. Analyzing and exploiting branch mispredictions in microcode, arXiv preprint. https://doi.org/10.48550/arXiv.2501.12890

Serberus: Protecting Cryptographic Code from Spectres at Compile-Time

Published in S&P'24, 2024

We present Serberus, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL, and/or PSF speculation primitives) on existing hardware. Serberus is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by software analyses. Second, conformance to the accepted CT code discipline permits two code patterns that are unsafe in the post-Spectre era. Third, once these code patterns are addressed, all Spectre leakage of secrets in CT programs can be attributed to one of four classes of taint primitives—instructions that can transiently assign a secret value to a publicly-typed register. We evaluate Serberus on cryptographic primitives in the OpenSSL, Libsodium, and HACL* libraries. Serberus introduces 21.3% runtime overhead on average, compared to 24.9% for the next closest state-of-the-art software mitigation, which is less secure.

Recommended citation: N. Mosier, H. Nemati, J. Mitchell and C. Trippel, Serberus: Protecting Cryptographic Code from Spectres at Compile-Time, in 2024 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2024 pp. 48-48. doi: 10.1109/SP54263.2024.00048

Hardware-Software Codesign for Mitigating Spectre

Published in PLARCH'23 Workshop at ISCA'23, 2023

Spectre attacks exploit control- and data-flow (mis)prediction on modern processors to transiently leak program secrets. Comprehensively mitigating Spectre leakage is hard, and doing so while preserving the program’s performance is even harder: no existing Spectre mitigations are widely deployed due to their high overhead or high complexity. We claim that a comprehensive, efficient, and low-complexity mitigation for Spectre attacks requires engaging in software-compiler-hardware co-design. In our talk, we will pitch such a co-designed Spectre mitigation that will be widely deployable at a low cost in security-critical applications. As a first step towards this goal, we have developed Serberus, a comprehensive and proven-correct Spectre mitigation for constant-time code that targets existing hardware. We are currently exploring lightweight hardware support to improve Serberus’ performance in other application domains.

Software Defined Grid Energy Storage

Published in BuildSys'22, 2022

We describe a software system that provides software control of multiple, networked battery energy storage systems in the electric grid. The system introduces two new ideas that enable flexible and dependable management of energy storage. The first is a virtual battery, which can either partition a battery or aggregate multiple batteries. The second is a reservation-based API which allows asynchronous control of batteries to meet contractual guarantees in a safe and dependable manner.

Recommended citation: Sonia Martin, Nicholas Mosier, Obi Nnorom Jr., Yancheng Ou, Liana Patel, Oskar Triebe, Gustavo Cezar, Philip Levis, and Ram Rajagopal. Software defined grid energy storage. In The 9th ACM International Conference on Systems for Energy-Efficient Buildings, Cities, and Transportation (BuildSys ’22), November 9–10, 2022, Boston, MA, USA. ACM, New York, NY, USA, page 218-227. https://doi.org/10.1145/3563357.3564082

Axiomatic Hardware-Software Contracts for Security

Published in ISCA'22, 2022

We propose leakage containment models (LCMs)—novel axiomatic security contracts which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Our core contribution is an axiomatic vocabulary for formalizing LCMs, derived from the established axiomatic vocabulary for formalizing processor memory consistency models. Using this vocabulary, we formalize microarchitectural leakage—focusing on leakage through hardware memory systems—so that it can be automatically detected in programs and provide a taxonomy for classifying said leakage by severity. To illustrate the efficacy of LCMs, we first demonstrate that our leakage definition faithfully captures a sampling of (transient and non-transient) microarchitectural attacks from the literature. Second, we develop a static analysis tool based on LCMs which automatically identifies Spectre vulnerabilities in programs and scales to analyze real-world crypto-libraries.

Recommended citation: Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. Axiomatic hardware-software contracts for security. In Proceedings of the 49th Annual International Symposium on Computer Architecture, ISCA ’22, page 72–86, New York, NY, USA, 2022. Association for Computing Machinery. https://doi.org/10.1145/3470496.3527412

Bypassing ALSR via Speculative Buffer Overflows (Original Undergraduate Research Thesis)

Published in Middlebury College, Department of Computer Science, 2020

Spectre, a class of speculative execution vulnerabilities disclosed in 2018, has demonstrated weaknesses in existing security protections. Attackers can exploit speculative buffer overflows, a Spectre variant, to achieve arbitrary speculative code execution in victims. The security community has not thoroughly explored which security protections speculative buffer overflows can bypass. Previous literature assesses that address space layout randomization (ASLR), a security protection in modern operating systems, effectively mitigates speculative buffer overflow attacks. I present SpectreR2P, a host-based attack that discloses a victim’s ASLR-randomized code address via speculative buffer overflow, thereby demonstrating the ineffectiveness of ASLR against speculative buffer overflows.

Primality Testing and the AKS Algorithm (Undergraduate Literature Review Thesis)

Published in Middlebury College, Department of Mathematics, 2019

Integer factorization is an inherently difficult problem for which there is no known algorithm that produces an answer in polynomial time. Until recently, it was unknown whether the very similar but weaker problem of primality testing is equally difficult. Primality testing is the problem of determining whether an arbitrary positive integer n ∈N is prime or composite. In 2002, Agrawal, Kayal, and Saxena presented a provably correct deterministic primality test that terminates in polynomial time over all N. Although previous polynomial-time algorithms had been presented, they rely upon unproven claims such as the Riemann Hypothesis. We restrict our focus to algorithms that are unconditionally correct. In this paper, we review principles common to existing deterministic, polynomial-time primality tests, specifically Fermat’s Little Theorem (FlT) and the related topic of cyclotomic fields. We introduce a simple primality test based on FlT, and then discuss increasingly advanced algorithms (Pocklington primality test, APR primality test). In the second part of the paper, we prove the correctness of the AKS Primality Test, concluding that primality testing is a problem solvable in polynomial time.