检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

符号执行中的约束求解问题研究进展

北京理工大学学报 2019年第9期39卷 957-966页

作者：邹权臣吴润浦马金鑫王欣辛伟侯长玉李美聪中国信息安全测评中心北京100085 360安全研究院北京100016 北京中测安华科技有限公司北京100085

在符号执行中,约束求解主要负责路径可达性进行判定及测试输入生成的工作,但路径爆炸问题带来的频繁调用,以及SMT求解器本身的能力和效率的不足,使得约束求解占用了符号执行中主要的性能开销,约束求解问题也成为符号执行中面临的主要瓶... 详细信息

在符号执行中,约束求解主要负责路径可达性进行判定及测试输入生成的工作,但路径爆炸问题带来的频繁调用,以及SMT求解器本身的能力和效率的不足,使得约束求解占用了符号执行中主要的性能开销,约束求解问题也成为符号执行中面临的主要瓶颈问题之一.本文介绍了符号执行和约束求解的基本概念,并分析了符号执行中约束求解问题的由来,对近年来的约束求解问题研究进展进行了归类,涉及的技术包括非相关约束分支切片、约束简化、快速不满足性检查及多求解器支持等.对这方面的研究进行了展望和总结.提出未来工作应在提高路径约束逻辑精简率、提高约束求解结果存储和重用的效率、约束求解并行化以及约束求解配置预测等方面展开.

关键词：符号执行约束求解性能优化漏洞挖掘

使用共享变量分析和约束求解检测安卓应用数据竞争

在线全文

学校读者我要写书评

暂无评论

软件学报 2019年第11期30卷 3281-3296页

作者：孙全许蕾夏昕濛张卫丰计算机软件新技术国家重点实验室(南京大学) 江苏南京210023 南京大学计算机科学与技术系江苏南京210023 南京邮电大学计算机学院江苏南京210023

安卓系统在移动端操作系统始终占据主导地位,在增强用户体验和提高程序性能的同时,其特有的事件驱动模型和多线程模型也造成了并发缺陷.并发程序中,线程调度的不确定性和难以再现性是并发缺陷检测困难的原因.现有技术主要在动态生成执... 详细信息

安卓系统在移动端操作系统始终占据主导地位,在增强用户体验和提高程序性能的同时,其特有的事件驱动模型和多线程模型也造成了并发缺陷.并发程序中,线程调度的不确定性和难以再现性是并发缺陷检测困难的原因.现有技术主要在动态生成执行路径的基础上进行发生序(happens-before)分析,进而检测安卓应用的并发缺陷,但仍然存在低覆盖率、误报、漏报等问题.结合共享变量分析和约束求解方法实现了安卓应用数据竞争的检测,并实现了检测工具RaceDetector.该工具首先根据安卓系统的特性和数据竞争的定义,通过静态分析抽取相关信息,并进一步使用安卓共享变量分析来提高准确性和性能,继而进行可疑数据竞争分析,得出可疑的数据竞争集合;接着根据每一个可疑的数据竞争候选者,通过约束求解的方法在所有事件调度和线程调度解空间下识别发生序关系,并最终检测出真正的数据竞争.实验部分是从Google Play等来源收集了15个流行的应用APK文件作为数据集,RaceDetector平均报告了340个数据竞争,误报率为13%(44/340).与现有工具EventRacer(默认产生300随机事件触发应用执行,平均检测2个有害数据竞争)相比,RaceDetector能够解析全部源码,覆盖了所有线程调度和事件调度,平均检测出15个有害数据竞争.

关键词：安卓应用数据竞争事件驱动模型多线程模型约束求解

在线全文

学校读者我要写书评

暂无评论

基于变异和约束求解的程序缺陷自动修复方法

计算机工程与设计 2024年第1期45卷 88-94页

作者：董兰洪玫伍佳四川大学计算机学院(软件学院) 四川成都610065

