一个正式验证的NAT.docx

一个正式验证的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的正确性并不是