Obtaining Information Leakage Bounds via Approximate Model Counting

Explore a 14-minute video presentation from the PLDI 2023 conference that introduces a sound symbolic quantitative information flow analysis for bounding information leakage in software systems. Learn about the challenges of using symbolic execution and model counting constraint solvers to quantify information leaks, and discover how this approach addresses unsoundness issues when program behavior is not fully explored or precise model counts are unavailable. Understand the implementation of this method as an extension to KLEE for computing sound bounds for information leakage in C programs. Gain insights into quantitative program analysis, symbolic quantitative information flow analysis, model counting, and information leakage optimization techniques presented by researchers from the University of California at Santa Barbara and Harvey Mudd College.