面向符号执行的内存模型研究

发布时间：2024-05-07 03:57

　　在软件可信性质保证的诸多方法中,面向软件源代码的分析与验证具有重要意义。形式化方法在软件可信性质保证中有不可替代的作用,但是距离大规模广泛应用还有不小的差距。符号执行是一种重要的形式化方法,在测试数据生成和静态分析中有广泛应用。但是,符号执行面临一些问题。其中,内存模型是影响符号执行的精确性和可扩展性的主要问题之一。 论文综述了面向符号执行的内存模型问题的研究现状,分析了符号执行中符号状态跟踪面临的主要问题和现有的内存抽象的不足,提出了基于抽象符号表的内存模型。抽象符号表的基本思想是,通过为可寻址对象生成抽象地址统一处理各种数据类型和建模内存操作。研究了使用抽象符号表建立内存模型的方法,给出了抽象地址生成方法以及符号执行算法。基于抽象符号表的内存模型能够很好地解决面向符号执行的内存模型面临的主要问题,包括指针和别名问题、类型不安全的内存访问和大小不确定的数据。最后,通过实验评估了基于抽象符号表的内存模型,设计的一个符号执行工具能够精确地跟踪符号状态,并且通过与其他内存模型的比较,说明了这个内存模型具有一定的可扩展性。 精确而且可扩展的内存模型是提高符号执行技术的实用性的关键,能够有效地...

【文章页数】：64 页

【学位级别】：硕士

【部分图文】：

则SymbolicState=<M,I号值的映射；，即程序计数器，指向下一个件。成面向硬件机器的目标代码，编语言定义精确的符号语义。编程，它定义各种数据类型的符号表状态下，程序控制的流动。如同bolicState=<M,IP,PC>更新置如下：PC的初始值设为....

存消耗也十分巨大。因此，精确的表示每字节数组内存模型对即使很小的代码段也代码没有动态内存分配并且是类型安全的代码，但是不能精确分析系统软件。monolithicmemorymodel）[26]在系统软件的7]的内存模型本质上就是单片内存模型。单分为不相交的区域（region）....

国防科学技术大学研究生院硕士学位论文存访问只发生在少数数据上[26]。所以这种保守做法不但浪费大量存储空间，增加了数据读写代价。然而，ASTable对类型不安全的内存访问的支持是需求的，其可扩展性比字节数组方法和单片内存模型都好。用下面图4.3中的一个的例子演示三者之间的区别....

ainteger1node1S5120678910p&char15node2S105图4.7ASTable方法在图4.3代码片段的L2处的内存布通过为每个大小不确定数据生成单独的全局ASTable，允许这缩或扩展，而不必在这些数据生成时对其大小....

本文编号：3966787