一个正式验证的NAT(5)

packet_is_sent和sent_packet，以在send（）调用之后立即捕获外部可见的效果。然后它将NF规范（语义属性）插入到ll上的跟踪中。24-26：

Vigor在每次循环迭代之后验证NF规格。

一旦证明检查器完成了从验证器接收到的所有验证任务，我们就可以证明验证器编写的跟踪属性适用于所有可能的无状态代码执行。 Vigor证明VigNAT通过将§4.1的属性编织到符号轨迹中来满足NAT规范，类似于ll。跟踪验证是高度可并行化的：验证由无状态VigNAT的108个执行路径产生的所有431个跟踪在单个内核上需要38分钟，在4个内核机器上需要11分钟。如后面将要提到的，这个验证时间不仅包括P1，还包括P4和P5。

5.2.3 验证libVig符号模型。我们说一个符号模型是有效的，如果它所展示的行为与正式接口契约所捕获的libVig实现的行为是无法区分的。在ESE期间没有观察到的模型的任何行为都与这个特定证明的有效性无关。这就是我们懒惰的证明技术背后的洞察力：模型是否是普遍有效的并不重要，而重要的是在符号执行过程中使用的模型的部分是否有效 - 这是一个比通用有效性更弱的属性，但对我们的目的来说就足够了。符号追踪记录了如何使用模型的所有必要信息。

证明libVig模型与libVig接口契约一致的技术类似于我们用来证明NAT语义的技术。只有这一次，验证器不会将NAT前后条件编入到跟踪中，而是在给定跟踪路径约束的断言中编织。然后它要求证明检查器验证断言是否仅仅依赖于libVig函数的后置条件。如果验证成功，则意味着在每次调用libVig模型之后，结果将覆盖libVig接口协议规定的所有可能的结果。

libVig模型可以是过度近似，近似或两者兼而有之。验证者要回答的问题是，对于特定的NF和属性，模型是否足够精确。如果一个模型对于期望的证明“太低估”，它将导致验证阶段失败，因为它的狭义行为不包括合同允许的行为范围。如果目标证明“太过于近似”，它将导致彻底的符号执行（ESE）或验证失败 - 如果模型的行为过于笼统，并且无法验证低级属性，后者如果低级属性验证，但循环不变或高级语义属性被违反。当ESE完成时，只要模型有效，我们就可以证明低级属性成立。 ESE失败意味着要么是违反低级财产，要么libVig提供的模式不合适 - Vigor尽力帮助开发人员区分这两者，但仍有改进的空间。不管是哪种情况，都回到了制图板：NF开发者需要修复bug，否则Vigor开发者需要改变

模型。

Vigor还使用我们写的DPDK数据包处理框架的发送，接收和免费通话模式。我们没有正式验证这个模型，尽管没有根本原因不能做到。我们使其成为Vigor可信计算基础的一部分（§5.4）。

5.2.4 证明VigNAT正确使用libVig。在上一节的证明中有一个警告：如果调用libVig方法实现并且相应的前提条件不成立，那么该方法的行为是未定义的。例如，当合约说它必须是nonnull时传递一个空参数可能会导致实现崩溃，行为不正确或行为正确。因此，在确认模型行为的同时，Vigor也必须验证调用者对接口契约的行为。

证明VigNAT无状态代码使用与libVig接口契约一致的libVig数据结构的方法与上述相同，除了Validator在包含在libVig接口契约中的前置条件中编织。实际上，Validator在NAT前后条件和libVig前后条件中编织一次，并且为每个迹线生成单个验证任务，同时验证属性P1，P4和P5。

验证libVig前提条件中最棘手的部分是跟踪整个接口的内存所有权。由libVig方法（作为返回值或通过输出参数）返回的指针引用由libVig首先拥有的内存; 返回后，所有权转移给主叫方。在使用/修改指针后，NF代码调用另一个函数将所有权返回给libVig。

作为参数传递给libVig方法的指针可能是libVig数据结构的地址（相当于C ++ / Java中的这个指针或者Python中的自引用）。这种类型的指针对于无状态代码仍然是不透明的：它可以被复制，赋值和比较以获得相等性，但不能被解除引用。验证器和证明检查器不需要看这样的指针指向的内存，而只是跟踪别名信息。指向的内存一直由libVig拥有。 Vigor在符号执行过程中验证了无状态代码服从这个指针规则，使用我们的SEE除了在libVig调用之间启用/禁用指针的引用。

