October 27, 2023 – Recently, a collaborative research paper between Alibaba Cloud (Alibaba’s cloud computing subsidiary) and Peking University titled “Automated Verification of an In-Production DNS Authoritative Engine” has been accepted for presentation at the prestigious ACM Symposium on Operating Systems Principles (SOSP) 2023. This paper introduces a groundbreaking approach to formal verification technology, which rigorously examines Alibaba Cloud’s infrastructure network’s DNS authoritative resolution service. The aim is to ensure its flawless operation, free from code bugs, making it the first-of-its-kind code verification technique for an industrial-grade DNS authoritative resolution.
SOSP, the ACM Symposium on Operating Systems Principles, is a flagship event in the field of computer systems organized by the ACM (Association for Computing Machinery). It is considered one of the most esteemed conferences in the international computer systems domain. SOSP maintains exceptionally high standards for the quality and quantity of accepted papers, with only about 30-40 formal conference papers admitted each year. The acceptance rate is usually around 19%, with this year’s rate being 18.78%. To secure a place at SOSP, contributions must be foundational, possess leadership influence, and demonstrate a solid systems background.
Alibaba Cloud’s featured paper sheds light on their in-house DNS authoritative resolution’s formal verification work, which holds significant importance in enhancing the stability and accuracy of Alibaba Cloud’s DNS products. DNS, or Domain Name System, is a fundamental component of the internet. It translates user-inputted domain names (e.g., www.example.com) into machine-readable addresses (e.g., 1.2.3.4), directing users to the correct network server. The correctness and stability of DNS systems are fundamental prerequisites for successful internet service to a wide array of users.
Traditional testing techniques for resolution programs can only partially guarantee the correctness of test cases. They fail to comprehensively ensure that the program is entirely free from bugs. In contrast, Alibaba Cloud’s formal verification work accomplishes the full identification of all bugs within the program without any blind spots. It significantly reduces reliance on manual assistance. Currently, this verification technology has been practically deployed in large-scale product codebases within the industry. It efficiently completed the verification of over 2000 lines of code for DNS authoritative resolution programs, providing Alibaba Cloud’s cloud customers with a robust assurance of stability.
For more information about the research paper, you can visit the following link: Research Paper Link.
