Exploits as Insecure Compilation
summary
Defines an exploit as a target context that makes the compiled program exhibit a behavior impossible in the source and proves this is equivalent to violating a property that all source contexts preserve, using hyperproperty/trace reasoning. Works through ROP and Spectre-style examples, shows when exploits are trace vs hyperproperty-level, and gives a composability theorem: an exploit found between intermediate and target lifts to the whole compiler under invertibility conditions. Offers a broader compiler model and directions for automated exploit-finding and mitigation.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:49What is a secure compiler
- 2:38State machine vs implementation
- 4:32Goal
- 4:52Proposed Definition
- 6:00Proposed Framework
- 9:15Robust Primary Preservation
- 11:30Exploits
- 13:09Trace Exploit
- 16:24Conclusion
- 18:23Next Steps
related talks
51mThe Anatomy of an Exploit
20mSound Abstract Nonexploitability Analysis
57mThe Anatomy of an Exploit
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
14mNon-interference Preserving Optimising Compilation
40mTransitive Vulnerabilities Exploit In Real-life
16mMitigating Transient-Execution Attacks with CHERI Compartments