论文部分内容阅读
当今世界,软件已经在我们的生活和生产中发挥着基础性的作用。与其重要性相伴的,是人类对软件安全日益增加的重视。对于那些安全攸关的大型软件系统,为了保证其安全可靠,已经有各种各样的方法被发明出来用以避免由此带来的损失。符号执行是一种在特定领域十分有效的用来提高软件质量的方法。符号执行以对变量的约束代替具体数值对程序进行模拟执行,用相对低的代价达到较高的路径覆盖率,以自动化的生成测试例以及搜寻程序中的缺陷。ShapeChecker是一个面向C语言的符号执行分析器,利用Clang作为前端,对由源代码编译得到的LLVM中间表示进行符号执行分析,可以找出程序中诸如访问越界、悬垂指针和算术溢出这样的错误。作为一种基础性的编程语言,由于其使用领域的敏感性和相对其他主流编程语言的脆弱性,C++一直是静态分析软件所关注的重点。在本文中,为了使ShapeChecker分析器能够对C++语言的程序进行分析,我们对其提出了一系列修改和扩展,包含:·一组在符号执行过程中引入标记和使用类型信息的方法,使用类型信息辅助分析的过程;·一组对ShapeChecker断言语言和执行状态的扩展,使其能够支持对包含异常处理特性的代码进行正确的符号执行分析;·一组对内存状态和内存谓词的修改,使ShapeChecker能够检测出使用C++内存管理机制的代码中隐藏的缺陷。通过实现文中的工作,我们成功使ShapeChecker分析器支持对包含了虚函数调用、运行时类型信息、异常处理等语言特性的代码,并给出了良好的分析效果。本文提出的方法已经在ShapeChecker上进行了实验,取得了对C++语言良好的分析效果。