一个正式验证的NAT(4)

实现：在Vigor中，我们使用VeriFast验证检查器[28]，它用于C程序注释的前提条件和后置条件写在分离逻辑[51]。注释代码并不是一件容易的事，特别是对于非专家来说。然而，分离逻辑相对友好：它是为使用共享可变数据结构的低级命令式程序设计的经典Hoare逻辑的扩展。它有一个很好的内存所有权的概念，可以很容易地通过指针来表示所有权的转移。分离逻辑支持本地推理[44]，其中规范和方法的证明只涉及该方法使用的内存，而不是整个全局状态。

libVig包含C的2.2 KLOC，前后条件和附带定义的4K行，以及21.8K行证明代码（内联注释）。写作证明的人力约为2个人月。 VeriFast在不到1分钟的时间内验证证明。

5.1.4 libVig数据类型的符号模型。符号执行[6,9,14,27,33,50]是我们在§5.2.1中用于验证VigNAT的低级属性（P2）的方法。这种方法需要一个符号执行引擎以符号而不是具体的值执行NF。符号值同时表示多个可能的值（例如，无约束的符号分组报头表示所有可能的分组报头）。赋值语句是它们的符号参数的函数，而条件语句将执行拆分成两条路径，每条路径的符号状态相应地受到分支条件的约束。

当象征性地执行调用libVig的VigNAT无状态代码时，我们不希望象征性地执行libVig实现，因为这会导致路径爆炸。因此，我们用一个符号模型来抽象libVig，模拟调用libVig的效果并以每个执行路径的方式跟踪副作用。符号模型与正式契约在两个方面有所不同：它是可执行代码，它可能是不完美的 - 它可能会错过libVig实现的一些可能的行为，或者展现永远不会发生的行为。

正如我们在下一节讨论的那样，写一个好的符号模型是困难的，我们的懒惰证明技术有助于解决这个挑战：它容忍符号模型中的缺陷，同时在形式上保证接受的缺陷不会影响整体证明的NF。

5.2 懒惰的证明

我们提出的懒惰证明技术将一个符号执行引擎（SEE）与一个证明检查器粘合在一起，以产生以前无法到达的NF属性的证据。再加上之前描述的有状态/无状态分离，这构成了我们如何验证VigNAT的基石。

主要思想是使用SEE枚举所有执行路径通过无状态的NF代码，并（a）记录每条路径的无状态代码如何与外部世界和libVig交互的符号轨迹; 和（b）验证P2（低级属性）在每条路径上都有效。验证器然后将符号轨迹（即，VigNAT无状态代码的所有可能的可观察行为的表示）转换成P4，P5以及最终P1（NAT语义）保持的机械可检验证明。

懒惰的证明不仅可以让我们为每个期望的财产使用正确的工具，而且还解决了建模的挑战：编写一个libVig的符号模型需要调和两个相互冲突的目标。一方面，模型必须移除足够的细节，即足够抽象以使符号执行在有用的时间内终止 - 毕竟，抽象是减少了符号探索的路径的数量。另一方面，模型必须足够详细以捕获足够的libVig行为，以便在被验证的属性的上下文中忠实于libVig实现。模型

的好坏直接取决于哪些细节与证明与非证明相关，哪些细节又取决于要证明的属性以及使用模型的代码。因此，设计好的模型通常是一个迭代过程，在经过多次尝试之后收敛到一个针对代码定制的良好模型和待验证的属性。花费时间证明模型的真实性（P5），然后才真正知道它们适合于证明P2是很浪费的。用懒惰的证明，现在我们可以首先尝试P2的证明，假设模型是OK的，如果模型确实有助于证明期望的性质，那么只有投资验证模型（P5）。从实际的角度来看，这种方法使得编写模型变得很便宜，因为我们不需要花时间去清理最后的错误。相反，我们依靠Vigor随着时间的推移来发现这些错误。

换句话说，懒惰的证据利用了这样一个事实：一个应用程序通常只使用其库所提供的语义的一个子集。因此，我们不是证明libVig模型准确地捕获了libVig的所有语义，而只是证明它对VigNAT使用的语义是如此。

我们现在描述P2低级属性（§5.2.1）的证明，Vigor验证器以及它如何使用符号轨迹来证明VigNAT语义的P1-正确性（§5.2.2），以及Validator如何验证正确性 libVig符号模型（§5.2.3）的正确性以及无状态代码（§5.2.4）如何使用libVig的正确性。

5.2.1 证明VigNAT满足低级属性。低级编码错误，如内存滥用，会导致程序崩溃或行为不正常，因此证明不存在这样的错误对于证明更高级别的语义属性至关重要。如§4.2所述，所需的低级属性是指缺少诸如缓冲区溢出/下溢，超出内存访问，双倍空闲，算术溢出/下溢等错误。

