Vulnerability Modeling with Binary Ninja

用二进制忍者进行漏洞建模。这是关于Binary Ninja Intermediate Language（BNIL）系列的一系列帖子的第3部分。你可以阅读

第1部分 https://blog.trailofbits.com/2017/01/31/breaking-down-binary-ninjas-low-level-il/

第2部分 https://blog.trailofbits.com/2017/02/13/devirtualizing-c-with-binary-ninja/

在我之前的文章中，我演示了如何利用低级IL（LLIL）编写一个可以虚拟化C ++虚函数的体系结构无关插件。自那时以来，Binary Ninja增加了许多新的和令人兴奋的功能; 特别是中等水平IL（MLIL）和单静态指配（SSA）[1]。在这篇文章中，我将讨论这两个方面，并展示它们的一个有趣用处：自动化漏洞发现。

大量的静态分析器可以在源代码上执行漏洞发现，但是如果只有二进制文件呢？我们如何建模一个漏洞，然后检查二进制文件以查看它是否存在漏洞？简短的回答：使用Binary Ninja的MLIL和SSA表单。总而言之，它们可以很容易地用一个定理证明器来构建和求解一个方程组，这个方法证明器将二进制文件转化为一个类似炼金术的漏洞！

作者使用它自己的工具，重新发现一次 Heartbleed 漏洞～