Let's talk about DNS formal verification technology

background

The Domain Name System (DNS) is a distributed naming system in the Internet. It serves as the "phone book" of the Internet, converting user-friendly domain names into IP addresses for network communications. The Internet connects global resources, and a single domain name server is not enough to support all address conversion operations, so there are multiple sets of domain name servers around the world that work together. As early as 1983, the Internet began to adopt a hierarchical tree-structured naming method and used a distributed domain name system for resolution operations. However, as the Internet grew and evolved, the DNS system has become more and more complex and large. If a DNS error occurs, users will not be able to correctly resolve the domain name, resulting in inaccessibility to the website or access delays. In addition, DNS errors may also cause users to be redirected to malicious websites or be subject to security attacks such as phishing. For businesses, DNS errors may cause economic and other losses to their business. In 2023, Hotmail users around the world encountered problems sending emails due to Microsoft's misconfiguration of the domain's DNS SPF record. On June 8, 2021, a large number of well-known websites around the world, including the New York Times, BBC, and Reddit, suffered downtime due to incorrect DNS configuration during the Fastly service outage. The downtime lasted for nearly an hour, and Amazon alone lost about $34 million in sales. Similarly, Microsoft Azure's service outage in March 2021 was also related to DNS misconfiguration, which seriously affected the data and applications of users and enterprises. Therefore, it is of great significance to study and develop effective methods to verify DNS configuration and ensure the correctness and reliability of DNS services.

Research status

Traditional Technology

Traditional technologies mainly focus on real-time monitoring, black box testing, and syntax checking. Operators usually manually review and verify DNS configuration files to ensure that they comply with best practices and business requirements. Manual review plays an important role in the DNS configuration process. For example, Akamai's Edge DNS[1] is a globally distributed DNS service designed to improve the performance and reliability of DNS queries. As an industry-leading CDN (content delivery network) provider, Akamai's Edge DNS provides high availability and low latency DNS query responses. However, it has the problems of traditional manual review being time-consuming, error-prone, and poor scalability.

Real-time testing and monitoring can be done through vendor-provided services such as ThousandEyes[2] and CheckHost[3] or research tools that monitor ongoing issues.

Some tools, such as Microsoft's DNSlint[4], are specifically designed to check DNS configuration files for syntax errors and best practice violations. These tools are very effective in finding common configuration errors, but they are unable to perform deeper semantic analysis and verify whether a query will resolve to an error such as NXDOMAIN.

However, these methods lack direct knowledge of DNS configuration, cannot fully explore the possible DNS query space, cannot know the correctness before running, and cannot provide strong correctness guarantees. To address these issues, people want to determine whether the results returned by DNS meet the preset requirements. DNS configuration verification can analyze the zonefile configuration in advance, infer all possible behaviors, and then compare the behaviors with the requirements to achieve advance verification before deployment. To this end, the DNS verification technology will be introduced below.

DNS Validation Technology

Formal verification of source code is a well-known methodology for ensuring the absence of bugs. In particular, verifying the functional correctness of a system involves defining a formal specification that describes the expected behavior of that system, and then using a verifier to rigorously check that every possible execution path in the source code complies with that specification. Network routing verification has also been around for a long time, but DNS verification has been less well established.

