Bi-abductive adversarial program synthesis
summary
Claims a practical pipeline that uses bi-abduction + deductive synthesis to automatically produce adversary programs that exploit real bugs, demonstrates a prototype that synthesizes concrete exploits (e.g., an out‑of‑bounds index that leaks a secret) using Castle concurrent adversarial separation logic to model pointers and concurrency, and shows the key reduction that reduces concurrent synthesis to sequential so existing sequential synthesizers can be reused; prototype works on small examples, while full parallel synthesis rules remain work in progress.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:22Research context
- 1:52Incorrectness logic in security
- 3:17Bug prioritization questions
- 4:19Adversary logic limits
- 8:09Castle concurrent logic
- 9:53Exploit synthesis
- 10:37Bi-abduction for synthesis
- 13:09Synthesizing adversarial conditions
- 15:18Adversarial program synthesis
- 16:44Deductive synthesis foundations
- 18:10Parallel program synthesis
- 19:55Concurrent synthesis rules
- 20:17Acknowledgments
- 20:38Q&A
related talks
29mSyntia: Synthesizing the Semantics of Obfuscated Code
31mSynthesizing Evidence of Emergent Computation
26mVerification of Programs with Concealed Components
17mAutomated Policy Synthesis for System Call Sandboxing
25mBehavioral simulation for smart contracts
35mBreaking Boundaries with Adversarial Testing
45mWinning by deception: tactics, techniques, and procedures of adversarial A.I.
19mInference of Robust Reachability Constraints