一句话：提出数据驱动方法自动合成可证可靠的侧信道静态分析器，并用查询包含检查保证规则可靠性。
本文研究如何自动合成用于检测密码软件侧信道信息泄漏的静态分析器，避免手工构建分析器繁琐、易错且次优的问题。方法以带真值标注的代码片段作为训练数据，学习一组类型推断规则：内部使用语法引导合成（SyGuS）生成新的递归特征，再用决策树学习基于这些特征生成分析规则。为保证可靠性，作者通过查询包含检查证明每条学习到的分析规则。该技术已在 LLVM 编译器中实现，用于检测实现密码协议的 C 程序中的功耗侧信道。实验表明，该分析器在合成过程中既可自动又具有可证可靠性，同时达到两个最先进手工分析器的经验精度，并分别快 300 倍和 900 倍。
We propose a data-driven method for synthesizing static analyses to detect side-channel information leaks in cryptographic software. Compared to the conventional way of manually crafting such static analyzers, which can be tedious, 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 the ground truth. Internally, we use syntax-guided synthesis (SyGuS) to generate new recursive features and decision tree learning (DTL) to generate analysis rules based on these features. We guarantee soundness by proving each learned analysis rule via a technique called query containment checking. We have implemented our technique in the LLVM compiler and used it to detect power side channels in C programs that implement cryptographic protocols. Our results show that, in addition to being automated and provably sound during synthesis, our analyzer can achieve the same empirical accuracy as two state-of-the-art, manually-crafted analyzers while being 300X and 900X faster, respectively.