BinSym: Binary-Level Symbolic Execution using Formal Descriptions of Instruction Semantics
<|reference_start|>BinSym: Binary-Level Symbolic Execution using Formal Descriptions of Instruction Semantics: 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, thereby reducing the margin for errors. Furthermore, BinSym's symbolic semantics can be directly related to the binary code, which improves symbolic execution speed by reducing solver query complexity.<|reference_end|>
@article{tempel2024binsym:,
    title={BinSym: Binary-Level Symbolic Execution using Formal Descriptions of
  Instruction Semantics},
    author={S"oren Tempel and Tobias Brandt and Christoph L"uth and Rolf
  Drechsler},
    journal={arXiv preprint arXiv:2404.04132},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.04132},
    primaryClass={cs.SE cs.CR cs.PL}
}