Plenty of static analyzers can perform vulnerability discovery on source code, but what if you only have the binary? Dynamic tools can analyze binaries, but there are times when you can’t execute the code, a targeted area is difficult to reach, you just want initial targets for your bug hunting, and other situations where static tools would better suit your needs. How can we perform automated static analysis to check a binary for vulnerabilities in an architecture-agnostic manner? The short answer: combine Binary Ninja’s MLIL and SSA forms with a theorem prover like Z3. Together, these tools make it easy to build a mathematical model of incorrect behavior that can turn binaries, alchemy-like, into vulnerabilities.
In this talk, I present a case study for Heartbleed. First, I briefly highlight previous work for detecting the bug at the source level. Then, step by step, I walk through developing an architecture-agnostic Binary Ninja plugin that automatically identifies the bug class in OpenSSL. This walkthrough 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. Finally, I discuss the results of running the plugin on both vulnerable and patched versions of OpenSSL, compiled for multiple architectures. After this talk, attendees will have the tools necessary to build their own static analysis plugins for vulnerability discovery with Binary Ninja.
Presented at
Authored by
- Josh Watson