| 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.
|
|---|