一个正式验证的NAT

一个正式验证的NAT

摘要

我们提出了一个用C语言编写的网络地址转换器（NAT），根据RFC 3022的规定，它在语义上是正确的，而且没有崩溃和内存安全。目前在网络验证方面还有很多工作，但是大多假设网络功能模型，并且证明了网络配置特有的属性，比如可达性和环路的缺失。我们的证明直接适用于网络功能的C代码，并且证明没有实现错误。之前的工作认为这是不可行的（即，用C语言来验证一个真正的，有状态的网络函数并不能扩展），但是我们证明了另外一点：NAT是最流行的网络功能之一，并且维持每个流状态正确更新和过期，这是验证挑战的典型来源。我们通过使用分离逻辑的符号执行和证明检查的新组合来解决可扩展性挑战; 这个组合很好地匹配了网络功能的典型结构。然后我们证明在这种情况下正式证明的正确性不会以牺牲性能为代价。 NAT代码，证明工具链和证明可以在[58]中找到。 CCS概念

网络→中间盒/网络设备; ?软件及其工程→正式软件验证;

关键词

网络功能验证; 懒惰证明; 符号执行

1 引言

这项工作是关于设计和实施被证明是安全和正确的软件网络功能（NF）。软件NF在低速环境中一直很受欢迎，例如家庭网关或无线接入点。最近，他们也出现在支持多Gbps线路速率的实验性IP路由器[20]和工业中间盒[8]中。此外，我们正在目睹虚拟网络功能的推进，这些虚拟网络功能可以在通用平台上按需部署，就像虚拟机部署在云端一样。

在网络验证方面有很多先前的工作，但据我们所知，没有任何理由说NF安全性和语义正确性。这些工作大部分依赖于与实现不同的NF的模型，因此它不

能推理后者（尽管我们应该注意到NF模型在推理网络配置方面是非常有效的[24,25,30-32,38 ，39,46,52,55,59]）。 Dobrescu等人是一个例外。 [19]介绍了软件数据平面验证的概念，并证明了用Click（即C ++）[35]编写的NF实现的低级属性。然而，这项工作无法证明有状态的NFs的语义正确性，因为它没有对状态进行推理。例如，尽管Dobrescu et al。为特定的NAT实现证明无崩溃和有界执行，由于没有办法推理流表的内容（例如，条目是否被正确添加或过期），所以它们不能证明它在语义上是正确的。

我们的贡献是一个NAT函数，用C语言编写，并使用DPDK数据包处理库[21]，我们证明它实现了RFC 3022 [53]中指定的语义，并且没有崩溃和内存安全。我们之所以选择这个特定的NF，是因为它可以说是最受欢迎的NF之一，但事实证明很难随时间推移：各种Cisco设备上的NAT可能会使用精心设计的输入来崩溃[17]或挂起[15]; Juniper的NAT [16]，Windows Server [40]的NAT和基于NetFilter的NAT都存在类似的问题[18]。而且，像许多NF一样，NAT保持每个流量状态都需要正确更新和过期，这是验证挑战的典型来源。

我们在C中实现了NAT，因为这是通常用于高性能数据包处理的语言，它可以从包含DPDK的丰富而稳定的生态系统中受益。鉴于我们无意中写了我们的NAT从头开始 - 而且我们的方法通常需要重构 - 我们确实考虑使用一种更易于验证的语言。然而，最终我们认为，NF开发者更容易采用我们的工具集，如果它允许他们使用熟悉的语言编写代码，并利用现有的专业知识和工具，即使他们必须遵循额外的约束（例如使用特定的库的数据结构）和注释他们的代码。最近的工作认为，验证一个真实的，有状态的NF的C实现是不可行的符号执行[55]，但我们表明，如果符号执行与其他验证技术相结合，可以完成。

我们的方法背后的基本原理是不同的验证技术最适合不同类型的代码。符号执行的美妙之处在于它的易用性：它能够自动进行代码分析，因此可以被开发人员使用，而不需要验证专业知识。符号执行的挑战是其臭名昭着的缺乏可扩展性：将其应用于真正的C代码通常导致路径爆炸[19,55]。通常导致无法管理的路径爆炸的真正的NF代码的一部分是操纵状态的部分。

因此，我们将NF代码分为两部分：（1）一个数据结构库，保持所有“困难”的状态，然后我们正式证明这是正确的 - 这需要时间和形式方法的专业知识，

但可以分摊，如果库在多个NF中重用; （2）使用库的无状态代码，我们使用符号执行自动并快速验证。挑战在于结合这两种验证技术的结果，为此我们开发了一种我们称之为“懒惰证明”的技术。一个懒惰的证明由分支证明构成，其中顶层证明进行假定较低层次的属性，后一种证明是后验证明。例如，符号执行需要使用必须正确的模型; 我们首先做符号执行，然后才自动验证模型的正确性。这种方法使我们可以避免必须证明我们的模型是普遍有效的 - 这是很难的 - 但是只能证明它们对于特定的NF和我们先前用符号执行来验证的特定属性是有效的，这很容易。