为了证明没有这样的错误，Vigor执行彻底的符号执行（ESE），使用SEE枚举所有执行路径通过NF的无状态部分。 SEE在条件语句中探索所有可行的分支，因此ESE是完全精确的：它只列举可行的路径，即存在一组输入的路径，使程序沿着该路径下来，并且不会错过任何可行的路径。低级属性被声明为assert，并且对于每个可行的执行路径，SEE象征性地引起是否存在可能违反断言的输入。为了使这种方法可行，Vigor首先用libVig模型调用libVig的所有调用;这将所有状态处理代码抽象出来，从而消除了导致路径爆炸的几乎所有构造，如松散约束的符号指针。接下来，通过用VIGOR_LOOP标记无限循环的环路保护并提供环路不变量，让SEE知道环路边界，以便SEE可以转换环路以避免不必要的环路展开（例如，通过havocing [1]）。这消除了VigNAT中路径爆炸的最后一个来源。

如果每个低级属性的断言在ESE期间的每条可行路径上都存在，那么我们就可以证明这个无状态代码没有低级错误，因为ESE会在没有列举这些输入的情况下对所有可能的输入进行解释。 libVig根据其接口契约（§5.1.3）行为的形式证明保证libVig也不存在低级别的错误，否则其证明将无法验证。这意味着所有的VigNAT代码都能满足低级属性。如果这不是无国籍的代码，而是一个有状态的程序，ESE可能不会完成。然而，在我们的例子中，SEE在不到1分钟的时间内通过VigNAT的无状态代码检查所有108条路径。

当然，这个证明提供了一些基本的假设，如编译器的正确性（更多在§5.4中），最重要的是假设libVig模型是正确的（P5），无状态代码正确使用VigNAT数据结构（P4）。验证这些假设后验需要一个验证器和符号轨迹，我们将在下一小节中介绍。

实现。在Vigor我们使用KLEE SEE [9]。它检查现成的几个低级属性，并且从LLVM的未定义行为消毒器中添加检查[42,43,57]。我们通过几种方式修改KLEE：首先，我们添加了循环不变支持，并且我们启用了KLEE来自动查找可能在循环内部改变的变量，并破坏它们[1]。 NF开发者仍然必须手动插入循环不变式的断言和假设，但是KLEE现在可以使用它们来避免列举不必要的路径。其次，我们通过提供允许libVig开发者启用/禁用libVig调用之间的指针的引用性的原语来添加动态指针访问控制。第三，我们增加了记录符号轨迹的能力，下面将会介绍。

5.2.2 证明VigNAT满足NAT RFC语义。我们把形式化的NAT语义看作是“跟踪属性”：给定一个NF与外部世界之间的交互作用的轨迹，那么对于一个正确的NAT NF产生的跟踪必须具备什么条件？更具体地说，NAT属性（在§4.1和图6中示出）是以数据包到达触发的动作的前置和后置条件的形式。前提条件（以抽象NAT状态加上传入数据包表示）选择应用哪个操作。相应的后置条件表明在动作完成之后必须保持抽象状态和潜在的外出分组。

为了验证所需的属性，Vigor从SEE收集每个探索执行路径的踪迹。此跟踪总结了VigNAT代码在符号执行过程中如何与（外部世界的）模型（无论是libVig库还是DPDK框架）进行交互。由于迹线具有相同的前缀，所以它们形成一个树--NF的执行树。在本节的上下文中，符号追踪是从执行树的根到树中的节点

的路径，无论是内部还是叶节点。换句话说，Vigor所考虑的一组符号轨迹由所有执行路径轨迹及其所有前缀组成。

每个跟踪都有两部分：在跟踪接口上创建的一系列调用，以及符号编程状态的一组约束。图9示出了使用环形数据结构的图1中的代码的轨迹的简单示例。这个跟踪中的七个调用是由图1中的8→9→12→13→14→16的执行引起的。loop_invariant_produce和loop_invariant_consume是指示循环迭代开始和结束的标记。在ring_pop_front调用中，包是指向弹出包的输出参数; 追踪记录了它的初始值和最终值。

约束部分显示了不同符号之间的关系。在这个简单的例子中，只有一个约束：y，9是在ring模型中应用packet_constraints（图2）的结果。初始值x是无约束的。

验证器现在获取每个跟踪，将要验证的属性编入其中，并将其转换为验证任务。这是一个C程序，包含来自跟踪的调用序列，丰富了用作参数和返回值的符号变量的元数据，以及描述跟踪中每个点上这些符号变量之间关系的约束。验证器还将引理插入到跟踪中，以帮助证明检查器。实质上，验证器将每个符号轨迹转换为迹线满足所需属性的证据。然后它将证明传递给证明检查器来验证它。

图10显示了图9的验证器变换版本。这七个调用现在在第6,8,10,12,15,18和22行。未初始化的arg1和arg2变量最初是无约束的符号。图9中记录的返回值约束转化为9,11和13行的@assume语句。图9中l.10的符号约束变成证明的l.17的@assume。这四个@assume语句构成了这个符号轨迹的先决条件。为了设置需要验证的后置条件，Validator在第19行和第20行初始化特殊句柄变量

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