Formal Modeling of Transient Execution Attacks

The Spectre family of speculative execution attacks have required a rethinking of formal methods for security. The promise of formal methods is to provide guarantees of correctness and security in exchange for rigorous specifications and sound layering of abstractions. Unfortunately, the discovery of speculation-based vulnerabilities such as SPECTRE has shown that some of the most basic abstractions are broken at the microarchitectural level in today’s mainstream computing architectures. Modern processors execute code speculatively and may have to roll back state if a prediction turns out to be wrong; despite being rolled back, the transient execution can leave traces in the microarchitectural state that an attacker can abuse. By causing the processor to mispredict certain conditions, such as whether a branch is taken or not, an attacker can exfiltrate data despite system-level protection.

This project focuses on defining new types of semantics for speculative execution and related micro-architectural features, based on insights from formal methods for concurrency and weak memory models. We propose to specify speculative semantics using the CAT modeling language for memory consistency to specify execution models. We extend the Dartagnan Bounded Model Checker to directly process assembly code and interpret our new models. With this new framework, we validate attacks and defenses with respect to speculative semantics.

Software

• Kaibyo analysis tool, based on the Dartagnan Bounded Model Checker [ GitHub ]

Publications

@inproceedings{oakland22-cats-vs-spectre,
  author    = {Hern{\'{a}}n Ponce-de-Le{\'{o}}n and Johannes Kinder},
  title     = {Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks},
  booktitle = {Proc. IEEE Symp. Security and Privacy (S\&P)},
  pages     = {1415--1428},
  publisher = {IEEE},
  year      = {2022},
  doi       = {10.1109/SP46214.2022.00082},
}

@techreport{cats-vs-spectre-arxiv,
  author      = {Hern{\'{a}}n Ponce-de-Le{\'{o}}n and Johannes Kinder},
  title       = {Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks},
  institution = {arXiv},
  number      = {arXiv:2108.13818},
  year        = {2021},
  url         = {https://arxiv.org/abs/2108.13818},
}