为能正确高效地生成修复补丁,针对Java程序中出现频率较高的条件语句相关缺陷修复问题,将启发式搜索方法与语义约束求解方法相结合,提出一个有针对性、更高效的解决方案。针对条件语句缺失错误,采用基于组件的程序合成技术,合成满足约... 详细信息

为能正确高效地生成修复补丁,针对Java程序中出现频率较高的条件语句相关缺陷修复问题,将启发式搜索方法与语义约束求解方法相结合,提出一个有针对性、更高效的解决方案。针对条件语句缺失错误,采用基于组件的程序合成技术,合成满足约束的候选条件语句;针对条件语句逻辑表达式错误,采用变异技术,生成候选逻辑表达式;针对条件语句逻辑表达式错误中,不能用变异技术修复的缺陷,使用基于组件的约束求解方法生成候选补丁。实验结果表明,所提方法有更高的补丁召回率和准确率。

关键词：程序自动修复变异分析约束求解程序合成条件语句缺陷补丁生成软件调试

在线全文

学校读者我要写书评

暂无评论

约束求解算法自动配置研究

约束求解算法自动配置研究

作者：吴云鹏吉林大学

学位级别：硕士

各种经典、元启发式约束求解算法在求解NP难题(NP-hard)时的性能通常取决于其参数配置。事实上,为一个算法配置一个合适的参数一直以来都被认为是一个重要的任务,这就给每个算法设计者和用户留下了一个问题:如何正确配置算法参数?在过去... 详细信息

各种经典、元启发式约束求解算法在求解NP难题(NP-hard)时的性能通常取决于其参数配置。事实上,为一个算法配置一个合适的参数一直以来都被认为是一个重要的任务,这就给每个算法设计者和用户留下了一个问题:如何正确配置算法参数?在过去,人们一直使用手动方式进行参数配置,通过对各种算法的研究发现,手动处理参数事实上是个很复杂的问题,需要不断在运行过程中改变参数,开销大量的时间去测试程序以使之达到理想效果。这无疑是件很麻烦的事情,既浪费人力、物力、财力,也给程序员的编程带来了困扰。而且通过经验法或者试错法来进行优化,不仅耗时耗力还很容易出错,有时,它通常还会导致不同算法的不均匀优化。此外,通过试错法优化过度依赖直觉和算法开发者的经验,而该方法难以和严格的数学证明对应起来,因此手动参数配置不具有推广性。近些年,参数优化算法逐渐成为算法发展过程的重要组成部分。许多高性能算法都具有众多参数,参数配置对控制算法行为有重要影响,特别对于难解优化问题的求解算法尤是如此。寻找启发式算法性能优化的参数配置通常需要耗费相当大的开销。在多数情况下,参数配置都是以繁琐复杂的手工操作进行,对于配置人员的素质要求极高,因此自动化参数配置研究具有重要的实用意义。不仅如此,算法自动配置还有如下优点,它能够减少开发时间和人为的主动干预;能够为算法设计提供更加有力的技术支持;能够利用计算能力探索算法设计空间;能够为更高层次的任务释放人类的创造力;能够为算法设计者在设计程序时提供帮助。配置复杂算法参数是一个高度劳动密集型的工作,消耗整体开发时间的很大一部分。使用算法自动配置方法可以显著节省时间,甚至得到潜在的更好结果。在比较启发式算法性能时的核心问题是:如何使算法在本质上更胜一筹,该算法的成功原因是开发人员更成功地优化了其参数。算法的自动配置方法可以减轻不公平比较这个问题,从而促进更有意义的比较研究。复杂启发式算法求解困难实例的能力往往取决于参数的合适配置。而用户往往很少了解有关于算法参数配置对其性能的影响,因此简单地使用默认配置。即使算法已经经过标准的基准组精心优化,默认配置可能不是遇到的特定问题的实例的最佳配置,算法也就不能呈现最佳性能。算法的自动配置方法可以以一种根本性的便捷的方式改善算法性能。本文首先介绍了算法配置,算法配置问题的定义和相关概念,接下来又介绍了解决算法配置问题的一些方法,主要进行了两个方面的研究:(1)深入研究了目前流行的并有重要影响的算法自动配置参数的软件irace。使用irace软件为acotsp程序自动的配置参数,通过对参数在不同的配置下得到的结果进行细致的分析,相互比较,使得我们对算法自动配置有了更深一步的理解。(2)基于流行的ParamlLS算法配置框架,进行了约束求解器级别的算法自动配置的尝试,实验结果表明,约束求解器级别的算法自动配置对于约束求解效率提升明显。当然,约束求解算法以及约束求解器的自动配置还处于一个比较初级的水平,未来希望能对于约束求解算法进行更为深入的研究,从算法自动配置的角度为研究高效约束求解算法提供一种可能。

