Synthesis of machine code from semantics
Synthesis of machine code from semantics
复制标题
从语义合成机器代码
DOI：
10.1145/2737924.2737960
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
T. Reps
中科院分区：
文献类型：
--
作者：
Venkatesh Srinivasan;T. Reps
在本文中，我们提出了一种从语义规范合成机器代码指令的技术，该规范以无量词位向量（QFBV）逻辑公式的形式给出。我们的技术使用反例引导归纳综合（CEGIS）框架的实例化，结合搜索空间修剪启发式来合成指令序列。为了克服枚举综合中固有的指数成本，我们的技术使用分而治之的策略将输入QFBV公式分解为独立的子公式，并为子公式合成指令。通过我们的技术创建的合成器可以用来创建基于语义的二进制重写工具，如优化器、部分求值器、程序混淆器/去混淆器等。我们对Intel的IA-32指令集进行的实验表明，与我们的基线算法相比，我们的搜索空间剪枝启发式算法将合成时间减少了473倍，而我们的分治策略将合成时间进一步减少了3到5个数量级。
In this paper, we present a technique to synthesize machine-code instructions from a semantic specification, given as a Quantifier-Free Bit-Vector (QFBV) logic formula. Our technique uses an instantiation of the Counter-Example Guided Inductive Synthesis (CEGIS) framework, in combination with search-space pruning heuristics to synthesize instruction-sequences. To counter the exponential cost inherent in enumerative synthesis, our technique uses a divide-and-conquer strategy to break the input QFBV formula into independent sub-formulas, and synthesize instructions for the sub-formulas. Synthesizers created by our technique could be used to create semantics-based binary rewriting tools such as optimizers, partial evaluators, program obfuscators/de-obfuscators, etc. Our experiments for Intel's IA-32 instruction set show that, in comparison to our baseline algorithm, our search-space pruning heuristics reduce the synthesis time by a factor of 473, and our divide-and-conquer strategy reduces the synthesis time by a further 3 to 5 orders of magnitude.