Abstract
Side channels are security vulnerabilities that may be exploited to extract sensitive information using the (often statistical) dependencies between secret data and non-functional properties of a software program, such as the execution time, power consumption, and electromagnetic radiation of the underlying computing device. In this work, we develop a data-driven method for synthesizing a static analyzer for detecting power side-channel leaks (or proving their absence). Compared to the conventional way of manually crafting such a static analyzer, which can be labor intensive, error prone, and suboptimal, our method is not only automated but also provably sound. The analyzer consists of a set of analysis rules learned from the training data, i.e., example code snippets annotated with the ground truth. Internally, we use syntax-guided synthesis (SyGuS) to generate new features and decision tree learning (DTL) to generate analysis rules based on these features. We guarantee soundness by formally proving each learned analysis rule via a technique called Datalog query containment checking. We have implemented our technique and evaluated it on a set of C programs that implements well-known cryptographic algorithms. The 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 orders-of-magnitude faster.