摘要：

近期，阿里巴巴云与北京大学携手发布的学术论文《DNS权威解析服务的自动化验证》，在国际计算机系统领域顶级会议SOSP 2023上脱颖而出，被大会收录。这篇论文创新地应用了形式化验证技术，对阿里巴巴云的基础设施网络DNS权威解析服务进行了全面而严格的审查。这一技术不仅确保了服务无代码错误且运行稳定，还开创了全球首个对工业级DNS权威解析服务进行代码验证的先河。

SOSP，即ACM Symposium on Operating Systems Principles，作为计算机系统领域的重要盛会，以其对论文质量与数量的严格要求著称，每年仅接纳30至40篇左右的正式会议论文，录取率约为19%，体现了其对基础性贡献、领导性影响以及扎实系统背景的高标准要求。阿里巴巴云入选的论文重点阐述了其在自研DNS权威解析方面的形式化验证工作，这项工作对于增强DNS产品的稳定性和准确性具有深远意义。

DNS，即Domain Name System，是将用户输入的网址（如www.example.com）转换为网络设备能识别的地址（如1.2.3.4），以引导用户连接至正确的网络服务器的核心系统。DNS系统的可靠性与稳定性，是网络能否高效服务于广大互联网用户的关键因素。

针对解析程序的传统测试手段往往局限于部分正确性的验证，难以实现全面且无遗漏的错误查找。阿里巴巴云所采用的形式化验证技术，则实现了对程序内所有潜在错误的精确发现，并显著减少了对人工干预的需求。目前，这一验证技术已成功应用于大规模部署的DNS权威解析程序代码中，高效完成了超过2000行代码的验证工作，为云上客户提供强有力的稳定性保障。