一个正式验证的NAT(6)

首先，我们测量测试仪的出站和入站接口之间的数据包延迟。我们首先运行一组实验，其中所有NAT被配置为在2秒不活动之后使流过期。在每个实验中，测试者产生10-64,000个“背景流”，总共产生10万pps，在整个实验中永不过期，1000个“探测流量”产生0.47 pps，并在每个包后过期。我们使用背景流来控制流表的占用，而我们测量属于探测流的数据包的延迟。我们专注于探测流程，因为从性能的角度来看，它们是NAT NF最糟糕的情况：它们的每个数据包都会导致NAT在其流表中搜索匹配的流ID，找不到任何匹配，并创建一个新的条目。

图12显示了对于三个DPDK NF，探测流经历的平均等待时间作为背景流数的函数：经验证的NAT（5.13μsec）比未验证的NAT（5.03μsec）具有高2％的等待时间，以及比无操作转发（4.75μsec）高8％。因此，除了由于数据包接收和传输造成的延迟之外，未经验证和已验证的NAT分别添加了0.28μs和0.38μs的NAT特定的数据包处理。对于所有三个NF，延迟保持稳定，因为流量表占用率增长，这表明两个NAT使用良好的散列函数来将负载均匀分布在它们的表中。延迟增加（至5.3μsec）的唯一情况是经过验证的NAT，当流量表几乎变满时（绿线在最后一个数据点向上弯曲）。 Linux NAT具有显着更高的延迟（20微秒）。

为了给出延迟变化的意义，图13示出了当存在60,000个背景流（即92％占

用率）时，探测流所经历的延迟的补充累积分布函数（CCDF）：经验证的NAT稍微更重比未验证的NAT还要好; 所有三个NF都具有高于平均值两个数量级的异常值，但这些都是由于DPDK数据包处理，而不是NAT特定的处理（三条曲线重叠超过6.5μsec的延迟）。针对不同数量的背景流计算的CCDF看起来相似。

在第二组实验中，我们得到了类似的结果，其中测试者产生与之前相同的流量混合，但是NAT被配置为在60秒不活动之后到期流量（因此探头流量和背景流量都不会过期）。在这种情况下，经过验证的NAT的平均延迟略低（5.07μsec），而未验证NAT的平均延迟与之前（5.03μsec）相同。

最后，我们测量每个NF实现的最高吞吐量。在每个实验中，测试者都会生成一个永不过期的固定数量的流，每个流以固定的速率生成64字节的数据包，我们测量吞吐量和数据包丢失。在所有的实验中，Middlebox都是CPU绑定的。图14显示了作为所产生的流的数量的函数，由每个NF实现的具有小于0.1％分组丢失的最大吞吐量。已验证的NAT（1.8 Mpps）比Unverified NAT（2 Mpps）

低10％。这种吞吐量的差异来自两个NAT施加的NAT特定处理延迟（0.38μsvs.0.28μsec）的差异：在我们的实验设置中，这个延迟差别不能被掩盖，因为每个NF在单个核心上运行并且处理一次一个数据包。 Linux NAT的吞吐量显着降低（0.6 Mpps）。

实质上，这些结果表明，libVig流表（具有正式的说明和证明）的性能与DPDK哈希表（两者都不具有）的性能接近，尽管不相同。这两个数据结构的实现是完全不同的。我们并没有尝试重用/修改DPDK哈希表的实现，因为它通过单独的链接项来解决哈希冲突，哈希到同一个数组位置的项被添加到同一个链表中，这是一个很难在正式合同。相反，libVig流表通过开放寻址来解决冲突：如果一个项目哈希到一个占用的数组位置，它将被存储在下一个空闲的数组位置，以及辅助元数据，以加快查找速度。我们还没有在指令级优化我们的实现，所以它总体上访问速度较慢，因为平均而言，每个项目有更多的候选内存位置;对于找不到匹配的查找，差异最大，因为这会导致搜索所有候选内存位置。

总之，我们的实验评估表明，有可能有一个NAT网络功能，既提供竞争力的性能，并正式验证。

7. 争论

开发和验证VigNAT是迈向经过验证的高性能NF更广泛目标的第一步。 Vigor的方法和原型有一些局限性，也为未来的研究提供了机会。在本节中，我们将介绍其中的一些。

活力不会产生不正确的证据，但由于模型无效，它可能无法证明一个给定的NF实际成立的属性。例如，在§3中，如果Vigor使用图4中的模型（b），那么它就不能证明给定的NF正确地实现了丢弃协议 - 即便是这种情况，因为模型太抽象了。因此，如果证明失败，并且所报告的失败原因不会导致NF开发人员在他们的代码中出现错误，那么给定的NF可能会执行libVig功能，这些功能不会被符号模型正确捕获; 在这种情况下，NF开发者可以向libVig开发者请求更详细的模型。

当前版本的Vigor无法验证并发代码。我们预计最大的挑战将是有用的并发数据结构的开发和验证。

