SPECTECTOR - Principled Detection of Speculative Information Flows

Explore a principled approach to detecting speculative information flows in this IEEE conference talk. Dive into the concept of speculative non-interference, the first semantic notion of security against speculative execution attacks. Learn about SPECTECTOR, an algorithm based on symbolic execution that automatically proves speculative non-interference or detects violations. Discover how this tool has been used to identify subtle leaks and optimization opportunities in major compilers' SPECTRE countermeasures. Gain insights into speculative execution, branch prediction, Spectre V1, and methods for capturing leakage. Examine the scalability of checking speculative non-interference and its relationship to symbolic execution. Cover topics including memory leaks, the implementation of Spectector, and the results of its application.

Intro
Speculative execution + branch prediction
Spectre V1
How to capture leakage?
Speculative non-interference
Detecting speculative leaks
Symbolic execution
Memory leaks
Spectector
Results