基于断言制导的多线程符号执行的设计与实现

发布时间：2021-07-04 10:19

　　现代社会,软件已经成为最重要的基础设施之一,在很多行业中发挥着不可或缺的作用。同时,软件的安全性也越来越受人们的重视。软件测试作为保障软件可靠性的重要手段之一,一直以来都是国内外科研人员的研究热点。动态符号执行技术是软件测试领域的前沿技术,从诞生以来一直受人们的广泛关注。国内外研究人员基于动态符号执行技术开发了很多实用的软件测试工具,KLEE就是其中的佼佼者。然而,KLEE只能对单线程程序进行符号执行。鉴于此,瑞典洛桑联邦理工学院的Stefan Bucur与其合作伙伴在KLEE的基础上开发了并行符号执行工具Cloud9,实现了对多线程程序的符号执行。但是Cloud9在对多线程程序进行符号执行时没有考虑线程交错调度问题,不能完全探索多线程程序的所有路径。因此,本文在Cloud9的基础上,设计并实现了可以覆盖所有路径分支的一般多线程符号执行框架,并在此基础上,提出了基于断言制导的多线程符号执行方法。本文的主要贡献包括以下三点:在研究了符号执行基本理论和Cloud9对多线程程序符号执行的方法的基础上,给出了可以覆盖所有路径分支的一般多线程程序符号执行框架,从三个方面来讲述:首先,对多线程符号... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：70 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
缩略语对照表
第一章 绪论
    1.1 研究背景与意义
    1.2 国内外研究现状
    1.3 研究内容和组织结构
        1.3.1 研究内容
        1.3.2 组织结构
第二章 相关理论与技术
    2.1 动态符号执行概述
        2.1.2 动态符号执行基本流程
        2.1.3 动态符号执行各模块介绍
        2.1.4 动态符号执行面临的挑战
    2.2 KLEE概述
        2.2.1 解释模块
        2.2.2 符号表示模块
        2.2.3 约束求解模块
        2.2.4 路径选择模块
        2.2.5 错误检测模块
    2.3 Cloud9概述
    2.4 本章小结
第三章 基于断言制导的多线程符号执行的设计
    3.1 一般多线程符号执行
        3.1.1 多线程程序的描述
        3.1.2 广义交错图
        3.1.3 算法描述
    3.2 基于断言制导的多线程符号执行
        3.2.1 主要思想
        3.2.2 算法描述
        3.2.3 最弱前置条件的计算
        3.2.4 b-PP结点的谓词摘要
        3.2.5 i-PP结点的谓词摘要
        3.2.6 基于谓词摘要的冗余执行修剪
        3.2.7 谓词摘要的优化
    3.3 本章小结
第四章 基于断言制导的多线程符号执行的实现
    4.1 方法实现的流程框架
    4.2 符号执行模块
    4.3 谓词摘要计算模块
        4.3.1 递归过程的实现
        4.3.2 结点分类的实现
        4.3.3 状态更新的实现
        4.3.4 谓词摘要生成的实现
    4.4 冗余执行修剪模块
    4.5 本章小结
第五章 实验与结果分析
    5.1 实验环境介绍
    5.2 实验测试
    5.3 实验结果分析
    5.4 本章小结
第六章 总结与展望
    6.1 总结
    6.2 展望
参考文献
致谢
作者简介


【参考文献】：
期刊论文
[1]计算机软件中安全漏洞检测技术的应用[J]. 陈楷.  数字技术与应用. 2010(07)
[2]浅谈代码安全质量保障中的模糊测试技术[J]. 邓承志,朱卫东.  信息网络安全. 2009(02)
[3]基于污点分析的源代码脆弱性检测技术[J]. 孔德光,郑烇,帅建梅,陈超,葛瑶.  小型微型计算机系统. 2009(01)
[4]软件安全漏洞的静态检测技术[J]. 张林,曾庆凯.  计算机工程. 2008(12)

硕士论文
[1]基于动态符号执行的MSVL程序模型检测理论与方法[D]. 卜康康.西安电子科技大学 2015



本文编号：3264606