背景

域名系統（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驗證還較少。

1.集中式DNS驗證 [SIGCOMM’21]

新興的DNS驗證方法旨在解決傳統方法的局限性，這種方法與現有的黑盒測試形成互補，能夠更全面地探索可能的DNS查詢空間。隨著形式化方法在網絡驗證中的應用，出現了Groot[5]，是第一個DNS驗證工具。這樣的工具開始專注于通過驗證一組區域文件來形式化定義DNS系統。它會檢查DNS區域文件是否符合指定的屬性，驗證這些屬性是否對所有潛在的DNS查詢都成立，如果不成立，則提供一個反例。

盡管Groot在DNS配置驗證方面取得了先進的進展，但其采用的集中化架構面臨顯著的可擴展性問題，以Groot為例，驗證過程需要大約100秒才能處理一百萬個區域文件。數百萬個聚合的區域文件給DNS驗證過程中的計算和通信帶來了巨大的開銷。這暴露了性能瓶頸，特別是在大規模網絡中。此外，集中化架構通常不支持增量驗證，這意味著每次驗證都需要從頭開始，增加了驗證的時間和資源消耗。

2.分布式DNS驗證 [APNET’24]

可擴展的DNS配置驗證是現實世界中的一個關鍵挑戰。集中化架構導致驗證器成為性能瓶頸，因為它需要處理所有區域文件的驗證。受到分布式數據平面驗證的啟發，廈門大學SNGroup提出了分布式驗證框架Octopus，以應對這些挑戰。Octopus旨在以高效的方式應對現實世界中大規模網絡中的DNS配置驗證。分布式分析讓每個權威域名服務器單獨關注其區域文件，得到的本地等價類（Local equivalence class）可以更深入地了解域的行為，其對比Groot的全局等價類的數量有很大的減少。通過符號執行技術從上到下覆蓋所有可能的查詢場景，并對查詢過程進行分析，確保驗證過程的全面性。總體而言，該方法提高了DNS配置驗證的效率和可靠性，解決了傳統集中化驗證的性能瓶頸，提供了一種創新的DNS驗證解決方案。可擴展的DNS驗證工具不僅可以快速檢測大型網絡中的DNS配置錯誤，未來還可以支持諸如實時配置文件驗證，增量驗證等服務。

3.發現攻擊的自動化驗證工具[SIGCOMM’23]

由于DNS協議規范的模糊性和極端復雜性，以及迅速發展的互聯網基礎設施。為了對抗破壞和修復循環，以改善DNS基礎設施，研究[6]提出了一種基于Maude的形式框架，構建了第一個端到端名稱解析的形式化語義，一個用于正式分析定性和定量屬性的組件集合，以及一個用于發現DoS攻擊的自動化工具，成功應用于分布式和聯網系統。框架的核心是目前最完整的DNS語義模型，捕捉了端到端名稱解析的所有基本方面。該框架還集成了一個工具包，用于不同形式分析任務，包括模擬、時間模型檢查和統計驗證。通過這個框架，作者發現了現有的攻擊并識別出了多種新攻擊，可以實現較大的放大效果，并在流行的DNS實現中驗證了這些攻擊。這些實現的測量結果與模型預測一致，證明了框架的準確性和預測能力。

4.分層驗證 [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.