阿里云DNS权威解析自动化验证_阿里云DNS形式化验证论文入选国际计算机系统顶级会议SOSP’23

最新时期，阿里云与北京大学联手撰写的名为《 of an In- DNS 》（DNS产品级解析服务的自动化验证）的论文，成功入选了国际计算机系统领域顶尖会议SOSP 2023的主会议程。该论文阐述的方法，运用形式化检测手段，对阿里云基础架构网络中的DNS权威解析功能执行了全面审查，确保其不存在程序缺陷且能正常稳定运作，这标志着全球首次针对工业领域产品级DNS权威解析实施代码验证，开创了行业先河。

SOSP是ACM组织在计算机系统领域主办的最高级别会议，也是全球计算机系统领域的权威盛会，其全称为ACM on 。该会议对论文的水平和数量有非常严格的标准，每年大约只会选择30到40篇正式会议论文，一般录取比例在19%左右，今年具体为18.78%。投稿作品必须展现出基础性的学术价值、具有引领行业的影响力，并且作者需要具备深厚的系统技术功底。

阿里云论文着重阐述了云设施网络自主研发DNS权威解析的形式化验证方法，这项工作对于增强阿里云DNS产品性能、确保其准确无误具有关键作用。DNS全称为Name，也就是域名解析系统。它能够将用户输入的网址（比如示例网址）转译成网络设备能够识别的地址（例如数字序列1.2.3.4），借此帮助用户顺利接入正确的网络服务。DNS系统运行是否可靠，关乎网络能否顺利为众多网民提供有效服务，这是基础保障。

解析程序通常借助传统测试手段，仅能验证部分测试用例的正确性，无法全面且彻底地排除程序中的错误，阿里云采用的形式化验证技术则能彻底发现所有潜在问题，显著减少人工介入的需求，这种验证方法已率先在业界应用于大规模部署的产品代码，成功验证了超过两千行代码的DNS权威解析程序，为云服务客户带来了可靠的稳定性支持。

论文链接参考：