1. Centralized DNS Validation [SIGCOMM'21]

Emerging DNS verification methods aim to address the limitations of traditional methods. This method complements existing black-box testing and can more comprehensively explore the space of possible DNS queries. With the application of formal methods in network verification, Groot[5] emerged as the first DNS verification tool. Such tools began to focus on formally defining the DNS system by verifying a set of zone files. It checks whether the DNS zone files conform to specified properties, verifies whether these properties hold for all potential DNS queries, and provides a counterexample if they do not hold.

Although Groot has made advanced progress in DNS configuration verification, the centralized architecture it adopts faces significant scalability issues. Taking Groot as an example, the verification process takes about 100 seconds to process one million zone files. Millions of aggregated zone files bring huge overhead to the calculation and communication in the DNS verification process. This exposes performance bottlenecks, especially in large-scale networks. In addition, centralized architectures usually do not support incremental verification, which means that each verification needs to start from scratch, increasing the time and resource consumption of verification.

2. Distributed DNS Validation [APNET'24]

Scalable DNS configuration verification is a key challenge in the real world. The centralized architecture causes the validator to become a performance bottleneck because it needs to handle the verification of all zone files. Inspired by distributed data plane verification, SNGroup of Xiamen University proposed Octopus, a distributed verification framework, to address these challenges. Octopus aims to handle DNS configuration verification in large-scale networks in the real world in an efficient way. Distributed analysis allows each authoritative domain name server to focus on its zone file separately, and the resulting local equivalence class can provide a deeper understanding of the behavior of the domain, which is significantly reduced compared to the number of global equivalence classes of Groot. All possible query scenarios are covered from top to bottom through symbolic execution technology, and the query process is analyzed to ensure the comprehensiveness of the verification process. Overall, this method improves the efficiency and reliability of DNS configuration verification, solves the performance bottleneck of traditional centralized verification, and provides an innovative DNS verification solution. The scalable DNS verification tool can not only quickly detect DNS configuration errors in large networks, but also support services such as real-time configuration file verification and incremental verification in the future.

3. Automated verification tools for attack discovery [SIGCOMM'23]

Due to the ambiguity and extreme complexity of the DNS protocol specification and the rapidly evolving Internet infrastructure. In order to combat the cycle of destruction and repair to improve the DNS infrastructure, the study [6] proposed a formal framework based on Maude, constructed the first formal semantics of end-to-end name resolution, a set of components for formally analyzing qualitative and quantitative properties, and an automated tool for discovering DoS attacks, which was successfully applied to distributed and networked systems. The core of the framework is the most complete DNS semantic model currently available, capturing all the basic aspects of end-to-end name resolution. The framework also integrates a toolkit for different formal analysis tasks, including simulation, temporal model checking, and statistical verification. Through this framework, the authors discovered existing attacks and identified a variety of new attacks that can achieve large amplification effects, and verified these attacks in popular DNS implementations. The measurement results of these implementations are consistent with the model predictions, proving the accuracy and predictive power of the framework.

4. Hierarchical Validation [SOSP'23]

In general, the key idea of ​​automated verification is based on the principle of layered verification. However, the lack of modularity in DNS authoritative engines in production, especially due to unclear interfaces and poor encapsulation of data structures, makes layered verification difficult to apply. To address this challenge, the DNS-V[7] framework is based on the layered verification principle and adopts an abstraction approach to perform full-path symbolic execution on modules and accumulate path conditions and computation effects, representing the module's behavior in an abstract form as a set of input-effect pairs. This approach decomposes the system into a set of layers. Each layer encapsulates all the behaviors of its source code into an abstract specification and proves that calling this specification is equivalent to calling the corresponding source code. In this way, the source code within each layer can be independently verified because it only depends on the abstract specifications of the lower layer functions. In addition, DNS-V has achieved remarkable success in discovering and preventing critical errors in production environments, greatly reducing production failures and business losses. This research is practiced on a highly available and scalable DNS service operated by Alibaba Cloud, serving billions of records and 1012 queries.

Summarize

In summary, DNS validation is a key step to ensure the correctness and reliability of DNS services. Combining existing technologies and emerging methods, operators can better discover and solve problems in the DNS system, improve the quality and stability of DNS services, and provide users with a more reliable network experience.

References

[1] Akamai https://www.akamai.com/products/edge-dns

[2] ThousandEyes https://www.thousandeyes.com/resources/dns-webinar

[3] Check Host https://check-host.net/

[4] Lint https://learn.microsoft.com/en-US/previous-versions/troubleshoot/windows-server/description-dnslint-utility

[5] Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, and George Varghese. 2020. GRooT: Proactive Verification of DNS Configurations. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication. Association for Computing Machinery, New York, NY, USA, 310–328.

[6] Si Liu, Huayi Duan, Lukas Heimes, Marco Bearzi, Jodok Vieli, David Basin, and Adrian Perrig. 2023. A Formal Framework for End-to-End DNS Resolution. In Proceedings of the ACM SIGCOMM 2023 Conference (ACM SIGCOMM '23). Association for Computing Machinery, New York, NY, USA, 932–949.

[7] Naiqian Zheng, Mengqi Liu, Yuxing Xiang, Linjian Song, Dong Li, Feng Han, Nan Wang, Yong Ma, Zhuo Liang, Dennis Cai, Ennan Zhai, Xuanzhe Liu, and Xin Jin. 2023. Automated Verification of an In-Production DNS Authoritative Engine. In Proceedings of the 29th Symposium on Operating Systems Principles (SOSP '23). Association for Computing Machinery, New York, NY, USA, 80–95.