Obtaining Information Leakage Bounds via Approximate Model Counting
summary
Provides a method that produces sound upper and lower bounds on Shannon entropy when symbolic execution fails to explore all paths or model counters return ranges instead of exact counts. It reduces leakage bounding to constrained optimization (hill-climb for the concave max, extremal search for the min), proves complexity bounds (practical algorithms achieve roughly O(n log n) for upper, O(n^2) for lower), implements the approach as a KLEE extension for C, and reports probabilistically sound results that are tighter than channel-capacity baselines.
AI-written summary · about
chapters (9)
- 0:00Information leakage bounds
- 1:25Leakage estimation limits
- 2:06Symbolic execution example
- 4:57Where symbolic execution fails
- 6:46Bounding leakage entropy
- 8:36Optimization algorithms
- 10:02Experimental validation
- 10:24Conclusion and future work
- 10:45Q&A
related talks
12mLeakage models are a leaky abstraction (...)
32mBlack box side-channel leakage verification using statistical approach
48mFormal Modelling of Information-flow Control Systems: Some Lessons Learned
01h 08mTutorial: Security
15mInterpretable Noninterference Measurement and its Application to Processor Designs
32mPoking Holes in Information Hiding
13mExposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
20mPantomime: Constructive Leakage Proofs via Simulation