Heap Models for Exploit Systems

Explore heap models for exploit systems in this IEEE conference talk presented at the 2015 LangSec Workshop. Delve into formal deductive reasoning for programs with dynamic memory allocations and the development of exploits to demonstrate the absence of safety invariants. Learn about the formalization of exploits as abstract machines called "exploit systems" and how specific heap configurations are crucial for successful attacks. Discover constructions that reconcile physical and logical heap properties, and understand how exploits can be expressed as a reachability problem. Examine various heap vulnerabilities, including invalid free, use after free, and Heartbleed. Gain insights into harness testing, heap locators, heap transitions, heap primitives, and fitness algorithms. This 48-minute presentation by Julien Vanegue offers a comprehensive look at the intersection of formal verification, security vulnerabilities, and exploit development in the context of heap models.

Intro
The Grand Challenge
Why is this important
Heap vulnerabilities
Invalid free
Use after free
Heartbleed
Harness Test
Heap Locator
Heap Transition
Heap Primitives
Fitness Algorithm
Summary