  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.
