DNS形式化验证技术概述

2024年5月30日15:30:28评论7 views字数 4827阅读16分5秒阅读模式

摘要

域名系统（DNS）是互联网中至关重要的基础设施，其作用是将用户可读的域名转换为对应的IP地址。然而，随着互联网的不断发展，DNS系统变得复杂且庞大。确保DNS服务的正确性和可靠性至关重要，因为任何DNS故障可能导致互联网用户无法访问网站、服务中断，甚至可能造成大规模的经济和安全问题。传统的实时监控和语法检查等方法在确保DNS服务稳定性方面取得了一定进展，但无法全面分析DNS配置中的错误。

近年来，研究人员通过形式化验证等新兴方法在DNS分析配置中取得了重大突破。例如，Groot利用静态分析技术对DNS配置文件进行验证，能够主动检测常见的DNS错误。然而，Groot的集中化架构面临可扩展性问题，分布式验证框架Octopus通过分布式分析让每个权威域名服务器单独关注其区域文件，解决了可扩展性的问题。此外基于Maude的形式框架提供了用于端到端名称解析的形式化语义，发现DoS攻击的自动化工具；DNS-V框架则是通过分层验证原则和摘要化的方法对模块进行全路径符号执行，提高了验证过程的效率和可靠性。

背景

域名系统（DNS）是互联网中的分布式命名系统，它作为互联网的“电话簿”，将用户友好的域名转换为用于网络通信的IP地址。互联网连通的是全球资源，单一的域名服务器不足以支撑全部的地址转换操作，因此全球有多套域名服务器相互配合使用。早在1983年互联网就开始采用层次树状结构的命名方法，并使用分布式的域名系统进行解析操作。然而，随着互联网的增长和演变，DNS系统也变得越来越复杂和庞大。如果发生DNS错误，用户将无法正确解析域名，导致无法访问网站或受到访问延迟的影响。此外，DNS错误还可能导致用户被重定向到恶意网站或受到网络钓鱼等安全攻击。对于企业而言，DNS错误可能会对其业务造成经济等方面的损失。2023年，由于Microsoft错误配置域的DNS SPF记录，全球范围内的Hotmail用户在发送电子邮件时遇到问题。2021年6月8日，Fastly的服务中断事件中，由于错误的DNS配置，全球大量知名网站遭遇宕机，包括纽约时报、BBC和Reddit等，宕机时间持续近1个小时，仅亚马逊就损失了约3400万美元的销售额。同样，Microsoft Azure在2021年3月的服务中断，也与DNS配置错误有关，严重影响了用户和企业的数据和应用程序。因此，研究和开发有效的方法来验证DNS配置和确保DNS服务的正确性和可靠性具有重要意义。

研究现状

传统技术

传统技术主要集中在实时监控、黑盒测试和语法检查等方面。运营商通常会通过人工审查和验证DNS配置文件，以确保其符合最佳实践和业务需求。手动审查在DNS配置过程中扮演着重要角色。例如Akamai的Edge DNS[1]是一种全球分布式DNS服务，旨在提高DNS查询的性能和可靠性。作为行业领先的CDN（内容分发网络）提供商，Akamai的Edge DNS提供了高可用性和低延迟的DNS查询响应。然而它具有传统手动审查耗时、易错、可扩展性差的问题。

实时测试和监控的方法可以通过供应商提供的服务（如ThousandEyes[2]和CheckHost[3]）或研究工具监控正在发生的问题。

一些工具，如Microsoft的DNSlint[4]，专门用于检查DNS配置文件中的语法错误和违反最佳实践的地方。这些工具在发现常见的配置错误方面非常有效，但它们无法进行更深入的语义分析，无法验证查询是否会解析为NXDOMAIN等错误。

然而，这些方法对DNS配置缺乏直接了解，无法全面探索可能的DNS查询空间，也无法在运行前得知正确性，无法提供强有力的正确性保证。针对这些问题，人们希望判定DNS返回的结果是否满足预设的要求，DNS配置验证可以通过提前分析zonefile的配置，推断出所有可能的行为，然后将行为与要求进行比较，以实现在部署前的提前验证。为此，下面将介绍DNS验证技术。

DNS验证技术

源代码的形式验证是一种众所周知的方法论，可保证没有错误。特别是，验证系统的功能正确性涉及定义一个正式规范，描述该系统的预期行为，然后使用验证器严格检查源代码中的每一个可能执行路径是否符合该规范。网络路由验证也已经发展了很长一段时间，但是针对DNS验证还较少。

集中式DNS验证 [SIGCOMM’21]

新兴的DNS验证方法旨在解决传统方法的局限性，这种方法与现有的黑盒测试形成互补，能够更全面地探索可能的DNS查询空间。随着形式化方法在网络验证中的应用，出现了Groot[5]，是第一个DNS验证工具。这样的工具开始专注于通过验证一组区域文件来形式化定义DNS系统。它会检查DNS区域文件是否符合指定的属性，验证这些属性是否对所有潜在的DNS查询都成立，如果不成立，则提供一个反例。