我们表明，正式验证我们的NAT的正确性并不是以性能为代价：与在DPDK上编写的未经验证的NAT相比，我们验证的NAT提供了类似的延迟，吞吐量损失小于10％。任何我们试验过的基于DPDK的NAT，无论是否验证，都明显优于流行的Linux内置NAT NetFilter。

本文的其余部分结构如下：在提供背景（§2）之后，我们用一个简单的例子（§3）来说明我们的方法，正式说明我们对NAT的证明（§4），描述我们的验证过程（§5），并报告我们的实验评估（§6）。然后我们讨论限制和未来的工作（§7），提出相关工作（§8），并结束（§9）。

2 背景

我们的工作属于“数据平面验证”的一般领域。这个术语通常用来表示两种不同类型的方法：一类工作作为一个大数据平面将网络设备的配置数据平面组合在一起网络和网络属性（可达性，循环等）的原因 - 我们称之为“网络验证”。正交类别是由于各个设备上运行的数据平面软件的属性以及软件属性（崩溃自由度，有限执行时间，内存安全等）的原因导致的，我们称之为“NF验证”。在网络验证中，目标是证明特定属性（例如，具有某些头部特征的分组将总是到达给定目的地）保持在特定网络中，特定NF以特定方式配置和连接。在NF验证中，目标是证明对于所有网络和工作负载，即不论NF如何配置或连接，都有一个特定属性（例如，在NF中不存在能够触发缓冲区溢出的输入分组）。在网络验证方面有很多工作[24,25,30,32,38,39,46,52,55,59]。相比之下，NF验证的工作就少得多[19]。网络验证的成功取决于NF验证的成功：网络验证依赖于组成网络的

NF的模型，无论这些模型是非正式地在RFC中捕获还是在SEFL模型中更正式地[55]，NICE模型[10 ]等。

然而，一个基于模型的数据包总是会到达目的地的证据被一个中间件的执行错误所取代，这个错误导致数据包被丢弃，违反了模型。有一些方法可以测试这样一个模型是否忠实于给定的实现[55]，但是在测试和验证之间存在很大的差距：一个成功测试的模型仍然可以表现出在实现中不会发生的行为，反之亦然。然而，NF验证可以确保部署在真实网络中的NF实现确实忠实于用于验证网络的模型。

我们的工作属于NF验证的范畴，旨在改善两个方面的技术水平：（1）验证高级语义属性，比如RFC的正确实现（;2）验证有状态的NF。 Dobrescu等人 [19]确实验证了一个有状态的NAT，但是只证明了低层次的属性（崩溃自由度和有界执行），因此没有遇到有状态NF的一些难度较大的挑战。我们的目标是解决这些挑战，同时不要让操作员承担写作或调整模型的重任，同时要把NF执行的性能保持在与未验证的NF相同的水平。在本文中，我们报告了我们在这项工作中的第一步：开发一个有状态的，性能良好的NF，除了没有崩溃，内存错误，泄漏之外，我们还证明可以实现从RFC 3022中了解的NAT语义和其他低级属性。

3 Vigor方法

为了验证我们的NAT，我们开发了一个名为Vigor的验证工具链，其中包括一个名为libVig的验证数据结构库。我们设想Vigor围绕三种不同的开发人员角色展开软件开发过程，其中包括：libVig开发人员，编写形式逻辑中指定公共标准的标准开发人员以及使用经过验证的NFs实现这些标准的NF开发人员。前两个角色需要软件验证和形式化方法方面的专业知识，但是他们的时间和精力投资可以在许多共享组件中分摊，并以不同的方式实现相同的标准。然而，担任后者角色的开发人员在验证方面几乎不需要任何专业知识。他们是Vigor的真正受益者，因为他们现在可以编写代码，证明它们相对容易。在本文中，作者承担了这三个角色，但是我们设想最终角色可以由不同的专业团队甚至不同的组织来承担。我们用一个简单的NF来说明Vigor的使用和功能，它实现了丢弃协议[48]：一个无限循环接收来自一个接口的数据包，丢弃发送到端口9的数据包，并通过另一个接口转发剩下的数据。

代码。NF开发人员还编写了两个额外的东西来编写标准代码：她注释循环并将状态封装在Vigor可以推理的libVig数据结构中。图1显示了我们验证的实现。它包含一个带注释的事件循环（1.6版的VIGOR_LOOP）和一个用于吸收突发的环形缓冲区（1.4版的r），通过四次调用（ll.9,11,12,13）来访问突发。网络交互通过三个功能发生：接收（l.10）非阻塞地读取一个入站包，并将其存储在输出参数中，返回成功或失败; can_send（l.12）检查是否可以发送新的数据包; 并发送（l.14）发送其自变量指向的数据包。

图1 丢弃协议的精确实施

循环不变量。我们的验证过程需要循环不变式来推断循环的影响。目前，NF开发人员以形式逻辑（图2,11.1-5）和C（11.7-9）手动写入这些不变量。在将来的工作中，我们希望能够使用现有的技术从代码中自动提取它们[23,47]，或者至少自动地帮助NF开发者制定它们。

图2 图1中循环保留的不变量

?packetp∈rinдr，packet_constraints（p）== true

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