关键词：约束求解算法配置 irace ParamILS

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于静态插装和约束求解的整数漏洞检测

华中科技大学学报（自然科学版） 2014年第11期42卷 86-90页

作者：张帆张聪徐明迪杨捷杭州电子科技大学通信工程学院浙江杭州310018 武汉轻工大学数学与计算机学院湖北武汉430023 武汉数字工程研究所系统软件部湖北武汉430072 华南理工大学软件学院广东广州510006

以C源码为研究对象,提出了一种基于静态插装和约束求解的整数漏洞检测方法.首先在C源码中可能的整数漏洞点前面插装检测代码,同时定位可能导致整数漏洞的输入源,并将其标记为符号变量.之后将静态插装后的源码编译成可执行代码,并进行(... 详细信息

以C源码为研究对象,提出了一种基于静态插装和约束求解的整数漏洞检测方法.首先在C源码中可能的整数漏洞点前面插装检测代码,同时定位可能导致整数漏洞的输入源,并将其标记为符号变量.之后将静态插装后的源码编译成可执行代码,并进行(符号和具体执行的)混合执行.在动态执行的过程中,通过对插装代码对应的符号约束进行求解,可以检测整数漏洞是否存在,以及获得当整数漏洞存在时符号变量相应的具体取值.进一步地,通过对从程序入口点到整数漏洞点所经过路径上的所有条件跳转约束进行求解,获得引导程序到达整数漏洞点时符号变量相应的具体取值.结合两者可以辅助生成触发漏洞的输入用例.基于CVE(通用漏洞披露)通告的实验表明本系统能够成功检测到相应漏洞.

关键词：整数漏洞符号执行约束求解程序插装漏洞检测

在线全文

学校读者我要写书评

暂无评论

约束求解与优化技术的结合

计算机学报 2005年第11期28卷 1790-1797页

作者：季晓慧黄拙张健中国科学院软件研究所计算机科学实验室

提出了将混合约束问题转化为混合整数规划问题的方法.用约束求解方法及混合整数规划方法共同求解混合约束问题可以令二者相互借鉴,从而促进二者求解技术的进一步发展.同时,由混合约束问题转化而来的混合整数规划问题也可作为求解混合整... 详细信息

提出了将混合约束问题转化为混合整数规划问题的方法.用约束求解方法及混合整数规划方法共同求解混合约束问题可以令二者相互借鉴,从而促进二者求解技术的进一步发展.同时,由混合约束问题转化而来的混合整数规划问题也可作为求解混合整数规划问题的测试问题(benchmarks).

关键词：约束求解优化技术混合约束问题混合整数规划

在线全文

学校读者我要写书评

暂无评论

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

武汉大学学报（理学版） 2020年第3期66卷 277-284页

作者：胡小辉应时赵学博罗琦凡浦帆贾向阳武汉大学计算机学院湖北武汉430072 中国科学院武汉病毒研究所湖北武汉430071

约束求解耗时一直是符号执行的瓶颈之一,约束求解结果重用是一种有效提高符号执行效率的方法。本文对约束求解重用技术Green、Klee-R、GreenTrie及Green、Utopia进行比较,证明了前三者重用能力从高到低依次是GreenTrie,Klee-R,Green,后... 详细信息

约束求解耗时一直是符号执行的瓶颈之一,约束求解结果重用是一种有效提高符号执行效率的方法。本文对约束求解重用技术Green、Klee-R、GreenTrie及Green、Utopia进行比较,证明了前三者重用能力从高到低依次是GreenTrie,Klee-R,Green,后两者中Utopia的重用能力高于Green。在动态符号执行场景下对四种重用方法的重用效率进行了实验比较,证明重用技术的重用效率并不完全取决于重用能力,并进一步从程序的特点、约束的类型以及约束的次序对重用效率的影响进行了分析和比较。本文的工作为约束求解重用领域的研究提供了综述和评估,可以为未来该领域的研究提供借鉴。

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

基于约束求解的代码查询技术在StackOverflow上的实证研究

在线全文

学校读者我要写书评

暂无评论

计算机科学 2019年第11期46卷 137-144页

作者：陈正钊姜人和潘敏学张天李宣东南京大学计算机软件新技术国家重点实验室

代码查询在代码复用的过程中起着十分重要的作用,而面向程序员的专业问答网站StackOverflow上围绕代码的问答则是代码复用的一个典型场景。在这个现实场景中,采取的是人工回答的方式,而人工回答往往存在实时性较差、提问描述不准确、回... 详细信息

代码查询在代码复用的过程中起着十分重要的作用,而面向程序员的专业问答网站StackOverflow上围绕代码的问答则是代码复用的一个典型场景。在这个现实场景中,采取的是人工回答的方式,而人工回答往往存在实时性较差、提问描述不准确、回答可用性不高等缺点,但如果采取代码查询的方式搜寻可用代码来实现自动化并替代人工回答,则可以省去大量的人力和时间成本。目前已经出现了许多代码查询技术,但大都缺少在真实案例上的应用经验,文中以Satsy的思路为参考,实现了针对Java语言的基于约束求解的代码查询技术,并设计了实证研究,以StackOverflow为研究对象,主要研究如何将基于约束求解的代码查询技术应用在该网站上围绕代码的问答中。首先对网站上的问题进行了分析,针对Java语言提取了浏览量高的35个问题作为查询问题;然后在GitHub上抓取了约3万行代码,将它们转换成约束的形式并构建了一个较大规模的代码库以支持代码查询;最后通过对这35个问题的查询结果进行分析,评估了该技术在StackOverflow上的实际应用效果。结果表明,该技术在所研究的具体问题和代码规模上具有较好的实际应用效果,在相当高的程度上能替代人工回答。

关键词：代码查询约束求解开源代码库实证研究

模糊测试中的变异策略在约束求解上的应用探究

在线全文

学校读者我要写书评

暂无评论

电脑编程技巧与维护 2024年第6期 13-15,33页

作者：石永生江苏信息职业技术学院江苏无锡214153

模糊测试是一种先进的自动化测试技术,可用于检测程序潜在漏洞。大多数模糊测试技术在处理复杂约束时效果较差。为提高约束求解能力,提出了TurboFuzz技术,使用路径敏感分析建模变量约束关系,并采用模拟退火算法避免陷入局部最优。评估... 详细信息

模糊测试是一种先进的自动化测试技术,可用于检测程序潜在漏洞。大多数模糊测试技术在处理复杂约束时效果较差。为提高约束求解能力,提出了TurboFuzz技术,使用路径敏感分析建模变量约束关系,并采用模拟退火算法避免陷入局部最优。评估结果显示,TurboFuzz的边覆盖数量超过基于符号执行技术的工具,并求解出其他技术无法处理的约束。在真实程序测试中,TurboFuzz发现了13个新漏洞。研究通过比较不同技术、提出了TurboFuzz优化方案,提升基于变异的模糊测试的效率,使其成为有效的自动化测试技术。TurboFuzz为处理复杂约束开启了新思路,并为符号执行和模糊测试建立了联系。

关键词：模糊测试符号执行约束求解