Fast location of similar code fragments using semantic 'juice'

Abstraction of semantics of blocks of a binary is termed as ‘juice.’Whereas the denotational semantics summarizes the computationperformed by a block, its juice presents a template of the relationshipsestablished by the block. BinJuice is a tool for extracting the‘juice’ of a binary. It symbolically interprets individual blocks ofa binary to extract their semantics: the effect of the block on theprogram state. The semantics is generalized to juice by replacingregister names and literal constants by typed, logical variables. Thejuice also maintains algebraic constraints between the numeric variables.Thus, this juice forms a semantic template that is expected tobe identical regardless of code variations due to register renaming,memory address allocation, and constant replacement. The termsin juice can be canonically ordered using a linear order presented.Thus semantically equivalent (rather, similar) code fragments canbe identified by simple structural comparison of their juice, or bycomparing their hashes. While BinJuice cannot find all equivalentconstructs, for that would solve the Halting Problem, it does significantlyimprove the state-of-the-art in both the computational complexityas well as the set of equivalences it can establish. Preliminaryresults show that juice is effective in pairing code variantscreated by post-compile obfuscating transformations.