57 citations · 130 across the 15 of their papers we have counts for
6 papers · 1 filter
Analyzing and Exploiting Branch Mispredictions in Microcode
Nicholas Mosier, Hamed Nemati, John C. Mitchell +1
We present uSpectre, a new class of transient execution attacks that exploit microcode branch mispredictions to transiently leak sensitive data. We find that many long-known and re…
RTL2MPATH: Multi-PATH Synthesis with Applications to Hardware Security Verification
Yao Hsiao, Nikos Nikoleris, Artem Khyzha +4
The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called SPEC models. Despite…
Serberus: Protecting Cryptographic Code from Spectres at Compile-Time
Nicholas Mosier, Hamed Nemati, John C. Mitchell +1
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 primi…
Relational Models of Microarchitectures for Formal Security Analyses
Nicholas Mosier, Hanna Lachnitt, Hamed Nemati +1
There is a growing need for hardware-software contracts which precisely define the implications of microarchitecture on software security-i.e., security contracts. It is our view t…
Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption
Meghan Cowan, Deeksha Dangwal, Armin Alaghi +3
Homomorphic encryption (HE) is a privacy-preserving technique that enables computation directly on encrypted data. Despite its promise, HE has seen limited use due to performance o…
MeltdownPrime and SpectrePrime: Automatically-Synthesized Attacks Exploiting Invalidation-Based Coherence Protocols
Caroline Trippel, Daniel Lustig, Margaret Martonosi
The recent Meltdown and Spectre attacks highlight the importance of automated verification techniques for identifying hardware security vulnerabilities. We have developed a tool fo…