Data-Driven Synthesis of a Provably Sound Side Channel AnalysisTechnical Track
Wed 26 May 2021 05:15 - 05:35 at Blended Sessions Room 3 - 1.4.3. Identifying Information Leaks
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.
Tue 25 MayDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:40 - 17:35 | 1.4.3. Identifying Information LeaksNIER - New Ideas and Emerging Results / Technical Track at Blended Sessions Room 3 +12h Chair(s): Oscar Dieste Universidad Politécnica de Madrid | ||
16:40 15mPaper | An Axiomatic Approach to Detect Information Leaks in Concurrent ProgramsNIER NIER - New Ideas and Emerging Results Sandip Ghosal Indian Institute of Technology, Bombay, R.K. Shyamasundar Indian Institute of Technology, Bombay Pre-print Media Attached | ||
16:55 20mPaper | Abacus: Precise Side-Channel AnalysisTechnical Track Technical Track Qinkun Bao The Pennsylvania State University, Zihao Wang The Pennsylvania State University, Xiaoting Li Penn State University, James Larus EPFL, Dinghao Wu The Pennsylvania State University Pre-print Media Attached | ||
17:15 20mPaper | Data-Driven Synthesis of a Provably Sound Side Channel AnalysisTechnical Track Technical Track Jingbo Wang University of Southern California, Chungha Sung University of Southern California, Mukund Raghothaman University of Southern California, Chao Wang USC Pre-print Media Attached |
Wed 26 MayDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
04:40 - 05:35 | 1.4.3. Identifying Information LeaksTechnical Track / NIER - New Ideas and Emerging Results at Blended Sessions Room 3 | ||
04:40 15mPaper | An Axiomatic Approach to Detect Information Leaks in Concurrent ProgramsNIER NIER - New Ideas and Emerging Results Sandip Ghosal Indian Institute of Technology, Bombay, R.K. Shyamasundar Indian Institute of Technology, Bombay Pre-print Media Attached | ||
04:55 20mPaper | Abacus: Precise Side-Channel AnalysisTechnical Track Technical Track Qinkun Bao The Pennsylvania State University, Zihao Wang The Pennsylvania State University, Xiaoting Li Penn State University, James Larus EPFL, Dinghao Wu The Pennsylvania State University Pre-print Media Attached | ||
05:15 20mPaper | Data-Driven Synthesis of a Provably Sound Side Channel AnalysisTechnical Track Technical Track Jingbo Wang University of Southern California, Chungha Sung University of Southern California, Mukund Raghothaman University of Southern California, Chao Wang USC Pre-print Media Attached |