BinSym: Binary-Level Symbolic Execution using Formal Descriptions of Instruction Semantics

arXiv:2404.04132v1 Announce Type: cross
Abstract: BinSym is a framework for symbolic program analysis of software in binary form. Contrary to prior work, it operates directly on binary code instructions and does not require lifting them to an intermediate representation (IR). This is achieved by formulating the symbolic semantics on top of a formal description of binary code instruction semantics. By building on existing formal descriptions, BinSym eliminates the manual effort required by prior work to implement transformations to an IR, …

analysis arxiv binary code cs.cr cs.pl cs.se descriptions framework instructions intermediate program program analysis representation software symbolic execution work