Inference of Robust Reachability Constraints
summary
Proposes an algorithm that uses theory-agnostic abduction to infer predicates on uncontrolled inputs that guarantee a property is robustly reachable, implemented as a prototype combining symbolic execution and robust symbolic execution over compiled binaries. Claims completeness relative to its inference language and ability to produce weakest constraints; uses robust reachability oracles to test candidates and several pruning strategies to speed search. Evaluated on verification and fault‑injection benchmarks: vanilla symbolic execution flags ~1,700 potential faults, robustly serious cases drop to 118, and some inferred constraints show >5% of inputs remain vulnerable. Artifacts available.
AI-written summary · about
chapters (16)
- 0:00Robust reachability constraints
- 1:55Traditional verification limits
- 3:02Bug replicability need
- 4:26Memory alignment robustness
- 5:28Defining constraints
- 6:32Contribution overview
- 7:55Constraint generation baseline
- 9:18Algorithm optimization
- 11:27Binary program evaluation
- 12:49Optimization impact
- 13:10Security with fault injection
- 14:36Conclusion and future
- 15:18Q&A: Quantifier elimination
- 16:42Q&A: Constraint sufficiency
- 17:47Q&A: Recursion limits
- 18:08Q&A: Symbolic execution optimization
related talks
16mQuantitative Robustness for Vulnerability Assessment
25mA Semantic Approach to Robust Property Preservation
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
58mAutomating Relational Verification of Infinite-State Programs
17mDynamic Robustness Verification against Weak Memory
22mComputational-Bounded Robust Compilation and Universally Composable Security
31mNecessity Specifications for Robustness