Sound Symbolic Execution via Abstract Interpretation and its Application to Sec...
summary
Combines symbolic execution with abstract interpretation to get sound proofs plus bounded counterexample pairs, claiming a formally proven analyzer called RedSoundRSE that is sound and “complete up to a bound.” Uses SMT-backed relational symbolic execution plus dependency-style abstract domains and faceted symbolic values to tighten loop over-approximations. Prototype implementation runs on a corpus of handcrafted simple-while benchmarks, produces actual refutation traces when precision flag holds, and empirically shows fewer false alarms than plain dependency analysis.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:17Motivation
- 0:51Roadmap of Semantics
- 3:45Verifying Noninterference
- 9:48Goals
- 10:33Symbolic execution and Noninterference
- 10:48Non-relational Symbolic Execution
- 12:47Relational symbolic execution (RSE)
- 15:45Dependences
- 17:34RedSoundRSE
- 20:27Theorems; Soundness and Refutation
- 23:06Conclusion
- 25:39Related work
- 28:00Results
related talks
28mForward Symbolic Execution for Trustworthy Automation of Binary Code Verification
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
18mSymbolic Execution Explained: Finding Bugs in Complex Code Paths
25mCertified Symbolic Finite Transducers: Formalization and Applications to String Analysis
29mSyntia: Synthesizing the Semantics of Obfuscated Code
20mSound Abstract Nonexploitability Analysis
31mSynthesizing Evidence of Emergent Computation