Synthesizing Evidence of Emergent Computation
summary
Tool called seek synthesizes counterexamples to secure compilation from executable language models and uses Rosette symbolic execution to produce concrete program+context pairs. It finds three evidence levels: changed behaviors, truly emergent computations, and composable gadgets; e.g., a buggy set implementation yields an add-one gadget that disappears after a fix. Case studies include printf-oriented gadgets, data-oriented-auth bypasses, and allocator attacks where an address-forcing gadget takes over an hour to synthesize but composes from fast subgadgets.
AI-written summary · about
chapters (22)
- 0:00Introduction
- 0:47Motivations
- 2:05Secure Compilation
- 3:52Seek
- 4:37Workflow
- 5:47Levels of Evidence
- 6:41Abstract vs Concrete
- 8:10Interpreters
- 10:21First level of evidence
- 11:26Second level of evidence
- 12:26Revisiting our implementation
- 13:20Program synthesis
- 14:52Gadget synthesis
- 16:18Case study 1
- 16:28Case study 2
- 17:55Case study 3
- 18:31TinyC TinyA
- 19:28Small Program
- 22:44High Level Lessons
- 23:06Scalability
- 24:12Questions
- 25:50Building a model
related talks
51mSynthesis and Verification for All
29mSyntia: Synthesizing the Semantics of Obfuscated Code
31mLetting users do the undecidable: lessons from program synthesis
42mEvidence-Oriented Programming
26mProgram Synthesis Using Example Propagation
39mAsk Me Anything with Alex Aiken
22mCounterexample-Guided Inference of Modular Specifications
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...