Arjun Guha：验证系统配置

我是 UMass Amherst 的计算机科学教授 Arjun Guha。我的团队将编程语言和验证技术用于复杂的系统问题。今天我将重点讨论 Puppet，以及我们希望系统配置具备哪些属性。

搭建一台 Web 服务器需要安装软件、编辑配置、重启服务并测试。在许多机器上重复这些步骤很困难，尤其是系统担任不同角色或运行不同操作系统时。配置错误也曾造成严重的服务中断。

配置管理语言旨在解决这个问题。Puppet 采用客户端—服务器架构：主服务器上的配置会应用到运行代理的机器上。我将重点讨论配置语言，而不是部署架构。

一个小型清单可以创建 authorized-keys 文件，并指定所有权、权限、父目录行为，以及是否替换或备份已有内容。Puppet 还提供专门的 SSH authorized-key 资源。这些资源描述机器的期望状态，同时隐藏许多底层操作。

Puppet 常被称为声明式语言：它描述要达到什么目标，而不是如何执行的每个步骤。我更愿意问，我们可以推理哪些属性。两个期望的属性是确定性和幂等性，但它们都不能替代配置测试。

确定性意味着同一初始状态应产生相同结果，而不受资源顺序选择的影响。幂等性意味着再次应用配置不会改变结果状态。Puppet 文档推崇这些想法，但单个清单仍可能违反它们。

考虑一个清单：它创建用户、在该用户的主目录中创建 vimrc 文件，并安装 Vim 软件包。如果没有指定依赖，文件可能在用户创建之前创建而失败。Puppet 有排序规则，但与其他模块组合时可能暴露不同顺序；依赖某个偶然的顺序很脆弱。

第二个例子安装 Go 并移除 Perl。在例子所用的 Ubuntu 版本中，Go 编译器依赖 Perl。根据执行顺序，安装和移除可能互相抵消；反复应用清单可能使系统在不同状态之间切换。

为什么不强制使用一个全局顺序？即使固定顺序产生可重现的错误，它也无法解决彼此冲突的意图。它还可能损害模块化：两个独立编写的模块如果为共享资源选择相反顺序，就可能形成依赖环，无法一起安装。

一个简单的不具幂等性的清单先将文件二复制到文件一，然后删除文件二。第一次运行成功，第二次却因输入已被删除而失败。我们希望工具识别这类失败，而不是假设声明式语言会保证这些属性。

分析很难，因为 Puppet 有许多内置和自定义资源类型，它们对系统状态的影响可能相互作用。语言本身也有复杂特性。我们的第一步通过 Datalog 将 Puppet 转换为原子资源和依赖关系构成的图，把语言特定细节与后续推理分开。

在真实机器或容器上尝试每一种可能的安装顺序很快就变得难以处理。即使清单固定，与其他模块组合时也可能暴露数量呈指数增长的有效顺序。因此我们转向静态分析。

下一步将每种资源映射为一种小型命令式建模语言中的程序，包含文件系统测试和更新。文件资源可能删除并重新创建文件；如果禁用 replace，则可能保留已有文件。这些是资源行为的模型，并非对底层 Ruby 实现的分析。

对于软件包，系统在容器中运行 repoquery 或 apt-file 等工具，获取软件包创建的文件，再对这些影响建模。该抽象可能产生误报，也不覆盖安装后脚本。演讲时团队已为约 25 种常见资源类型建模，主要针对 Linux。

建模后的资源是一个函数，将输入文件系统映射到输出状态或错误。部分有序的资源图对于同一个输入可能产生多个输出。确定性要求每个输入的结果集合恰好只有一个元素；该元素也可以是错误。

我们在 Z3 中编码模型语义。一个反例由一个输入状态和两次产生不同结果的允许执行组成。如果求解器找不到这样的例证，就在该模型和所支持特性的范围内确立了确定性。

朴素表述的规模非常大：可能的文件系统实际上无限，每个状态可能很大，编码所有资源交互可能产生指数级大小的公式。要让问题切实可处理，必须先进行归约。

偏序归约利用可交换性。如果两个操作以任一顺序执行都总是产生相同结果，我们只需考虑一种顺序。传统的读写集合检查对软件包过于保守，因为许多软件包都可能创建相同的父目录。

领域特定检查还追踪资源创建的目录。它可以证明，尽管某些操作会建立相同目录，它们仍不会互相干扰。工具在构造公式时使用这些信息，避免生成指数级对象，而不是先生成再剪枝。

这里展示的分析不对权限和模式建模，因此基准结果依赖这一抽象。讲者指出，权限对其他问题可能很重要，纳入权限也可能使推理变慢。

第二个挑战是每个状态的大小。一个软件包可能创建数百或数千个文件，但大多数不会与其他资源交互。我们可以移除模型中那些与非确定性问题相关的所有操作都可交换的部分。

例如，安装 Apache 并单独创建其配置时，如果缺少依赖，二者可能冲突。分析器保留会产生交互的配置路径，同时剪掉无关的软件包文件。同样，如果清单创建两个用户，但只涉及其中一人的主目录文件，也可以移除无关路径。

这并不只是全局丢弃每条只访问一次的路径。分析会推理资源的片段，以及能否在不改变比较结果的前提下，将它们交换到相关执行的末尾。只供可移除片段使用的路径不必出现在模型中。

有限状态抽象在空目录上有一个微妙的边界情况。只看清单中显式提到的路径可能遗漏差别：一个未提及的子项可以使目录变成非空。模型必须加入额外的代表性路径来保留这种区别。

在网页演示中，Rehearsal 分析用户和 vimrc 的例子，并报告它可能具有非确定性。工具提供了一段 Puppet 依赖代码；添加后，这个例子变得确定且具备幂等性。建议的修正仍需人工审查，因为让配置具有确定性不等于让它正确。

资源的解释由团队使用自己的建模语言编写。容器用于获取软件包文件列表，而不是在验证时执行每个建模资源。结果可以缓存，需要时再查询新的软件包。

对从 GitHub 收集的清单进行的基准测试表明归约很重要。有些案例在朴素模型下超时，但使用优化后约一秒半即可完成。一个例子中，相关建模文件数从约 1,500 个降到约 250 个。

模型追踪文件相等性、目录和空目录，但不详细检查任意文件内容。复制文件可以精确建模，而读取并转换文件部分内容的脚本超出了这种精度。权限和模式也没有纳入本次分析。

一旦确立确定性，就可以在模型范围内将清单视为从输入文件系统到输出文件系统的函数。这使其他检查更容易：幂等性要求应用函数两次与应用一次的结果相同，用户也可以表达前置条件或后置条件。

团队正在探索如何处理清单中嵌入的 shell 脚本。一个例子是需要以非交互方式接受许可协议的安装程序。当前抽象通常不分析这类脚本，而讲者估计许多公开清单都使用它们。

所提出的方法是在容器中运行脚本并扰动输入，从输入输出样例中学习有限状态模型。为清单中使用特定参数的命令建模，比为通用工具的所有可能调用建模更窄。这项工作仍在进行。

另一个研究方向是配置修复。用户可能部署了包含错误设置的 vimrc，通过 shell 命令修复运行中的机器，然后还需要将同样的修正应用回清单。团队正在探索如何根据原始配置和观察到的修改，合成更新后的配置。

同一组修改可能对应多个一致的配置更新，因此如何选择并呈现备选方案也是问题的一部分。目标是缩短编辑、部署和调试周期，同时让配置与修复后的系统保持一致。