| Summary: | We present a new method for automatically synthesizing code-reuse attacks—for example, using Return Oriented Programming—based on mechanized formal logic. Our method reasons about machine code via abstraction to the p-code intermediate language of Ghidra, a well-established software reverse-engineering framework. This allows it to be applied to binaries of essentially any architecture, and provides certain technical advantages. We define a formal model of a fragment of p-code in propositional logic, enabling analysis by automated reasoning algorithms. We then synthesize code-reuse attacks by identifying selections of gadgets that can emulate a given p-code reference program. This enables our method to scale well, in both reference program and gadget library size, and facilitates integration with external tools. Our method matches or exceeds the success rate of state-of-the-art ROP chain synthesis methods while providing improved runtime performance.
<br> <br>
Our artifacts are composed of four main folders:
<br>
<ul>
<li>jingle: The implementation of our logical modeling of p-code. </li>
<li>crackers: The implementation of crackers, our algorithm for synthesizing code-reuse attacks.</li>
<li>crackers_evaluation: The code and data for our evaluation of crackers and the other ROP tools, as well as our ablation study. This contains our raw evaluation data, the tools used to produce our graphs and tables, and the code needed to re-run the entire evaluation.</li>
<li>dnsmasq_poc: A case study demonstrating the usage of crackers in the exploitation of a (simple) real-world vulnerability.</li>
</ul>
<br>
Subsequent development of the two software libraries in this artifact will occur here:
<br>
<ul>
<li>jingle: https://github.com/toolCHAINZ/jingle</li>
<li>crackers: https://github.com/toolCHAINZ/crackers</li>
</ul>
|
|---|