Talk: Automated Synthesis of Instruction-Centric Leakage Contracts

Side-channel attacks pose a significant security threat for modern computing platforms, because they exploit subtle discrepancies in CPU behaviors to leak sensitive information. To model the information leaked by a CPU via microarchitectural side-channels, recent work proposed leakage contracts: an ISA-level security abstraction that provides the foundations for secure CPU programming. Unfortunately, due to the complexity of current microarchitectures, devising a leakage contract for a CPU requires extensive manual effort. We present a methodology to extract sound and precise instruction-centric leakage contracts for major CPU architectures with minimal manual intervention. We implemented this technique in malcos, which automates the synthesis of leakage contracts for black-box CPUs. We evaluate malcos on x86 and ARM CPUs, and show that the contracts it synthesizes are sound and precise. Our results demonstrate that learning leakage contracts from black-box CPUs is feasible.