Towards static analyses and abstract domains for hyperproperties
summary
Outlines concrete static-analysis routes for hyperproperties: noninterference is two-safety / K-safety with counterexamples of K executions, reduced to safety by self-composition multiplies program size by K which makes analyses costly; lightweight taint analysis uses a taint-augmented semantics; a more precise route uses hypercollecting semantics (sets of sets) and relational domains via self-composition or symbolic execution; separate abstract domains and a reduced product handle continuity/smoothness properties and value dependencies.
AI-written summary · about
chapters (15)
- 0:00Hyperproperties and static analysis
- 22:23Interval analysis to trace properties
- 23:45Non-interference and two-safety
- 26:00K-safety and decomposition
- 27:45Hyperliveness versus hyper-safety
- 30:53Static analysis methods
- 31:59Taint analysis for flow tracking
- 38:18Taint analysis limitations
- 40:44Self-composition for two-safety
- 43:34Abstract interpretation with self-composition
- 46:26Conditionals in self-composition
- 47:54Symbolic execution for precision
- 49:21Cost of static analysis
- 49:44Functional analysis for hyperliveness
- 54:04Abstract semantics for continuity
related talks
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
14mNon-interference Preserving Optimising Compilation
15mProducts of Recursive Programs for Hypersafety Verification
25mA Semantic Approach to Robust Property Preservation
25mComposing Secure Compilers
15mStable Relations and Abstract Interpretation of Higher-Order Programs
22mA Categorical Basis for Robust Program Analysis