符号执行中约束求解结果重用技术的比较  

Comparison of Constraint Solving Solutions Reuse Techniques in Symbolic Execution

作　　者：胡小辉 应时[1] 赵学博 罗琦凡 浦帆 贾向阳[1] HU Xiaohui;YING Shi;ZHAO Xuebo;LUO Qifan;PU Fan;JIA Xiangyang(School of Computer Science,Wuhan University,Wuhan 430072,Hubei,China;Wuhan Institute of Virology,Chinese Academy Sciences,Wuhan 430071,Hubei,China)

机构地区：[1]武汉大学计算机学院,湖北武汉430072 [2]中国科学院武汉病毒研究所,湖北武汉430071

出　　处：《武汉大学学报（理学版）》2020年第3期277-284,共8页Journal of Wuhan University:Natural Science Edition

基　　金：国家重点研发计划项目(2016YFC1202204)。

摘　　要：约束求解耗时一直是符号执行的瓶颈之一,约束求解结果重用是一种有效提高符号执行效率的方法。本文对约束求解重用技术Green、Klee-R、GreenTrie及Green、Utopia进行比较,证明了前三者重用能力从高到低依次是GreenTrie,Klee-R,Green,后两者中Utopia的重用能力高于Green。在动态符号执行场景下对四种重用方法的重用效率进行了实验比较,证明重用技术的重用效率并不完全取决于重用能力,并进一步从程序的特点、约束的类型以及约束的次序对重用效率的影响进行了分析和比较。本文的工作为约束求解重用领域的研究提供了综述和评估,可以为未来该领域的研究提供借鉴。Constraint solving is the blockneck in symbolic execution and constraint solving solutions reuse is an effective way to re⁃duce cost of symbolic execution.We conduct a comparative study on four solution reuse approaches.Among Green,Klee-R,GreenTrie,we prove that the reuse ability from high to low is GreenTrie,Klee-R,Green,and between Utopia and Green,Utopia􀆳s reuse ability is higher than that of Green.We also compare the efficiency of four reuse methods under the dynamic symbolic exe⁃cution scenario and prove that the efficiency of a reuse technology does not depend entirely on its reuse ability.We further analyze the factors which affect the reuse efficiency,including characteristics of programs,the type of constraints and the order of con⁃straints.A survey and an evaluation on the solution reuse approaches have been made useful for future research.

关 键 词：符号执行 约束求解 重用 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]