用作输出参数的指针指向调用者期望libVig返回结果被写入的位置。在这种情况下，指向内存由调用代码拥有。验证器和证明检查器通过将其包含在调用之前的函数输入集中以及调用之后的函数输出集中来跟踪指向内存的演变。输出指针的特殊情况是指向数据结构分配函数中出现的库数据结构（例如X ** p）的双指针。 VigNAT代码拥有pointee * p，所以Validator会跟踪它，但是pointee ** p的指针是一个库数据结构，因此内存由库所有，所以不需要跟踪它。目前Vigor

不支持双重或更深的指针的其他情况。

活力也检查内存泄漏。即使无状态的代码不能动态地分配内存，但是如果使用libVig不正确，例如忘记调用释放方法，泄漏也是可能的。不像简单的低级属性（如整数溢出），可以说是一个简单的断言，没有内存泄漏是一个全局属性。因此，Vigor必须跟踪内存所有权，并在执行结束之前验证所有权是否已正确返回到libVig。例如，这个工具在VigNAT中发现了一个意外的内存泄漏，我们无法释放与DPDK返回的数据包相对应的DPDK内存，从而违反了DPDK接口协议。

5.3 活跃工作流

上面描述的Vigor工作流程可以概括如下：我们将NAT NF分成无状态和有状态的部分，后者包含在libVig库中。然后我们使用形式定理证明来验证在libVig中实现的数据结构的P3正确性。我们使用详尽的符号执行（ESE）和KLEE的修改版本[9]来探索无状态部分中的所有路径（使用数据结构的符号模型），并验证P2-低级属性，如碰撞自由度，内存安全性，没有溢出 - 以及VigNAT严格使用指针。这个步骤是在无状态代码根据它们的接口契约（P4）使用libVig数据类型并且libVig模型忠实于在ESE期间探索的特定执行路径的libVig接口契约（P5）的假设下进行的。这两个假设我们都使用了我们的Vigor Validator和VeriFast校验器[28]来验证后验。最后，我们使用相同的工具组合来证明VigNAT的语义属性（P1），即它符合RFC 3022的形式化[53]。 P1∧P2∧P3∧P4∧P5一起正式证明了VigNAT的正确性，在下一节描述的假设下。

5.4 假设

Vigor验证NF的可信计算基础包括Vigor工具链（Clang LLVM编译器，VeriFast，KLEE和我们自己的Validator）以及NF运行的环境（DPDK，设备驱动程序，操作系统内核，BIOS和硬件）。我们假设编译器实现了Vigor使用的相同的语言语义（例如，C原语类型的相同字节长度）。我们为三个DPDK函数和系统时间编写了符号模型，在撰写本文时我们还没有验证。他们很小（约400 LOC），所以我们手工说服他们，他们是正确的过度近似。人们可以设想采用一

个具有正式规范的环境，如seL4 [34]，其中有可能证明这些模型的有效性。

6. 性能评估

在之前的章节中，我们证明了我们如何验证VigNAT的正确性，现在我们证明这种形式验证并不是以性能为代价的：与在DPDK上编写的未经验证的NAT相比，我们验证的NAT提供了类似的延迟和低于10％的吞吐量罚款。我们将我们的评估重点放在比较VigNAT（图中标记为NAT）和其他三个NF：

(a) 在DPDK之上执行无操作转发; 它接收一个端口上的流量，并将其转发

出另一个端口，而无需其他处理。它作为一个基准，显示了DPDK NF可以在我们的实验环境中实现的最佳吞吐量和延迟。

(b) 未验证的NAT也在DPDK之上实现; 它实现与VigNAT相同的RFC，

并支持相同数量的流（65,535），但使用DPDK分发附带的散列表。它是由一位经验丰富的软件开发人员撰写的，几乎没有验证专业知识，与编写和验证VigNAT的人不同。它用来比较VigNAT和没有用验证书写的NAT。

(c) Linux的NAT是NetFilter [5]，用简单的伪装规则建立并调整性能[29]。

我们预计它会比另外两个慢得多，因为它不会从DPDK的优化数据包接收和传输中受益。我们用它来表明，VigNAT的性能明显好于当前在基于Linux的家庭和小型企业路由器中使用的典型NAT，正如人们所期望的那样，DPDK NAT。

我们使用RFC 2544 [7]建议的图11所示的测试平台。测试机和Middlebox机器是相同的，具有3.30 GHz的Intel Xeon E5-2667 v2处理器，32 GB的DRAM和82599ES 10 Gbps DPDK兼容的NIC。 Middlebox机器运行上面提到的四个NF之一（我们使用一个核心）。测试机运行MoonGen [22]产生流量并测量数据包丢失，吞吐量和延迟; 对于延迟测量，我们依靠硬件时间戳来获得更好的准确性[49]。我们在Ubuntu Linux上使用DPDK v.16.07，内核为3.13.0-119-generic。

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