Verification of Programs with Concealed Components
summary
Usher synthesizes inductive invariants for programs with concealed components (inline assembly, third‑party APIs, sampling) by running a learner-teacher loop that turns a candidate invariant and spec into a nondeterministic program and uses fuzzing + symbolic execution to hunt counterexamples. Evaluated on 15 real-world examples (one calls a CNN) and a 113-benchmark suite, the pipeline automatically validates or rejects candidates and succeeds on 102 of 113 benchmarks; randomized cases encode distributions with probabilistic symbolic variables (Monty Hall) to bound probabilities.
AI-written summary · about
chapters (6)
- 0:00Concealed components intro
- 2:00Almost verification with unknowns
- 7:59Almost verification with stochastic
- 12:01Future directions
- 22:05Practical benefits
- 26:18Q&A
related talks
14mCollapsing Towers for Side-Channel Security
12mMemory-Safety Verification of Open Programs With Angelic Assumptions
58mAutomating Relational Verification of Infinite-State Programs
29mSyntia: Synthesizing the Semantics of Obfuscated Code
52mStructure aware fuzzing
16mTooling Design and Lessons Learned from Systematic Evaluations of the Preservation of(…)
01h 15mMake your programs more reliable with Fuzzing
31mSynthesizing Evidence of Emergent Computation