HeapHopper: Bringing Bounded Model Checking to Heap Implementation Security
summary
HeapHopper brings bounded model checking plus symbolic execution (uses angr) to concrete heap allocators, encoding up to a bounded number of transactions (e.g., six) as symbolic C tests and producing runnable proof-of-concept exploits. It finds real flaws in ptmalloc (compare 2.23 → 2.26), showing the new T-cache layer removes consistency checks and enables fake-free and arbitrary-write bypasses, reproduces a null‑byte/poison attack, and guides a patched defense that the tool verifies.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:33Poison NULL Byte Attack
- 4:02Motivation
- 4:39HeapHopper
- 5:21Heap Interaction Models
- 6:55Transactions
- 9:19Use-After-Free (UAF)
- 11:14Model Checking
- 12:13Identifying Security Violations
- 15:02Limitations
- 15:37Allocator Comparison
- 17:41Poison NULL Byte Allack
related talks
26mTowards Efficient Heap Overflow Discovery
32mPoking Holes in Information Hiding
37mHeap Layout Optimisation for Exploitation
15mTAILCHECK: A Lightweight Heap Overflow Detection Mechanism with Page Protection and...
01h 00mIntroduction to memory exploitation
08mChatGPT, Make a Secure Malloc for me
12mMemory-Safety Verification of Open Programs With Angelic Assumptions
14mCollapsing Towers for Side-Channel Security