Publications

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