中文摘要：

符号执行能够对软件的路径分支信息进行收集和形式化表示，然后通过路径可达性推理得到软件行为同用户输入、网络输入等外部执行环境间的依赖关系．这些依赖关系已被广泛地应用到漏洞发掘、代码复用、协议分析等领域．该逆向分析技术也可被黑客用于软件破解、篡改和盗版等，对软件知识产权的保护带来了新的威胁．提出了一种新的基于路径模糊的软件保护方法以抵抗基于符号执行的逆向分析：利用条件异常代码替换条件跳转指令来隐藏程序的路径分支信息，使用不透明谓词技术引入伪造的路径分支来弥补程序在统计属性上的差异，并对路径模糊技术的强度、弹性和开销进行了分析．实验结果表明路径模糊技术能保护各类路径分支条件，有效减少路径分支信息的泄露，抵抗基于符号执行的逆向分析．

英文摘要：

Symbolic execution can collect branch conditions along a concrete execution trace of a program and build a logical formula describing the program execution path. Then the logical formula is used to reason about the dependence of control flow on user inputs, network inputs and other inputs from the execution environment, which can be used to effectively direct dynamic analysis to explore execution path space of the program. Symbolic execution has been widely used in vulnerability detection, code reuse, protocol analysis and so on. But it can be also used for malicious purposes, e. g., software cracking, software tampering and software piracy. The reverse engineering based on symbolic execution is a new threat to software protection. This paper proposes a novel binary code obfuscation scheme that obfuscates branch conditions to make it difficult for symbolic execution to collect branch conditions from the execution trace. It conceals branch information by substituting conditional jump instructions with conditional exception codes and uses exception handler to transfer control. It also introduces opaque predicates into the obfuscated program to impede statistical analysis. Furthermore, this paper provides insight into the potency, resilience and cost of the branch obfuscation. Experimental result shows that branch obfuscation is able to protect various branch conditions and reduces the leakage of branch information at run time that impedes reverse engineering based on symbolic execution to analyze program＇s internal logic.