二维码（扫一下试试看！） | | 符号执行中的约束求解问题研究进展 | | Survey of Constraint Solving Techniques Research Progress in Symbolic Execution | | 投稿时间：2018-06-23 | | DOI：10.15918/j.tbit1001-0645.2019.09.013 | | 中文关键词:符号执行约束求解性能优化漏洞挖掘 | | English Keywords:symbolic executionconstraint solvingperformance optimizationvulnerability discovery | | 基金项目:国家自然科学基金资助项目（U1636115，61502536，61872386）；国家重点研发计划项目（2016QY071401，2016YFB0800902） | | | 摘要点击次数:1507 | | 全文下载次数:407 | | 中文摘要: | | 在符号执行中，约束求解主要负责路径可达性进行判定及测试输入生成的工作，但路径爆炸问题带来的频繁调用，以及SMT求解器本身的能力和效率的不足，使得约束求解占用了符号执行中主要的性能开销，约束求解问题也成为符号执行中面临的主要瓶颈问题之一.本文介绍了符号执行和约束求解的基本概念，并分析了符号执行中约束求解问题的由来，对近年来的约束求解问题研究进展进行了归类，涉及的技术包括非相关约束分支切片、约束简化、快速不满足性检查及多求解器支持等.对这方面的研究进行了展望和总结.提出未来工作应在提高路径约束逻辑精简率、提高约束求解结果存储和重用的效率、约束求解并行化以及约束求解配置预测等方面展开. | | English Summary: | | In symbolic execution, constraint solving is mainly responsible for path reachability prediction and test input generation, but due to the path explosion problem and the limited power of the SMT solver, constraint solving occupy high overhead in symbolic execution, and this problem has become one of the bottlenecks in symbolic execution. This paper first introduces the basic concepts of symbolic execution, constraint solving, and analyzes the origin of the constraint solving problem. Second, this paper divides the optimization techniques in recent years into three stages:pre-solving, in-solving and post-solving. The related techniques include slicing, simplification, fast unsatisfiability check, multi-solver support, etc. Finally, the conclusions and prospects are made. It is proposed that the future work should focus on the improvements in respect of constraint reduction, constraint solutions reuse, parallel solving, solving configuration prediction, etc. | | 查看全文查看/发表评论下载PDF阅读器 | |
杨诗雨,苏丽丽,侯元伟,郝永乐,李伟平.面向漏洞管理的工作流技术应用研究[J].北京理工大学学报（自然科学版）,2019,39(9):967~973.YANGShi-yu,SULi-li,HOUYuan-wei,HAOYong-le,LIWei-ping.ResearchonWorkflowTech ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21郭磊,邢立华,袁倩,葛方俊.干式生化分析仪机载环境力学适应性技术研究[J].北京理工大学学报（自然科学版）,2019,39(10):1045~1050.GUOLei,XINGLi-hua,YUANQian,GEFang-jun.ResearchonMechanicalEnvironmentAdapt ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21魏光辉,纪凯夫,孟令媛.效应物置入对环境电磁辐射场强测试的影响[J].北京理工大学学报（自然科学版）,2019,39(11):1173~1179,1186.WEIGuang-hui,JIKai-fu,MENGLing-yuan.TheEffectofEUTonEnvironmentElectroma ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21李维浩,姚世明,李蔚清,苏智勇.面向AR沙盘异地协同标绘的动作重构技术[J].北京理工大学学报（自然科学版）,2019,39(12):1298~1303,1320.LIWei-hao,YAOShi-ming,LIWei-qing,SUZhi-yong.AMotionReconstructionTec ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21.北京理工大学学报2019年总目次（第39卷）[J].北京理工大学学报（自然科学版）,2019,39(12):1321~1338..[J].TransactionsofBeijingInstituteofTechnology,2019,39(12):1321-1338.二维码（扫一下试试看！）北京理 ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21张志广,李宁,包云肽,张阳天.基于小波变换的离子迁移谱信号处理技术[J].北京理工大学学报（自然科学版）,2019,39(S1):164~167.ZHANGZhi-Guang,LINing,BAOYun-Tai,ZHANGYang-Tian.SignalProcessingTechnologyfor ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21汪怡平,郭承奇,王涛,黎帅,姚云龙.基于自由变形技术的Ahmed模型气动减阻优化[J].北京理工大学学报（自然科学版）,2018,38(3):221~228.WANGYi-ping,GUOCheng-qi,WANGTao,LIShuai,YAOYun-long.AerodynamicDragRedu ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21孙崔源,薛里,孟海利,付天杰,康永全.几种典型爆破振动控制技术的试验研究[J].北京理工大学学报（自然科学版）,2018,38(4):359~363,370.SUNCui-yuan,XUELi,MENGHai-li,FUTian-jie,KANGYong-quan.ExperimentalResea ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21王登峰,蔡珂芳,张帅,马明辉.基于激光拼焊技术的汽车B柱结构优化设计[J].北京理工大学学报（自然科学版）,2018,38(7):691~697,708.WANGDeng-feng,CAIKe-fang,ZHANGShuai,MAMing-hui.StructureDesignofAutomotiv ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21曹猛,薛正辉,蔡洪伟,朱若晴.天线时域平面近场测试的信号源误差修正[J].北京理工大学学报（自然科学版）,2018,38(7):721~725,732.CAOMeng,XUEZheng-hui,CAIHong-wei,ZHURuo-qing.ErrorCorrectionforSourceofTim ... 北京理工大学科研学术 本站小编 Free考研考试 2021-12-21
| |
