Automated Template-free Synthesis of Instruction-Centric Leakage Contracts for Black-Box CPUs
Cryptography and Security
Summary
The authors address the problem of side-channel attacks, where tiny differences in how CPUs work can reveal secret information. They focus on creating 'leakage contracts,' which describe these leaks at the instruction level to help secure CPU programming. Because current CPUs are complex, making these contracts by hand is very hard, so the authors developed a tool called malcos that automatically finds these leakage patterns without needing to know the CPU's internal design. They tested malcos on popular CPU types like x86 and ARM and found their contracts are accurate and reliable for the leaks they detected. This work shows it's possible to automatically understand CPU leakage even when the CPU design is unknown.
Authors
Elvira Moreno, Tiziano Marinaro, Ryan Williams, Marco Patrignani, Roberto Guanciale, Hamed Nemati, Marco Guarnieri
Abstract
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 and thus modern CPUs lack dedicated leakage contracts. We present a methodology to extract instruction-centric leakage contracts for major CPU architectures with minimal manual intervention. We implemented this technique in malcos, the first template-free tool that 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 precise and sound with respect to all leaks observed during synthesis. Our results demonstrate that learning leakage contracts from black-box CPUs is feasible.