Data-Driven Synthesis of Provably Sound Side Channel Analyses

TL;DR

This paper introduces a fully automated, data-driven static analysis method for detecting side-channel leaks in cryptographic software, which is both provably sound and significantly faster than existing manual analyzers.

Contribution

It presents a novel learning-based approach that synthesizes sound static analyzers using syntax-guided synthesis and decision tree learning, with formal soundness guarantees.

Findings

Achieves empirical accuracy comparable to state-of-the-art analyzers.

Runs 300X to 900X faster than manual analyzers.

Successfully detects power side channels in C programs.

Abstract

We propose a data-driven method for synthesizing a static analyzer to detect side-channel information leaks in cryptographic software. Compared to the conventional way of manually crafting such a static analyzer, which can be labor intensive, error prone and suboptimal, our learning-based technique is not only automated but also provably sound. Our analyzer consists of a set of type-inference rules learned from the training data, i.e., example code snippets annotated with ground truth. Internally, we use syntax-guided synthesis (SyGuS) to generate new features and decision tree learning (DTL) to generate type-inference rules based on these features. We guarantee soundness by formally proving each learned rule via a technique called Datalog query containment checking. We have implemented our technique in the LLVM compiler and used it to detect power side channels in C programs. Our results show that, in addition to being automated and provably sound during synthesis, the learned analyzer also has the same empirical accuracy as two state-of-the-art, manually crafted analyzers while being 300X and 900X faster, respectively.