论文标题
SYDR:尖端动态符号执行
Sydr: Cutting Edge Dynamic Symbolic Execution
论文作者
论文摘要
安全开发生命周期(SDL)已成为行业标准。动态符号执行(DSE)具有大量计算机安全性应用程序(模糊,漏洞发现,反向工程等)。我们为动态符号执行提出了几种性能和准确性改进。跳过非符号指令允许构建一个路径谓词1.2--3.5倍。符号引擎在符号执行过程中简化了公式。路径谓词切片消除了从求解器查询中的无关连接。我们将每个跳跃表(Switch语句)作为多个分支处理,并描述多线程程序的象征性执行方法。提出的解决方案是在SYDR工具中实现的。 SYDR在路径谓词中进行分支反转。 Sydr将Dynamorio动态二进制仪器工具与Triton符号发动机结合在一起。我们在64位Linux可执行文件上评估了SYDR功能。
The security development lifecycle (SDL) is becoming an industry standard. Dynamic symbolic execution (DSE) has enormous amount of applications in computer security (fuzzing, vulnerability discovery, reverse-engineering, etc.). We propose several performance and accuracy improvements for dynamic symbolic execution. Skipping non-symbolic instructions allows to build a path predicate 1.2--3.5 times faster. Symbolic engine simplifies formulas during symbolic execution. Path predicate slicing eliminates irrelevant conjuncts from solver queries. We handle each jump table (switch statement) as multiple branches and describe the method for symbolic execution of multi-threaded programs. The proposed solutions were implemented in Sydr tool. Sydr performs inversion of branches in path predicate. Sydr combines DynamoRIO dynamic binary instrumentation tool with Triton symbolic engine. We evaluated Sydr features on 64-bit Linux executables.