基于分支混淆算法的符号执行技术  

Symbolic Execution Based on Branch Confusion Algorithm

作　　者：过辰楷[1,2] 姬秀娟[1,2] 许静[1,2] 

机构地区：[1]南开大学信息技术科学学院,天津300071 [2]南京大学计算机软件新技术国家重点实验室,南京210093

出　　处：《计算机科学》2012年第9期115-119,共5页Computer Science

基　　金：南京大学计算机软件新技术国家重点实验室开放课题(KFKT2010B22);天津市科技攻关项目(08ZCKFGX01100)资助

摘　　要：符号执行是静态分析中的一项常用技术,数组元素混淆问题是限制符号执行本身性能的关键因素之一。通过分析数组混淆实质,提出了一种分支混淆算法,利用边混淆边符号执行的策略,可以处理较为复杂的数组问题。该策略使用实时的约束求解,及时地剪除不可达的混淆分支。结合符号执行和约束求解技术,开发了基于分支混淆算法的工具原型ASym。初步实验表明,利用分支混淆算法可以处理具有分支结构的数组混淆问题,避免延迟替换出现的数组语义误差,且在很大程度上缩减了分支数量,提高执行效率。Symbolic execution is a common static analysis technology.Issue of array element confusion is one of the key factors limiting symbolic execution performance itself.Through analysis to array confusion essence,branch confusion algorithm was proposed.With the strategy that manages confusion algorithm and symbolic execution in the same time,some complex array problems were solved.Using the real time method of constraint solving,infeasible confusion branches were cut in time.Combining with symbolic execution and constraint solving,the prototypical tool ASym was developed,which was based on improved confusion algorithm.Primary experiments show that it can solve the confusion problem in branch structure and avoid array semantic error in delay replacement.Meanwhile,extensional branches are dramatically reduced and efficiency is improved.

关 键 词：符号执行 软件测试 数组混淆 约束求解 

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