主要观点：Cloudflare 过去一年开始正式验证内部 DNS 寻址行为的正确性，通过验证服务器执行的程序来确保 DNS 寻址行为的准确性，其验证器已投入生产，名为 Topaz，本文介绍了 Topaz 的工作原理、技术细节及相关权衡。
关键信息：

• Cloudflare 为每个代理域的 DNS 查询确定返回的 IP 地址，可根据不同业务目标选择，如应对攻击、测试新功能等。
• Topaz 程序由匹配函数、响应函数和配置组成，用于编码 DNS 业务目标，程序以 YAML 形式存储在版本控制文件中。
• Topaz 程序在热路径上执行，控制平面验证、分发程序，服务器检测变化并更新程序列表，名称服务器接收查询后转发给 Topaz 服务，执行匹配函数并返回 IP 地址。
• 程序分发前进行正式验证，检查程序的可满足性、可达性和冲突，确保程序无错误且不冲突，还新增了语义差异功能帮助理解程序变化的影响。
• 验证器基于 Rosette 实现，通过 SMT 求解器检查所有可能的 DNS 查询是否满足属性，但存在维护成本、函数限制和验证速度等问题。
  重要细节：
• Topaz 程序的配置中，绑定了各种名称到具体值，如 IP 地址、TTL 等，匹配函数根据 DNS 查询元数据判断是否执行，响应函数指定返回的 IP 地址和 TTL。
• 验证器检查程序的可满足性，确保存在使匹配函数返回 true 的 DNS 查询；检查可达性，确保给定前面的程序存在使匹配函数返回 true 的 DNS 查询；检查冲突，防止两个程序在相同查询上都匹配。
• Rosette 将所需属性转换为一阶逻辑公式，通过 SMT 求解器找到使公式成立的 DNS 查询参数值，将其转换为 Racket 数据结构。
• 验证器的维护成本在于模型检查器的解释器需与主解释器保持同步，且函数需与形式验证兼容，限制了可验证的函数类型，如不支持处理字符串的复杂操作，但支持简单的字符串操作。
• 验证速度方面，目前验证 7 个程序约需 6 秒，验证 50 个程序约需 300 秒，正在研究优化以减少时间。Topaz 的验证器从研究项目部署到生产，可确保 DNS 行为的准确性，文中还介绍了 Cloudflare 的其他服务及获取相关信息的途径。