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.

翻译：BinSym 是一个用于二进制形式软件符号化程序分析的框架。与先前工作不同，它直接操作于二进制代码指令，无需将其提升为中间表示（IR）。这一目标通过将符号语义构建于二进制代码指令语义的形式化描述之上来实现。通过基于现有形式化描述，BinSym 消除了先前工作中为实现向 IR 转换所需的手动工作量，从而降低了错误概率。此外，BinSym 的符号语义可直接关联至二进制代码，通过降低求解器查询复杂度来提升符号执行速度。