Yuheng Yang

PhD student at MIT advised by Mengjia Yan
Email: yuhengy@mit.edu

Bio

I am a PhD student at MIT EECS advised by Prof. Mengjia Yan. I work on using formal methods to design secure hardware, with a focus on mitigating timing side channels and speculative execution attacks. Recently, I have been studying microarchitecture modeling approaches and developing Pensieve (Code), a security-oriented microarchitecture model to assist early-stage security evaluation with model checking. Before starting PhD, I received a BEng degree from the University of Chinese Academy of Sciences with RISC-V core tape-out experience advised by Prof. Yungang Bao.

Research Insterests

Hardware Security, Computer Architecture, Formal Method

Publications & Presentations

• RTL Verification for Secure Speculation Using Contract Shadow Logic, ASPLOS 2025.
  Qinhan Tan*, Yuheng Yang*, Thomas Bourgeat, Sharad Malik, Mengjia Yan
  Abstract: Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from unknown vulnerabilities. Thus, a formal and rigorous evaluation of the ability of hardware designs to deal with speculative execution attacks is urgently desired.
  This paper proposes a formal verification technique called Contract Shadow Logic that can effectively improve RTL verification scalability while being applicable to different defense mechanisms. In this technique, we leverage computer architecture design insights to... improve verification performance for checking security properties formulated as software-hardware contracts for secure speculation. Our verification scheme is accessible to computer architects without requiring formal-method expertise.
  We evaluate our technique on multiple RTL designs, including three out-of-order processors. The experimental results demonstrate that our technique exhibits a significant advantage in finding attacks on insecure designs and deriving unbounded proofs on secure designs, when compared to the baseline and two state-of-the-art verification schemes, LEAVE and UPEC. Read more
• Pensieve: Microarchitectural Modeling for Security Evaluation, ISCA 2023. Code
  Yuheng Yang, Thomas Bourgeat, Stella Lau, Mengjia Yan
  ISCA Lightning,  ISCA,  Intel RARE Workshop,  FCCM Workshop,  NEHWS Workshop (Best Poster Award),  Poster
  Abstract: Traditional modeling approaches in computer architecture aim to obtain an accurate estimation of performance, area, and energy of a processor design. With the advent of speculative execution attacks and their security concerns, these traditional modeling techniques fall short when used for security evaluation of defenses against these attacks.
  This paper presents Pensieve, a security evaluation framework targeting early-stage microarchitectural defenses against speculative execution attacks. At the core, it introduces a modeling discipline for... systematically studying early-stage defenses. This discipline allows us to cover a space of designs that are functionally equivalent while precisely capturing timing variations due to resource contention and microarchitectural optimizations. We implement a model checking framework to automatically find vulnerabilities in designs. We use Pensieve to evaluate a series of state-of-the-art invisible speculation defense schemes, including Delay-on-Miss, InvisiSpec, and GhostMinion, against a formally defined security property, speculative non-interference. Pensieve finds Spectre-like attacks in all those defenses, including a new speculative interference attack variant that breaks GhostMinion, one of the latest defenses. Read more
• DAGguise: Mitigating Memory Timing Side Channels, ASPLOS 2022.
  Peter W. Deutsch*, Yuheng Yang*, Thomas Bourgeat, Jules Drean, Joel Emer, Mengjia Yan
  ASPLOS,  ASPLOS,  Poster
• CaSA: End-to-end Quantitative Security Analysis of Randomly Mapped Caches, MICRO 2020.
  Thomas Bourgeat*, Jules Drean*, Yuheng Yang, Lillian Tsai, Joel Emer, Mengjia Yan
  ICCAD Workshop (Top Picks Honorable Mention)
• CaSA: End-to-end Quantitative Security Analysis of Randomly Mapped Caches (Top Picks Version), IEEE Design & Test 2024.
  Thomas Bourgeat*, Jules Drean*, Yuheng Yang, Lillian Tsai, Joel Emer, Mengjia Yan
• SoK: Understanding Design Choices and Pitfalls of Trusted Execution Environments, AsiaCCS 2024.
  Mengyuan Li, Yuheng Yang, Guoxing Chen, Mengjia Yan, Yinqian Zhang