Vulnerability Modeling with Binary Ninja

title	Vulnerability Modeling with Binary Ninja
date	2018
authors	Josh Watson
conference	Pacific Hackers 2018
resources	label path Slides Vulnerability Modeling with Binary Ninja.pdf label url Blog Post https://blog.trailofbits.com/2018/04/04/vulnerability-modeling-with-binary-ninja/

Plenty of static analyzers can perform vulnerability discovery on source code, but what if you only have the binary? This talk presents a case study for Heartbleed, walking step by step through developing an architecture-agnostic Binary Ninja plugin that automatically identifies the bug class in OpenSSL. It explains how to combine Binary Ninja's powerful intermediate languages and SSA form with the Z3 theorem prover to build a mathematical model of the vulnerability, and discusses results across multiple architectures.