近日，阿里云与北京大学联合开展的论文《生产中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，即域名解析系统。它将用户输入的URL（例如：www.example.com）翻译成网络设备可以理解的地址（例如：1.2.3.4），从而引导用户连接到正确的网络服务器。 DNS系统的正确性和稳定性是网络成功服务广大互联网用户的前提。

对于解析程序，传统的测试技术只能保证测试用例的部分正确，而不能完全、无盲点地保证程序没有Bug。阿里云的形式化验证工作可以无盲点地发现程序中的所有Bug，降低测试成本。该验证技术严重依赖人工辅助，在业界首次实际应用于产品代码程序的大规模部署，高效完成了2000多行代码的DNS权威解析程序的验证，为云客户提供真正强大的稳定性保障。

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