一个正式验证的NAT(3)

表中存在具有数据包的流ID（1.20）的条目，则NAT转发数据包，根据数据包是否抵达内部或外部接口来修改其数据头; 否则，它丢弃数据包（1.39）。

我们写了一个正式的机器可读的NAT标准规范，按类似的方式组织起来。它将expire_flows，update_flow和forward合并为一个决策树。树包含图6所示条件（前置条件）的分支，如P .iface = internal，以及检查相应输出（后置条件）的断言，例如“packet P is 丢弃“或”S.dst_ip等于P .dst_ip“。前置条件和后置条件都写在分离逻辑中，作为抽象NAT状态和/或传入/传出数据包的谓词。决策树覆盖了每个前提条件的两个分支，因此它提供了在任何情况下NAT的行为的完整说明。我们正式验证了VigNAT的C实现实现了从图6导出的正式规范中的行为。

最后，由于VigNAT在libVig数据结构中保持其状态，我们也证明它正确地使用了这些数据结构（§5.2.4），即数据结构的前提条件是满足的。

4.2低级属性

除了NAT语义之外，我们还证明VigNAT没有下列不需要的行为：缓冲区溢出/下溢，无效的指针解除引用，未对齐的指针，超出范围的数组索引，访问非存取器所拥有的内存，使用经过免费的双倍空闲类型的转换，会溢出目标，被零除，有问题的位移和整数溢出/下溢。证明这些性质归结为证明了VigNAT代码中引入的一组表达式（无论是在KLEE符号执行引擎[9]中还是使用LLVM未定义的行为消毒器[42,43,57]）都能保持。

5设计和实施

在本节中，我们将介绍VigNAT的设计以及我们如何验证其属性以及一些与实现相关的亮点。完整的细节和源代码可以在[58]中找到。

虽然本文提出的工作的目标是专门建立一个正式验证的NAT，但是我们的更广泛的目标是找到一个实用的方法来验证任何有状态的NF，所以我们采取了比绝对必要的更为原则的方法。我们认为，实用性包括同时实现两个设计目标：竞争性表现和低验证工作。后者有三个组成部分：以可验证的方式编写代码，写出证明，并验证证明。 Vigor支持C语言，因此不会给编写NF代码带来不必要

的负担，所以我们专注于设计一种高效编写和验证现实NF的技术。与此任务相关的众所周知的验证方法包括整个程序定理证明（例如，seL4 [34]）或像符号执行的每个路径/每个状态的技术[19,55]。与前者一样，验证财产证明是相对较快的，但是写证明是一个缓慢的，往往是手动的工作。对于后者，由于路径爆炸[19,55]，验证真正的NF中的属性可能需要很长甚至是永久的，但是很容易自动化。为了验证一个有状态的NF，这两种方法都看起来不切实际。

在我们的方法中，我们将证明分解成几部分，并用适合于该部分的技术来证明每个部分; 在那之后，我们把证据拼在一起。我们假设大多数NFs是由许多NFs共同组成的一个部分（因此投入人工努力来证明其正确性是值得的），另一部分在每个NF中是不同的（因此验证应该是自动的）。我们也认为，随着时间的推移，NF将会聚合使用稳定的，通用的数据类型来封装NF状态，NF之间的差异将主要来源于它们的无状态代码如何使用这些数据类型。对于VigNAT，我们将所有的NF状态放在驻留在库中的数据结构中，并使用人工辅助的定理证明来验证这个库的正确性。然后我们使用符号执行来证明无状态代码的正确性。

图7 VigNAT正确性证明的结构。 Pi（X）<—Pj表示属性Pi的证明是由X完成的，假设

Pj成立

面临的挑战是如何将两种验证技术的结果联系在一起。我们开发了懒惰的证明，一种自动将符号执行与基于分离逻辑的证明检查器接口的方法。我们构建了一个实现这个技术的验证器，并将子证明一起粘贴到VigNAT实现NAT RFC的最终证明中[53]。

VigNAT证明由五个子证明组成，如图7所示。顶层证明目标P1是显示

VigNAT展示正确的NAT语义。 P1的证明假定了三件事：首先，代码必须在基本意义上正常工作，如不崩溃，没有溢出（P2）。其次，库数据结构的实现必须按照其接口契约（P3）中指定的那样工作，例如查找刚添加的流应返回该流。第三，NF的无状态部分必须以与它们的接口（P4）一致的方式来使用数据结构，例如，指向流表的指针不会被错误地作为指向流入口的指针传入。假定P2?P3 ?P4，验证器产生由证明检查器机械验证的P1证明。

这三个假设当然必须被证明。为了证明P2 - VigNAT满足低级属性 - Vigor象征性地执行无状态代码，并检查属性是否保留在每个执行路径上。为了扩大规模，我们采用了抽象符号模型的数据库结构。因此，P2的证明必须假设这些模型是正确的（P5），数据结构实现满足它们的接口（P3），并且无状态代码正确地使用有状态数据结构（P4）。如果这三个假设中的任何一个都不存在，则证明将不起作用。为了证明P3，我们使用相对直接的（但仍然乏味的）定理证明，库的实现满足定义它的接口的契约。

