阿里云DNS形式化驗證論文入選國際計算機系統(tǒng)頂級會議SOSP’23

近日,阿里云和北京大學合作的論文《Automated Verification of an In-Production DNS Authoritative Engine》(DNS 產品級解析服務的自動化驗證)被國際計算機系統(tǒng)頂級會議SOSP 2023主會收錄。論文提出的形式化驗證技術,對阿里云基礎設施網(wǎng)絡的DNS權威解析服務進行嚴格檢查,保證其無代碼bug、正確穩(wěn)定運行,這也是世界上第一個針對工業(yè)界產品級DNS 權威解析進行的代碼驗證技術,屬業(yè)界首創(chuàng)。

BF3058F9-E72F-4863-82F4-3B6835E994AA.jpeg

SOSP,全稱ACM Symposium on Operating Systems Principles,是ACM組織在計算機系統(tǒng)領域的旗艦型會議,也是目前國際計算機系統(tǒng)領域的頂級會議。SOSP頂會對論文的質量和數(shù)量要求極高,每年只錄用30-40篇左右正式會議論文,通常錄取率約19%(今年錄取率是 18.78%),要求投稿方具有基礎性貢獻、領導性影響和堅實的系統(tǒng)背景。

A22482C4-5D64-4093-8C62-245CB3A511E5.png

阿里云入選論文主要介紹了云基礎設施網(wǎng)絡自研DNS權威解析的形式化驗證工作,該工作對于提升阿里云DNS產品穩(wěn)定性、正確性具有重要意義。DNS全稱Domain Name System,即域名解析系統(tǒng)。它將用戶輸入的網(wǎng)址(例如:www.example.com)翻譯為網(wǎng)絡設備可以讀懂的地址(例如:1.2.3.4),從而引導用戶連接到正確的網(wǎng)絡服務器。DNS系統(tǒng)的正確性和穩(wěn)定性,是網(wǎng)絡可否成功服務廣大互聯(lián)網(wǎng)用戶的先決條件。

 

針對解析程序,傳統(tǒng)的測試技術只能保證測試用例部分正確性,并不能完整的、無死角的確保程序沒有 bug,阿里云形式化驗證工作則實現(xiàn)了無死角發(fā)現(xiàn)程序中全部bug,并降低了對人工輔助的大量依賴,目前,該驗證技術在業(yè)界已首次實際應用于規(guī)?;渴鸬漠a品代碼程序中,并高效完成了2000多行代碼的DNS權威解析程序的驗證,為云上客戶提供了真實有力的穩(wěn)定性保障。

 

論文鏈接參考:https://dl.acm.org/doi/10.1145/3600006.3613153

 

極客網(wǎng)企業(yè)會員

免責聲明:本網(wǎng)站內容主要來自原創(chuàng)、合作伙伴供稿和第三方自媒體作者投稿,凡在本網(wǎng)站出現(xiàn)的信息,均僅供參考。本網(wǎng)站將盡力確保所提供信息的準確性及可靠性,但不保證有關資料的準確性及可靠性,讀者在使用前請進一步核實,并對任何自主決定的行為負責。本網(wǎng)站對有關資料所引致的錯誤、不確或遺漏,概不負任何法律責任。任何單位或個人認為本網(wǎng)站中的網(wǎng)頁或鏈接內容可能涉嫌侵犯其知識產權或存在不實內容時,應及時向本網(wǎng)站提出書面權利通知或不實情況說明,并提供身份證明、權屬證明及詳細侵權或不實情況證明。本網(wǎng)站在收到上述法律文件后,將會依法盡快聯(lián)系相關文章源頭核實,溝通刪除相關內容或斷開相關鏈接。

2023-10-27
阿里云DNS形式化驗證論文入選國際計算機系統(tǒng)頂級會議SOSP’23
近日,阿里云和北京大學合作的論文《Automated Verification of an In-Production DNS Authoritative Engine》(DNS產品級解析服務的自動化驗證)被國際計算機系統(tǒng)頂級會議SOSP 2023主會收錄。論文提出的形式化驗證技術,對阿里云基礎設施網(wǎng)絡的DNS權威解析服務進行嚴格檢查...

長按掃碼 閱讀全文