尽管Groot在DNS配置验证方面取得了先进的进展，但其采用的集中化架构面临显著的可扩展性问题，以Groot为例，验证过程需要大约100秒才能处理一百万个区域文件。数百万个聚合的区域文件给DNS验证过程中的计算和通信带来了巨大的开销。这暴露了性能瓶颈，特别是在大规模网络中。此外，集中化架构通常不支持增量验证，这意味着每次验证都需要从头开始，增加了验证的时间和资源消耗。

分布式DNS验证 [APNET’24]

可扩展的DNS配置验证是现实世界中的一个关键挑战。集中化架构导致验证器成为性能瓶颈，因为它需要处理所有区域文件的验证。受到分布式数据平面验证的启发，厦门大学SNGroup提出了分布式验证框架Octopus，以应对这些挑战。Octopus旨在以高效的方式应对现实世界中大规模网络中的DNS配置验证。分布式分析让每个权威域名服务器单独关注其区域文件，得到的本地等价类（Local equivalence class）可以更深入地了解域的行为，其对比Groot的全局等价类的数量有很大的减少。通过符号执行技术从上到下覆盖所有可能的查询场景，并对查询过程进行分析，确保验证过程的全面性。总体而言，该方法提高了DNS配置验证的效率和可靠性，解决了传统集中化验证的性能瓶颈，提供了一种创新的DNS验证解决方案。可扩展的DNS验证工具不仅可以快速检测大型网络中的DNS配置错误，未来还可以支持诸如实时配置文件验证，增量验证等服务。

发现攻击的自动化验证工具[SIGCOMM’23]

由于DNS协议规范的模糊性和极端复杂性，以及迅速发展的互联网基础设施。为了对抗破坏和修复循环，以改善DNS基础设施，研究[6]提出了一种基于Maude的形式框架，构建了第一个端到端名称解析的形式化语义，一个用于正式分析定性和定量属性的组件集合，以及一个用于发现DoS攻击的自动化工具，成功应用于分布式和联网系统。框架的核心是目前最完整的DNS语义模型，捕捉了端到端名称解析的所有基本方面。该框架还集成了一个工具包，用于不同形式分析任务，包括模拟、时间模型检查和统计验证。通过这个框架，作者发现了现有的攻击并识别出了多种新攻击，可以实现较大的放大效果，并在流行的DNS实现中验证了这些攻击。这些实现的测量结果与模型预测一致，证明了框架的准确性和预测能力。

分层验证 [SOSP’23]

一般来说，自动化验证的关键思想基于分层验证原则。然而，正在生产中的DNS权威引擎缺乏模块化，尤其是由于接口不清晰和数据结构封装不良，使得分层验证难以应用。为了解决这个挑战，该DNS-V[7]框架基于分层验证原则，采用摘要化的方法对模块进行全路径符号执行，并累积路径条件和计算效果，将模块的行为以抽象形式表示为输入-效果对的集合。这种方法将系统分解为一组层。每一层将其源代码的所有行为封装到一个抽象规范中，并证明调用这个规范等同于调用相应的源代码。通过这种方式，每一层内的源代码可以独立验证，因为它只依赖于较低层功能的抽象规范。此外，DNS-V在发现和防止生产环境中的关键错误方面取得了显著成功，大大减少了生产故障和业务损失。该研究在阿里巴巴云运营的高可用性和可扩展性的DNS服务上进行实践，为数十亿的记录和1012次查询提供服务。

总结

综上所述，DNS验证是确保DNS服务正确性和可靠性的关键步骤。结合现有技术和新兴方法，运营商可以更好地发现和解决DNS系统中的问题，提高DNS服务的质量和稳定性，为用户提供更可靠的网络体验。

参考文献

[1] Akamai https://www.akamai.com/products/edge-dns

[2] ThousandEyes https://www.thousandeyes.com/resources/dns-webinar

[3] Check Host https://check-host.net/

[4] Lint https://learn.microsoft.com/en-US/previous-versions/troubleshoot/windows-server/description-dnslint-utility

[5] Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, and George Varghese. 2020. GRooT: Proactive Verification of DNS Configurations. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication. Association for Computing Machinery, New York, NY, USA, 310–328.

[6] Si Liu, Huayi Duan, Lukas Heimes, Marco Bearzi, Jodok Vieli, David Basin, and Adrian Perrig. 2023. A Formal Framework for End-to-End DNS Resolution. In Proceedings of the ACM SIGCOMM 2023 Conference (ACM SIGCOMM '23). Association for Computing Machinery, New York, NY, USA, 932–949.

[7] Naiqian Zheng, Mengqi Liu, Yuxing Xiang, Linjian Song, Dong Li, Feng Han, Nan Wang, Yong Ma, Zhuo Liang, Dennis Cai, Ennan Zhai, Xuanzhe Liu, and Xin Jin. 2023. Automated Verification of an In-Production DNS Authoritative Engine. In Proceedings of the 29th Symposium on Operating Systems Principles (SOSP '23). Association for Computing Machinery, New York, NY, USA, 80–95.