Formal framework for reasoning about the precision of dynamic analysis
summary
Provides a formal framework that models dynamic-analysis precision by treating trace properties as equivalence relations and defining obfuscation as transformations that split equivalence classes. Shows specific obfuscations that actually increase required traces: unknown opaque predicates (make semantically equivalent branches diverge per input), parametric data encodings, range dividers and gadget diversification that force multiple distinct execution paths. Proves soundness conditions by comparing coverage criteria as refinements of property partitions and outlines extending the model to hyperproperties and input probability measures.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:13Program Analysis
- 1:19Code Debugging/Verification
- 1:52Software Protection
- 3:19Code Obfuscation & Static Analysis
- 6:48Code Obfuscation & Dynamic Analysis
- 8:08Formalizing Dynamic Analysis
- 13:52Dynamic Data Obfuscation
- 14:35Dynamic CFG Obfuscation
- 16:56Coverage Criteria
- 18:33Open Issues
related talks
22mA Categorical Basis for Robust Program Analysis
52mThink Abstractly, Work Concretely
26mAn Effective Approach to Software Obfuscation
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
21mMechanised Hypersafety Proofs about Structured Data
24mRelational Symbolic Execution for Differential Privacy
23mSpecifying and Verifying Future Conditions
26mUnfolding Expressions for Gradual Verification