P4和P5的证明，我们发现了懒惰证明技术的第二个可扩展性好处：它不仅允许我们用不同的工具完成证明（从而允许我们为每个子证明使用任何工具提供最佳的效益比），但也使得有可能摆脱证明较弱的属性。例如，我们不是证明P5是普遍真实的，然后用这个证明来进一步证明P2，而是首先证明P2假设P5，之后只证明P5对于P2证明依赖于P5的具体方式成立。对于所有可能的用例，P5的用例特定证明比证明P5更容易。

我们现在描述Vigor的数据结构库及其正确性证明（§5.1），我们的“懒惰证明”技术及其用于验证VigNAT语义的正确性（§5.2），并总结了Vigor工作流程 5.3）以及我们方法的假设（§5.4）。

5.1 验证的NF数据类型库

VigNAT由无状态应用程序逻辑组成，这些应用程序逻辑处理由Vigor库（libVig）提供的数据结构中存储的状态，如散列表和数组。例如，在§3中，我们将传入数据包放入libVig的环形数据结构中。一般来说，无状态的NF代码应该没有任何动态分配的状态和复杂的数据结构。它可以保留基本的程序状态，如静态分配的标量变量以及标量结构。

处理明确的状态在必要的非类型安全程序的验证中是困难的，这主要是由于追踪内存所有权和类型信息以及解开指针别名的困难。例如，void *指针可以引用哪个内存的问题通常是不可判定的。功能性，类型安全的语言（Haskell，ML等）对于验证是有吸引力的，但是对于我们来说，支持C（初步证据[60]表明C在NF开发者中广泛流行）是最重要的，并且能够验证完全状态NF。我们通过将NF状态封装在libVig的接口之后，并且遵循规则使用指针来完成这两个任务。虽然这种方法与所有软件都不兼容，但我们相信这是NF的一个很好的选择。

除了NF的数据类型外，libVig还提供了一个正式的接口规范来定义这些数据类型的行为，同时也证明了libVig实现服从规范。为了实现无状态NF代码的符号执行，libVig还提供了其数据类型的符号模型。我们验证libVig一次，证明继承任何使用库的NF。

本小节详细介绍了libVig实现（§5.1.1），描述了我们使用抽象和契约来正式指定libVig的语义（§5.1.2），说明了我们如何证明实现满足其接口规范（§5.1.3），并提出了符号执行引擎使用的libVig数据结构（§5.1.4）的符号模型。

5.1.1libVig实现。竞争性能是一个重要的设计目标，libVig是优化性能的好地方。我们做出的关键设计决定是预先分配所有libVig的内存。虽然这缺乏在运行时动态分配的灵活性，但它提供了对内存布局的控制，使得控制高速缓存放置成为可能，并节省运行时内存管理开销。预分配的成本可以忽略不计（例如，在我们的实验中，VigNAT的峰值驻留集大小为27 MB），我们相信预分配完全符合真实NF的使用状态。在与Vigor的证明检查器进行验证方面，静态分配对于动态分配没有明显的好处，但对于其他检查器可能会这样做。

在撰写本文时，libVig提供了开发VigNAT所需的几个基本数据结构：流表，实现为双键哈希映射，网络流抽象，环形缓冲区，用于跟踪和过期流的expirator抽象，用于分组同质项目的分批器，用于跟踪分配端口的端口分配器，以及经典的哈希表，数组和向量。 libVig还提供nf_time抽象来访问系统时间和DPDK框架顶部的dpdk层。

5.1.2 使用抽象和契约来正式指定libVig语义。我们根据数据类型的方法操作的抽象状态来指定libVig数据类型的语义。这与我们在形式化NAT RFC（§4.1）中采用的方法是一样的。每种方法的先决条件和后置条件形成了定义每种

数据类型应该做什么的合同。

图8显示了libVig流程表的get方法的片段。前提条件是第3-6行，后面的条件是第7-14行。契约是为了验证者和证明检查者的消费，但是当模棱两可的自然语言或阅读源代码失败时它们也可以作为文档。

每个都需要先决条件说明要运行的函数的要求：它的参数和抽象状态之间的关系，或指针的内存所有权标记。每个确保后置条件指定方法完成后保留的内容：参数和返回值之间的关系，某个内存位置的更新值或内存所有权令牌。

我们对指针的使用采取了“卫生”策略：无状态代码可以在libVig接口上传递/接收指针，但是libVig数据结构对调用者来说仍然是不透明的。无状态代码可以复制指针，分配它们，比较它们是否相等，但不能对其进行解引用。 Vigor会自动检查无状态代码是否遵守这个规范（第5.2.4节）。

5.1.3 验证libVig的正确性（P3）。一旦接口的形式化完成，我们编写证明，即用断言，循环不变式等注释代码，并为证明的中间步骤定义引理。

证明检查器首先假定前提条件（ll.3-6），并在制定假设条件的同时逐步通过每个代码语句。当它遇到分支条件时，它探索两个分支。内联注释（第16-18,20-22,24,28-30行）帮助检查者了解抽象状态的转换，验证它们确实对应于具体机器状态的转换。在内存访问（1.19）上，校验检查器检查地址和内存所有权令牌的有效性。在方法调用（l.23）上，它检查被调用方法的先决条件，然后采用其后置条件，实质上用假设被调用者的后置条件来替换调用（分别验证后置条件是否成立每当被调用者返回时）。当到达返回点时（l.31），证明检查员检查后置条件。

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