Obtaining Information Leakage Bounds via Approximate Model Counting
Information leaks are a significant problem in modern software systems. In recent years, information theoretic concepts, such as Shannon entropy, have been applied to quantifying information leaks in programs. One recent approach is to use symbolic execution together with model counting constraints solvers in order to quantify information leakage. There are at least two reasons for unsoundness in quantifying information leakage using this approach: 1) Symbolic execution may not be able to explore all execution paths, 2) Model counting constraints solvers may not be able to provide an exact count. We present a sound symbolic quantitative information flow analysis that bounds the information leakage both for the cases where the program behavior is not fully explored and the model counting constraint solver is unable to provide a precise model count but provides an upper and a lower bound. We implemented our approach as an extension to KLEE for computing sound bounds for information leakage in C programs.
Tue 20 JunDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 11:00 | |||
09:00 20mTalk | Obtaining Information Leakage Bounds via Approximate Model Counting PLDI Research Papers Seemanta Saha University of California Santa Barbara, Surendra Ghentiyala University of California Santa Barbara, Shihua Lu University of California Santa Barbara, Lucas Bang Harvey Mudd College, Tevfik Bultan University of California at Santa Barbara DOI | ||
09:20 20mTalk | CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity PLDI Research Papers DOI | ||
09:40 20mTalk | Discrete Adversarial Attack to Models of Code PLDI Research Papers Fengjuan Gao Nanjing University of Science and Technology, Yu Wang Nanjing University, Ke Wang Visa Research DOI | ||
10:00 20mTalk | Generalized Policy-Based Noninterference for Efficient Confidentiality-Preservation PLDI Research Papers Shamiek Mangipudi Università della Svizzera italiana (USI), Pavel Chuprikov USI Lugano, Patrick Eugster USI Lugano; Purdue University, Malte Viering TU Darmstadt, Savvas Savvides Purdue University DOI | ||
10:20 20mTalk | Taype: A Policy-Agnostic Language for Oblivious Computation PLDI Research Papers DOI | ||
10:40 20mTalk | Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs PLDI Research Papers Shankara Pailoor University of Texas at Austin, Yanju Chen University of California at Santa Barbara, Franklyn Wang Harvard University, 0xparc, Clara Rodríguez-Núñez Complutense University of Madrid, Jacob Van Geffen Veridise Inc., Jason Morton ZKonduit, Michael Chu 0xparc, Brian Gu 0xparc, Yu Feng University of California at Santa Barbara, Işıl Dillig University of Texas at Austin DOI | ||
