一个正式验证的NAT(2)

目标属性。 Vigor证明了这个NF永远不会崩溃（一个低级属性的例子），它永远不会产生一个包含目标端口9（语义属性的例子）的数据包。对于后者，证明的要点是显示代码不会将目标端口9压入环形分组，并且环形不会改变存储的分组; 这两个属性意味着一个弹出的数据包永远不会有目标端口9.有三个步骤：

第一步：功能合同和证明。对于libVig数据类型的每种方法，libVig开发人员编写一份合同，即该方法保证的正式规范; 她还写了一个正式的证明，说明该方法的实施符合合同。这是一个重要的任务，但可以分摊到潜在的许多使用相同数据类型的NF。图3显示了合同（ll.2-6）和ring_pop_front函数的实现，它删除了ring前面的数据包。合同规定，这个函数不会损坏环，会移除环前面的包，并且会遵守一些对环中所有包持有的约束（1.6），只要环是在良好的状态，并在函数被调用之前尊重这些约束（l.2）。在合同中，packet_constraints_fp是一个抽象函数，即契约说ring_pop_front将会在任何包被约束之前保持任何包的约束。 NF开发人员可以在使用libVig时提供所需的约束; 在这个例子中，所提供的约束（图2）也方便地用作循环不变量。§5.1.2具有libVig合同的细节。

图3 摘自ring_pop_front（）及其正式合约的实施

步骤2：彻底的符号执行。（a）Vigor用呼叫符号模型来代替访问状态或与网络交互的所有函数调用。例如，ring_pop_front（图4中的模型（a））的符号模型通过packet_constraints返回具有完全符号内容的分组（即，其内容可以是任何

内容的分组），以使其目标端口不同于9。尽管它很简单，但是这个模型捕获了在我们的上下文中重要的ring_pop_front的所有行为，也就是说，它永远不会产生一个包含目标端口9的数据包。（b）一旦所有的函数调用被符号模型的调用所取代，Vigor就象征性地执行结果代码。尽管Vigor正在执行真正的C代码，但是由于模型是无状态的并且只有很少的分支点（如图4所示），所以这个步骤会很快结束，并且循环注释有助于防止不必要的展开。这种彻底的符号执行有两个结果，都假设符号模型是有效的：首先，它证明了目标低级属性（即，NF不能为任何输入而崩溃）成立。其次，它产生所有可能的函数调用序列，这些序列可能是由于运行代码而产生的，以及每次调用之后对程序状态的限制。图5显示了一个这样的呼叫序列，当环充满时产生。有关详尽的符号执行的详细信息，请参阅第5.2.1节。

图4ring_pop_front的符号模型

第3步：懒惰模型验证。（a）对于访问状态的每个函数调用，在每个可行的调用序列中，Vigor验证用于在步骤2中通过符号执行产生推测验证的符号模型是回想起来的，对于该调用是有效的。这个有效性意味着模型的输出是实际实现可能产生的输出的超集（在限制符号状态的意义上）。例如，考虑调用ring_pop_front（图5,1.13）：Vigor在步骤2中符号执行模型之后提取对符号程序状态的约束; 在调用之后插入这些所谓路径约束的断言（l.16）; 并要求证明检查员验证这个断言是否与ring_pop_front的合同兼容（详见§5.2.3）。证明检查器得出结论，特别是模型的输出（一个目标端口可以不是9的数据包）是由函数的契

约指定的输出的超集，因此也是函数的实现（自Step （b）Vigor验证在每个包send（）之后（图5中未示出），目标语义属性成立，即输出包没有目标端口9。更多细节在§5.2.2中。

无效的模型。无效的模型会导致步骤2或步骤3失败，但是不会导致错误的证据。例如，图4中的模型（b）对于我们的目的来说太抽象了：它返回的内容可能是任何东西的包，包括有一个目标端口9。这是验证发言中的“过度近似”模型。如果Vigor在步骤2中使用该模型，则步骤3b失败：因为模型可以返回具有目标端口9的分组，所以Vigor无法验证所有的输出分组没有目标端口9的调用序列。相反，图4中的模型（c）对于我们的目的来说太具体：它总是返回一个带有目标端口0的分组，即它是“近似（under-approximate）”模型。如果Vigor在步骤2中使用这个模型，则步骤3a失败：回想一下，对于每个调用，Vigor获得在步骤2中符号执行模型之后保持的路径约束，并且在调用之后插入一个断言对于这些路径约束。有了这个模型，断言将是// @assert（arg2.port？0）。证明检查器不能确认这个断言总是正确的，因为ring_pop_front的契约（图3,11.4-6）为arg2.port指定了比0更宽的范围。

图5 由步骤2得到的示例函数调用序列，由Vigor用路径约束断言（l.16）进行了注释

本节说明了Vigor如何通过函数调用序列通过证明验证缝合符号执行。在这个证明中还有一些其他的步骤（在这里省略是为了清楚起见），我们在§5中做了充分的描述。

4 证明的属性

我们使用§3中概述的方法验证了我们的NAT（我们称之为VigNAT）。我们现在描述我们验证的具体属性。

4.1语义属性

我们证明了VigNAT正确地实现了传统NAT RFC [53]中指定的语义。为此，我们编写了一个NAT规范，将RFC的解释形式化，我们认为这与典型的NAT实现相一致。规范[58]有300行分离逻辑[51]，需要3个人日才能完成。

从分组到达对抽象状态（flow_table）的影响来看，我们从正式描述NAT行为开始，如图6所示。有三个静态配置参数：流量表（CAP）的容量，流量超时（Texp）和外部接口（EXT _IP）的IP地址。

图6 NAT语义属性的正式规范的概念总结（基于RFC 3022）

F（P）函数根据流的源和目标IP地址和端口从流表中提取数据包流ID。随着每个数据包到达（l.1），NAT发现并移除过期流（l.2），根据接收到的数据包更新流表（l.3），然后潜在地重写数据包并转发它（l.4）。为了更新流表，NAT查找与接收到的数据包具有相同流ID的所有条目，并更新它们的时间戳（ll.10-12）。如果没有匹配的条目（l.13），并且如果数据包到达内部接口（l.14），并且如果流表未满（l.15），则NAT在流表（l.16）中添加新条目。如果此时在流

百度搜索“77cn”或“免费范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，免费范文网，提供经典小说综合文库一个正式验证的NAT(2)在线全文阅读。