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.

Fast location of similar code fragments using semantic 'juice'

DALLA PREDA, Mila;GIACOBAZZI, Roberto
2013

Abstract

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.
9781450318570
metmorphic malware; binary analysis
File in questo prodotto:
File Dimensione Formato  
2013-PPREW-Lakhotia - FINAL.pdf

accesso aperto

Tipologia: Documento in Post-print
Licenza: Accesso ristretto
Dimensione 130.43 kB
Formato Adobe PDF
130.43 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/620352
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 66
  • ???jsp.display-item.citation.isi??? ND
social impact