我們一起聊聊DNS形式化驗(yàn)證技術(shù)
背景
域名系統(tǒng)(DNS)是互聯(lián)網(wǎng)中的分布式命名系統(tǒng),它作為互聯(lián)網(wǎng)的“電話簿”,將用戶友好的域名轉(zhuǎn)換為用于網(wǎng)絡(luò)通信的IP地址。互聯(lián)網(wǎng)連通的是全球資源,單一的域名服務(wù)器不足以支撐全部的地址轉(zhuǎn)換操作,因此全球有多套域名服務(wù)器相互配合使用。早在1983年互聯(lián)網(wǎng)就開始采用層次樹狀結(jié)構(gòu)的命名方法,并使用分布式的域名系統(tǒng)進(jìn)行解析操作。然而,隨著互聯(lián)網(wǎng)的增長(zhǎng)和演變,DNS系統(tǒng)也變得越來越復(fù)雜和龐大。如果發(fā)生DNS錯(cuò)誤,用戶將無法正確解析域名,導(dǎo)致無法訪問網(wǎng)站或受到訪問延遲的影響。此外,DNS錯(cuò)誤還可能導(dǎo)致用戶被重定向到惡意網(wǎng)站或受到網(wǎng)絡(luò)釣魚等安全攻擊。對(duì)于企業(yè)而言,DNS錯(cuò)誤可能會(huì)對(duì)其業(yè)務(wù)造成經(jīng)濟(jì)等方面的損失。2023年,由于Microsoft錯(cuò)誤配置域的DNS SPF記錄,全球范圍內(nèi)的Hotmail用戶在發(fā)送電子郵件時(shí)遇到問題。2021年6月8日,F(xiàn)astly的服務(wù)中斷事件中,由于錯(cuò)誤的DNS配置,全球大量知名網(wǎng)站遭遇宕機(jī),包括紐約時(shí)報(bào)、BBC和Reddit等,宕機(jī)時(shí)間持續(xù)近1個(gè)小時(shí),僅亞馬遜就損失了約3400萬美元的銷售額。同樣,Microsoft Azure在2021年3月的服務(wù)中斷,也與DNS配置錯(cuò)誤有關(guān),嚴(yán)重影響了用戶和企業(yè)的數(shù)據(jù)和應(yīng)用程序。因此,研究和開發(fā)有效的方法來驗(yàn)證DNS配置和確保DNS服務(wù)的正確性和可靠性具有重要意義。
研究現(xiàn)狀
傳統(tǒng)技術(shù)
傳統(tǒng)技術(shù)主要集中在實(shí)時(shí)監(jiān)控、黑盒測(cè)試和語法檢查等方面。運(yùn)營(yíng)商通常會(huì)通過人工審查和驗(yàn)證DNS配置文件,以確保其符合最佳實(shí)踐和業(yè)務(wù)需求。手動(dòng)審查在DNS配置過程中扮演著重要角色。例如Akamai的Edge DNS[1]是一種全球分布式DNS服務(wù),旨在提高DNS查詢的性能和可靠性。作為行業(yè)領(lǐng)先的CDN(內(nèi)容分發(fā)網(wǎng)絡(luò))提供商,Akamai的Edge DNS提供了高可用性和低延遲的DNS查詢響應(yīng)。然而它具有傳統(tǒng)手動(dòng)審查耗時(shí)、易錯(cuò)、可擴(kuò)展性差的問題。
實(shí)時(shí)測(cè)試和監(jiān)控的方法可以通過供應(yīng)商提供的服務(wù)(如ThousandEyes[2]和CheckHost[3])或研究工具監(jiān)控正在發(fā)生的問題。
一些工具,如Microsoft的DNSlint[4],專門用于檢查DNS配置文件中的語法錯(cuò)誤和違反最佳實(shí)踐的地方。這些工具在發(fā)現(xiàn)常見的配置錯(cuò)誤方面非常有效,但它們無法進(jìn)行更深入的語義分析,無法驗(yàn)證查詢是否會(huì)解析為NXDOMAIN等錯(cuò)誤。
然而,這些方法對(duì)DNS配置缺乏直接了解,無法全面探索可能的DNS查詢空間,也無法在運(yùn)行前得知正確性,無法提供強(qiáng)有力的正確性保證。針對(duì)這些問題,人們希望判定DNS返回的結(jié)果是否滿足預(yù)設(shè)的要求,DNS配置驗(yàn)證可以通過提前分析zonefile的配置,推斷出所有可能的行為,然后將行為與要求進(jìn)行比較,以實(shí)現(xiàn)在部署前的提前驗(yàn)證。為此,下面將介紹DNS驗(yàn)證技術(shù)。
DNS驗(yàn)證技術(shù)
源代碼的形式驗(yàn)證是一種眾所周知的方法論,可保證沒有錯(cuò)誤。特別是,驗(yàn)證系統(tǒng)的功能正確性涉及定義一個(gè)正式規(guī)范,描述該系統(tǒng)的預(yù)期行為,然后使用驗(yàn)證器嚴(yán)格檢查源代碼中的每一個(gè)可能執(zhí)行路徑是否符合該規(guī)范。網(wǎng)絡(luò)路由驗(yàn)證也已經(jīng)發(fā)展了很長(zhǎng)一段時(shí)間,但是針對(duì)DNS驗(yàn)證還較少。
1.集中式DNS驗(yàn)證 [SIGCOMM’21]
新興的DNS驗(yàn)證方法旨在解決傳統(tǒng)方法的局限性,這種方法與現(xiàn)有的黑盒測(cè)試形成互補(bǔ),能夠更全面地探索可能的DNS查詢空間。隨著形式化方法在網(wǎng)絡(luò)驗(yàn)證中的應(yīng)用,出現(xiàn)了Groot[5],是第一個(gè)DNS驗(yàn)證工具。這樣的工具開始專注于通過驗(yàn)證一組區(qū)域文件來形式化定義DNS系統(tǒng)。它會(huì)檢查DNS區(qū)域文件是否符合指定的屬性,驗(yàn)證這些屬性是否對(duì)所有潛在的DNS查詢都成立,如果不成立,則提供一個(gè)反例。
盡管Groot在DNS配置驗(yàn)證方面取得了先進(jìn)的進(jìn)展,但其采用的集中化架構(gòu)面臨顯著的可擴(kuò)展性問題,以Groot為例,驗(yàn)證過程需要大約100秒才能處理一百萬個(gè)區(qū)域文件。數(shù)百萬個(gè)聚合的區(qū)域文件給DNS驗(yàn)證過程中的計(jì)算和通信帶來了巨大的開銷。這暴露了性能瓶頸,特別是在大規(guī)模網(wǎng)絡(luò)中。此外,集中化架構(gòu)通常不支持增量驗(yàn)證,這意味著每次驗(yàn)證都需要從頭開始,增加了驗(yàn)證的時(shí)間和資源消耗。
2.分布式DNS驗(yàn)證 [APNET’24]
可擴(kuò)展的DNS配置驗(yàn)證是現(xiàn)實(shí)世界中的一個(gè)關(guān)鍵挑戰(zhàn)。集中化架構(gòu)導(dǎo)致驗(yàn)證器成為性能瓶頸,因?yàn)樗枰幚硭袇^(qū)域文件的驗(yàn)證。受到分布式數(shù)據(jù)平面驗(yàn)證的啟發(fā),廈門大學(xué)SNGroup提出了分布式驗(yàn)證框架Octopus,以應(yīng)對(duì)這些挑戰(zhàn)。Octopus旨在以高效的方式應(yīng)對(duì)現(xiàn)實(shí)世界中大規(guī)模網(wǎng)絡(luò)中的DNS配置驗(yàn)證。分布式分析讓每個(gè)權(quán)威域名服務(wù)器單獨(dú)關(guān)注其區(qū)域文件,得到的本地等價(jià)類(Local equivalence class)可以更深入地了解域的行為,其對(duì)比Groot的全局等價(jià)類的數(shù)量有很大的減少。通過符號(hào)執(zhí)行技術(shù)從上到下覆蓋所有可能的查詢場(chǎng)景,并對(duì)查詢過程進(jìn)行分析,確保驗(yàn)證過程的全面性??傮w而言,該方法提高了DNS配置驗(yàn)證的效率和可靠性,解決了傳統(tǒng)集中化驗(yàn)證的性能瓶頸,提供了一種創(chuàng)新的DNS驗(yàn)證解決方案??蓴U(kuò)展的DNS驗(yàn)證工具不僅可以快速檢測(cè)大型網(wǎng)絡(luò)中的DNS配置錯(cuò)誤,未來還可以支持諸如實(shí)時(shí)配置文件驗(yàn)證,增量驗(yàn)證等服務(wù)。
3.發(fā)現(xiàn)攻擊的自動(dòng)化驗(yàn)證工具[SIGCOMM’23]
由于DNS協(xié)議規(guī)范的模糊性和極端復(fù)雜性,以及迅速發(fā)展的互聯(lián)網(wǎng)基礎(chǔ)設(shè)施。為了對(duì)抗破壞和修復(fù)循環(huán),以改善DNS基礎(chǔ)設(shè)施,研究[6]提出了一種基于Maude的形式框架,構(gòu)建了第一個(gè)端到端名稱解析的形式化語義,一個(gè)用于正式分析定性和定量屬性的組件集合,以及一個(gè)用于發(fā)現(xiàn)DoS攻擊的自動(dòng)化工具,成功應(yīng)用于分布式和聯(lián)網(wǎng)系統(tǒng)??蚣艿暮诵氖悄壳白钔暾腄NS語義模型,捕捉了端到端名稱解析的所有基本方面。該框架還集成了一個(gè)工具包,用于不同形式分析任務(wù),包括模擬、時(shí)間模型檢查和統(tǒng)計(jì)驗(yàn)證。通過這個(gè)框架,作者發(fā)現(xiàn)了現(xiàn)有的攻擊并識(shí)別出了多種新攻擊,可以實(shí)現(xiàn)較大的放大效果,并在流行的DNS實(shí)現(xiàn)中驗(yàn)證了這些攻擊。這些實(shí)現(xiàn)的測(cè)量結(jié)果與模型預(yù)測(cè)一致,證明了框架的準(zhǔn)確性和預(yù)測(cè)能力。
4.分層驗(yàn)證 [SOSP’23]
一般來說,自動(dòng)化驗(yàn)證的關(guān)鍵思想基于分層驗(yàn)證原則。然而,正在生產(chǎn)中的DNS權(quán)威引擎缺乏模塊化,尤其是由于接口不清晰和數(shù)據(jù)結(jié)構(gòu)封裝不良,使得分層驗(yàn)證難以應(yīng)用。為了解決這個(gè)挑戰(zhàn),該DNS-V[7]框架基于分層驗(yàn)證原則,采用摘要化的方法對(duì)模塊進(jìn)行全路徑符號(hào)執(zhí)行,并累積路徑條件和計(jì)算效果,將模塊的行為以抽象形式表示為輸入-效果對(duì)的集合。這種方法將系統(tǒng)分解為一組層。每一層將其源代碼的所有行為封裝到一個(gè)抽象規(guī)范中,并證明調(diào)用這個(gè)規(guī)范等同于調(diào)用相應(yīng)的源代碼。通過這種方式,每一層內(nèi)的源代碼可以獨(dú)立驗(yàn)證,因?yàn)樗灰蕾囉谳^低層功能的抽象規(guī)范。此外,DNS-V在發(fā)現(xiàn)和防止生產(chǎn)環(huán)境中的關(guān)鍵錯(cuò)誤方面取得了顯著成功,大大減少了生產(chǎn)故障和業(yè)務(wù)損失。該研究在阿里巴巴云運(yùn)營(yíng)的高可用性和可擴(kuò)展性的DNS服務(wù)上進(jìn)行實(shí)踐,為數(shù)十億的記錄和1012次查詢提供服務(wù)。
總 結(jié)
綜上所述,DNS驗(yàn)證是確保DNS服務(wù)正確性和可靠性的關(guān)鍵步驟。結(jié)合現(xiàn)有技術(shù)和新興方法,運(yùn)營(yíng)商可以更好地發(fā)現(xiàn)和解決DNS系統(tǒng)中的問題,提高DNS服務(wù)的質(zhì)量和穩(wěn)定性,為用戶提供更可靠的網(wǎng)絡(luò)體驗(yàn)。
參考文獻(xiàn)
[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.