57 citations · 130 across the 15 of their papers we have counts for
17 papers
VeriCoder: Enhancing LLM-Based RTL Code Generation through Functional Correctness Validation
Anjiang Wei, Huanmi Tan, Tarun Suresh +5
Recent advances in Large Language Models (LLMs) have sparked growing interest in applying them to Electronic Design Automation (EDA) tasks, particularly Register Transfer Level (RT…
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…
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
Matthias Cosler, Christopher Hahn, Daniel Mendoza +2
A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as wri…
Dynamic Network Adaptation at Inference
Daniel Mendoza, Caroline Trippel
Machine learning (ML) inference is a real-time workload that must comply with strict Service Level Objectives (SLOs), including latency and accuracy targets. Unfortunately, ensurin…
RecShard: Statistical Feature-Based Memory Optimization for Industry-Scale Neural Recommendation
Geet Sethi, Bilge Acun, Niket Agarwal +3
We propose RecShard, a fine-grained embedding table (EMB) partitioning and placement technique for deep learning recommendation models (DLRMs). RecShard is designed based on two ke…
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…
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni +12
Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique wh…
Analysis and Mitigations of Reverse Engineering Attacks on Local Feature Descriptors
Deeksha Dangwal, Vincent T. Lee, Hyo Jin Kim +9
As autonomous driving and augmented reality evolve, a practical concern is data privacy. In particular, these applications rely on localization based on user images. The widely ado…
RecSSD: Near Data Processing for Solid State Drive Based Recommendation Inference
Mark Wilkening, Udit Gupta, Samuel Hsia +4
Neural personalized recommendation models are used across a wide variety of datacenter applications including search, social media, and entertainment. State-of-the-art models compr…
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…
CPR: Understanding and Improving Failure Tolerant Training for Deep Learning Recommendation with Partial Recovery
Kiwan Maeng, Shivam Bharuka, Isabel Gao +8
The paper proposes and optimizes a partial recovery training system, CPR, for recommendation models. CPR relaxes the consistency requirement by enabling non-failed nodes to proceed…
TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests
Naorin Hossain, Caroline Trippel, Margaret Martonosi
Memory consistency models (MCMs) specify the legal ordering and visibility of shared memory accesses in a parallel program. Traditionally, instruction set architecture (ISA) MCMs a…
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…
Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings
Yatin A. Manerkar, Caroline Trippel, Daniel Lustig +2
The C and C++ high-level languages provide programmers with atomic operations for writing high-performance concurrent code. At the assembly language level, C and C++ atomics get ma…
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
Caroline Trippel, Yatin A. Manerkar, Daniel Lustig +2
Memory consistency models (MCMs) which govern inter-module interactions in a shared memory system, are a significant, yet often under-appreciated, aspect of system design. MCMs are…