阿里云DNS形式化验证论文入选国际计算机系统顶级会议SOSP’23

近日，阿里云和北京大学合作的论文《Automated Verification of an In-Production DNS Authoritative Engine》（DNS 产品级解析服务的自动化验证）被国际计算机系统顶级会议SOSP 2023主会收录。论文提出的形式化验证技术，对阿里云基础设施网络的DNS权威解析服务进行严格检查，保证其无代码bug、正确稳定运行，这也是世界上第一个针对工业界产品级DNS 权威解析进行的代码验证技术，属业界首创。

SOSP，全称ACM Symposium on Operating Systems Principles，是ACM组织在计算机系统领域的旗舰型会议，也是目前国际计算机系统领域的顶级会议。SOSP顶会对论文的质量和数量要求极高，每年只录用30-40篇左右正式会议论文，通常录取率约19%（今年录取率是 18.78%），要求投稿方具有基础性贡献、领导性影响和坚实的系统背景。

阿里云入选论文主要介绍了云基础设施网络自研DNS权威解析的形式化验证工作，该工作对于提升阿里云DNS产品稳定性、正确性具有重要意义。DNS全称Domain Name System，即域名解析系统。它将用户输入的网址（例如：www.example.com）翻译为网络设备可以读懂的地址（例如：1.2.3.4），从而引导用户连接到正确的网络服务器。DNS系统的正确性和稳定性，是网络可否成功服务广大互联网用户的先决条件。

针对解析程序，传统的测试技术只能保证测试用例部分正确性，并不能完整的、无死角的确保程序没有 bug，阿里云形式化验证工作则实现了无死角发现程序中全部bug，并降低了对人工辅助的大量依赖，目前，该验证技术在业界已首次实际应用于规模化部署的产品代码程序中，并高效完成了2000多行代码的DNS权威解析程序的验证，为云上客户提供了真实有力的稳定性保障。

论文链接参考：https://dl.acm.org/doi/10.1145/3600006.3613153

生成海报

免责声明：本网站内容主要来自原创、合作伙伴供稿和第三方自媒体作者投稿，凡在本网站出现的信息，均仅供参考。本网站将尽力确保所提供信息的准确性及可靠性，但不保证有关资料的准确性及可靠性，读者在使用前请进一步核实，并对任何自主决定的行为负责。本网站对有关资料所引致的错误、不确或遗漏，概不负任何法律责任。任何单位或个人认为本网站中的网页或链接内容可能涉嫌侵犯其知识产权或存在不实内容时，应及时向本网站提出书面权利通知或不实情况说明，并提供身份证明、权属证明及详细侵权或不实情况证明。本网站在收到上述法律文件后，将会依法尽快联系相关文章源头核实，沟通删除相关内容或断开相关链接。