我们还没有将Vigor应用于成熟的旧代码方面的经验。这样的软件经常有状态处理代码，所以重构它将所有的状态放在libVig数据结构中可能是有挑战性的。它还需要注释循环和提取循环不变量，但我们希望能够使用已知技术自动化这些任务[23,47]。

更一般地说，我们希望通过自动执行大部分任务来减少扩展libVig和使用Vigor所需的人力。（a）步骤3需要的许多引理是锅炉板，我们应该能够自动生成它们。（b）为了证明低级属性，使用简单的过度近似模型就足以使输出不受约束，并且这样的模型可以自动生成。我们还可以利用从痕迹中学习不变量的技术[13,45]来完善符号模型或为libVig合同生成初始草稿。（c）验证libVig的许多努力都是为了弥补VeriFast自己无法实现的逻辑跳跃而写入中间引理。使用证明助手或更强大的定理证明可以减少这种努力[4,12]。（d）生成指定标准的正式合同（例如RFC中所描述的）将始终需要手动工作;然而，标准通常具有适合于自然语言处理的结构，所以我们也许可以采用自动化技术[37]生成第一批草稿，然后由人类来完善。

8. 相关工作

如§2所述，我们在VigNAT上的工作属于NF验证领域，在更广泛的“数据平面验证。

与我们最接近的工作是Dobrescu et al。 [19]，其中核实了点击[35]中包括的NF，包括一个NAT。他们证明了这些NF的碰撞自由度和有限执行的低级属性。他们的方法依赖于单个Click元素的详尽的符号执行以及由此产生的分析的按需组合，以推断Click管道。和Vigor一样，他们的方法把所有的状态都放在特殊的数据结构中，但是它并没有对数据结构本身进行验证，也没有对NF进行正确的使用。正是由于这个原因，Dobrescu等人的工作无法证明语义属性 - 向前迈出的一步，使得这样的证明是我们在这里描述的“懒惰的证明”技术。

正交于NF验证是我们所说的网络验证：验证建模网络设备组合的网络属性（可达性，循环等）。在这方面有许多先前的工作[24,25,30-32,38,39,46,52,55,59]。

Stoenescu等人 [55]注重网络验证，但是依赖于比这个领域的其他工作更详细的NF模型，并且测试他们的模型以忠实于相应的NF实现。活力也依赖于模

型（不是整个NF，而是状态访问函数），但它不依赖于测试来获得对模型忠实度的信任。相反，Vigor正式验证了模型对于证明是有效的，这意味着用相应的实现替换模型保留了证据，模仿§5.4中的假设。

我们之前的很多应用验证技术来联网和分布式系统。我们共享工具和技术，这些工作是象征性的执行，正式的合同，证明检查，但是对代码的不同部分使用不同的验证技术，结合结果通过懒惰的证据，是新颖的。 Musuvathi等人 [41]测试了Linux TCP实现是否符合正式规范。主教等。 [3]测试了TCP / IP和套接字API的几个实现，以符合正式的规范。 Kuzniar等人 [36]测试了OpenFlow交换机与参考实现的互操作性。 Hawblitzel等人。 [26]验证了用Dafny编写的网络应用程序，这是一种内置验证支持的高级语言。 Beringer等人 [2]验证了OpenSSL的实现，证明了函数的正确性和密码性质。

在验证系统软件属性方面，已有一系列先前的工作取得重大进展。这些工作大部分也可以应用于NF验证。例如，seL4 [34]，CompCert [54]和FSCQ [11]展示了如何证明系统的语义属性。不幸的是，他们都需要使用高级（有时是深奥的）编程语言和深入的验证专业知识，我们认为这是一个很大的障碍。 Vigor背后的动机是为大多数（理想的是所有）NF开发人员提供网络功能的验证。

9. 结论

我们提出了一个NAT盒子，并附有一个技术和工具链，用于证明RFC 3022的形式解释是正确的。我们的主要贡献是利用NF结构的具体细节提出一种新的验证技术，将详尽的符号执行与基于分离逻辑的正式证明检查。这种被称为“懒惰证明”的技术可以可扩展地证明我们的NF的低级和语义特性。实验结果证明了我们的方法的实用性：经过验证的NAT盒子以及未经验证的DPDK NAT性能都优于标准的Linux NAT。我们希望我们的技术将最终推广到证明许多其他软件NF的属性，从而分摊了构建经过验证的NF数据结构库的繁琐工作。

致谢

我们感谢Jonas Fietz，Vova Kuznetsov，Christian Maciocco，Mia Primorac，Martin Vassor和Jonas Wagner进行了深入的技术讨论，并感谢EPFL网络架构实

验室和可靠系统实验室的成员提供了宝贵的反馈。感谢我们的牧羊人， Arjun Guha和匿名审稿人的评论和指导。这项工作得到瑞士国家科学基金会启动资助和英特尔资助

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