---
id: 2046
title: "Vulnerability Modeling with Binary Ninja"
source_domain: blog.trailofbits.com
source_url: "https://blog.trailofbits.com/2018/04/04/vulnerability-modeling-with-binary-ninja/"
published_at: "2018-04-04T10:50:35Z"
tags: ["vulnerability-research", "binary-analysis", "openssl", "static-analysis", "binary-ninja", "symbolic-execution", "heartbleed", "theorem-proving"]
phying_url: "https://phying.com/item/2046"
lang: en
---

# Vulnerability Modeling with Binary Ninja

## Summary

Trail of Bits shows automated vulnerability discovery on stripped binaries, using Binary Ninja's MLIL and SSA forms with a theorem prover to model and rediscover the Heartbleed bug in OpenSSL.

## Intelligence Metadata

- **Sources:** blog.trailofbits.com
- **Published:** 2018-04-04T10:50:35Z
- **Original:** https://blog.trailofbits.com/2018/04/04/vulnerability-modeling-with-binary-ninja/
- **Phying News:** https://phying.com/item/2046