英语原文共 11 页，剩余内容已隐藏，支付完成后下载完整资料
摘 要
在本文中，我们提出了一种新的通过程序进行跟踪价值流动的算法。我们的算法表示相对于现有技术有实质性的改进。我们的算法适用于大型程序，它对路径敏感。我们的算法的效率来自三个洞察：价值流问题可以通过跟踪“位向量化”一次一个值的流动；来自不同实体的数据流如果具有相同价值流信息的执行路径可以合并；信息复杂混叠的价值流可以从不同的分析中得到解决。我们已将我们的分析结合到ESP中，这是一种软件验证工具。我们使用ESP来验证出了Windows操作系统内核中存在的可能问题。这个经验表明我们的算法可以扩展到大型程序，并且是准确的足以追踪实际代码中的价值流。
关键词
价值流程，别名分析，路径敏感分析
- 引言
价值流分析已经在许多不同的领域进行了研究。例如，数据流分析协会已经研究了价值流分析定义[24,5]，功能性编程社区已将其作为流量分析和封闭分析进行了研究[22，29]，具有代表性的评估界已经对此进行了研究并将此作为最强的后置条件[16]。无论名称或地区如何，价值流分析都是答案以下问题：哪个内存位置保存a给定的利益价值[在某一特定节目点[沿着某个特定节目点]给出执行路径]。感兴趣的价值通常是象征性的;例如，我们可能有兴趣追踪流量作为参数传递给函数的不可信值在可信的代码库中。我们指的是这组内存保持值为“值别名集”的位置。近年来，基于过程间的软件验证工具价值流分析已经成熟[4,10,15]。这些工具使用详尽的分析来查找所有潜在的错误在一个程序中的某种特定类型。他们使用价值流分析以确定给定语句是否运作在给定的利益价值。例如，在一个给定的程序中，函数调用Lock（p→mLock）是否在该函数上运行由前面的函数调用l创建的锁对象= NewLock如果不是，程序可能包含一个锁定错误。答案取决于p→mLock是否在值的别名集l。限制软件采用的难题验证工具是没有已知的价值算法流量分析既足够准确以用于这些流量分析工具，并且可扩展到足以在大型程序上运行。在本文提出了这样一种算法。我们的算法是可扩展的，并且对路径敏感，因为它消除了价值从不可行的执行路径流动信息。我们的算法基于三种不同的见解，每种都不相同其中允许我们重复使用以前的工作结果一个新的上下文。本文的技术优点在于这些想法的适应和组合产生一个有用的结果。
第一个见解是价值流分析是可分离的数据流问题[24]，即使存在内存如果我们计算出内存别名的计算，就会出现混叠来自价值流量分析。众所周知，可分离的数据流问题可以进行位向量化，从而产生用每个子问题的更小的内存占用量进行分析[23]。因此，我们可以为其计算值别名集一次感兴趣的价值。第二个见解是，对于一个给定的兴趣值，程序中的大多数分支不会影响其值别名集，即使它们影响着具体的执行状态程序。因此，我们可以使用在[10]中描述设计的一个可扩展的路径敏感分析选择性合并技术，该路径仅跟踪相关分支。
我们的“价值流仿真”算法识别相关分支机构如下：我们象征性地评估该计划，生成包含执行的符号状态状态和值别名集。在控制中的合并点流程图，如果两个符号状态具有相同的值别名集，我们通过合并产生一个单一的符号状态他们的执行状态。否则，我们处理符号分开陈述。这种方法避免了完全路径敏感的成本分析，但捕获相关的相关性。
第三点是当计算值别名集时在带有内存别名的程序中，我们可以使用compact占位符代表内存别名而不是代表所有内存别名明确地在值别名集中。这种价值别名集的隐式表示使我们能够将精确的价值流分析与众所周知的可扩展性结合起来内存别名分析[9,18,11]，甚至当不精确时的可扩展分析可能会导致非常大的别名集。我们工作的动机是启用软件验证工具。更一般地说，许多重要的分析是价值流分析实例。例如，调用图构建涉及跟踪函数名称的流程间接调用网站，以及内存别名分析本身涉及跟踪内存地址流以取消引用操作。价值流仿真提供了可扩展的，路径敏感的解决这些和其他问题的方法。
在本文中，我们做出以下贡献：
bull;我们呈现价值流模拟，一个新的框架用于程序间，上下文敏感，路径敏感价值流分析使该框架可以被实例化通过修改值别名的传递函数的选择集合和符号执行状态。
bull;我们引入价值别名集的概念，并提供这些集合上的传递函数。值别名集使客户分析甚至可以执行强大的更新在存在别名的情况下。我们展示如何信息从现成的内存别名分析可以用来保守和有效地更新值别名集。
bull;我们在ESP中使用价值流模拟，这是一种软件验证C代码工具。我们使用ESP的经验验证Windows操作系统内核一个重要的安全属性表明：- 价值流模拟是可扩展的。 ESP能够跟踪用户输入值的流向百万行内核代码。- 价值流模拟是准确的。粗略的由ESP跟踪的500个输入值，它无法准确追踪流量（导致虚假错误报告）30个值，失败率为6％。
本文的其余部分组织如下：在部分2，我们为我们的方法提供了激励的例子。在第3节，我们介绍程序间价值流模拟。在第4节中，我们提出了一系列价值转移函数别名集。在第5节中，我们描述了我们的实验Windows内核。我们在第6节总结相关工作，并在第7节得出结论。
- 例子
在本节中，我们使用示例来解释值别名集和价值流量模拟，并展示他们如何改进之前的工作。
2.1值别名集
考虑操作中的（简化）代码片段系统内核如图1（a）所示。假设我们是有兴趣强制执行内核函数的属性应该只能释放以前获得的锁。对于示例程序，分析需要检查在第k行创建锁的每条路径上被释放，它以前被收购。分析必须能够将锁的状态更新为“获得”之后第一行问题是线路l上的呼叫运行指向未知内存位置的指针表达式。在以前的方法中，要么分析涉及昂贵的形状/堆分析[22,27]或分析被迫执行弱更新，这意味着锁可能或可能没有被收购。这将导致一个在UnLock调用中发生虚假错误报告。我们想要一个分析，即使通话也可以执行强大的更新不依靠任何指针表达式在昂贵的形状分析上我们的解决方案是引入价值别名集的概念。直观地，为给定的兴趣值设置值别名包括程序中评估的那些表达式在特定点的给定值。例如，在线l在示例中，为在上创建的锁定设置的值别名行k是{p→mLock}。这意味着无论哪个内存位置p→mLock指的是，所持有的值内存位置是在第k行创建的值。结果是，我们可以对锁的状态进行强有力的更新第一行在第4节中，我们正式定义了价值别名集并提供了值别名集的传递函数。
2.2价值流模拟
考虑图1（b）所示的代码。假设我们是有兴趣执行内核应该的属性不是取消引用从用户代码传入的NULL指针。对于示例程序，分析需要跟踪通过指针参数传入的值的流量o和p在代码中取消引用操作KernelEntryPoint。分析必须跟踪相关性只有当o？= NULL时，q才保存用户指针o的值。在换句话说，分析必须是路径敏感的。以前路径敏感价值流分析方法[5,4]不能扩展到大型节目。正如第1节所述，我们可以将问题向量化通过独立跟踪参数o和p的值流。这种位矢量化导致两个正交可扩展性的改进：首先，数据流的大小事实减少。我们需要计算和存储价值别名一次只设置一个参数。其次，分支机构较少在代码中是相关的。在这个例子中，第二个分支与参数o的价值流无关，而第一个分支与参数p的值流无关。
示例1.考虑跟踪值的分析
(a) void Process() {
k: p-gt;mLock = NewLock();
l: Lock(p-gt;mLock);
...
UnLock(p-gt;mLock);
}
(b) void KernelEntryPoint(int *o, int *p) {
if (o != NULL)
q = o;
else
q = malloc();
if (p != NULL)
r = p;
else
r = malloc();
m: *q = data1;
*r = data2;
}
图1：来自OS内核的代码片段。如所描述的，通过计算符号状态来参数o的流动在第1节中。可能的符号状态在行下面描述三种可能的分析推断。每个符号状态都包含值别名集和模拟州。值别名集有两个组成部分：“必须”设置（显示为{}）包含表达式，在“May”设置的情况下，将评估值追踪到所跟踪的值（显示为{}？）包含可能评估的表达式到跟踪值全路径敏感分析。有四个可行的到第m行的路径，导致状态：
[{o}{o}?, o = NULL, q = new, p = NULL, r = new]
[{o}{o}?, o = NULL, q = new, p = NULL, r = p]
[{o, q}{o, q}?, o = NULL, q = o, p = NULL, r = new]
[{o, q}{o, q}?, o = NULL, q = o, p = NULL, r = p]
这些状态捕捉变量q所处的相关性值别名设置，意味着第m行的语句dereferences参数o，iff oDagger; NULL，所以没有错误。标准数据流分析。符号状态被合并在CFG的加入点。因此，单一的象征第m行的状态是[{o} {o，q} ?,？]这个状态允许分析考虑o = NULL和q的可能性值别名集，导致在第m行错误报告。价值流模拟。符号状态来自第一个分支的两条腿具有不同的值别名集合，因此不合并。第二个分支没有影响参数o的值别名集。所以，四由第二个分支产生的符号状态被合并分成两个州：
[{o} {o}？，o = NULL，q = new]
[{o，q} {o，q}？，oDagger; NULL，q = o]
这些状态可以捕获所需的相关性，但可以放弃来自第二个分支的不相关的相关性。
- 价值流程模拟
在本节中，我们将介绍价值流模拟，一种算法用于程序间，上下文敏感和路径敏感价值流分析。价值流模拟是基于在前面描述的“属性模拟”算法上深入[10]。关键的区别是属性模拟传播抽象有限状态机状态为其数据流事实，而价值流模拟传播值别名集。我们提到读者[10]或[13]有关这两种算法的更多细节，包括终止和复杂性论证。在这里，我们为整个程序间提供pseduocode价值流模拟的版本，我们提供了一个概述该算法的两个关键要素：选择性合并象征性的国家，有效地处理程序调用。
3.1一个简单的命令式语言
价值流模拟运行于超图的[26] a程序。超图包括每个标准的CFG程序和代表程序间控制的边缘流。超图包含以下几种节点和边缘：
计算：赋值语句，单个后继者
分支：有条件分支，真/假接班人
调用：“无参数”过程调用
后继者：被调用者的入口节点
条目：程序条目，单个后继者
退出：程序退出
后继者：CallReturn呼叫者的节点CallReturn：从过程调用返回我们假设所有的间接电话已被替换直接调用使用某种形式的调用图分析[25]和该过程调用已被简化为无参数（c.f. [21]）。例如，调用foo（x y，z * 2）来运行foo（int a，int b）被替换为：t1：= x y; t2：= z * 2; a：= t1; b：= t2; FOO（）3.2域我们使用适当命名的访问函数来提取来自CFG节点的边缘信息，反之亦然。该算法引用了以下域：
N个CFG节点、F功能、S模拟状态、VA价值别名集、C = Ntimes;VAtimes;VA
分析坐标传递函数查找与之关联的表达式CFG节点和计算新信息的前缀为M.由va和s指定的函数适用于值别名设置和模拟状态，分别。进入功能图从呼叫者到被叫者的信息，输出功能地图信息从被叫到呼叫者，以及Over功能保留呼叫站点的信息不能被被呼叫者修改。
3.2概述
给出了价值流仿真（VFS）的伪代码见图2.给定一个变量t和一个程序点n at其中t被分配跟踪值（我们将n表示为“创建点”），该算法计算值别名集对于在所有节目点的n产生的价值。
Global
1 Worklist : 2C
2 Info : C → S
3 Summary : (F times; VA) → 2C
procedure Solve(Global G = [N,E,F] Value = [t, n])
begin
4 star
全文共21323字，剩余内容已隐藏，支付完成后下载完整资料
资料编号：[13699]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
