research-article

A Formal Framework for End-to-End DNS Resolution

Authors:

Adrian PerrigAuthors Info & Claims

ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

Pages 932 - 949

https://doi.org/10.1145/3603269.3604870

Published: 01 September 2023 Publication History

Abstract

Despite the central importance of DNS, numerous attacks and vulnerabilities are regularly discovered. The root of the problem is the ambiguity and tremendous complexity of DNS protocol specifications, amid a rapidly evolving Internet infrastructure. To counteract the vicious break-and-fix cycle for improving DNS infrastructure, we instigate a foundational approach: we construct the first formal semantics of end-to-end name resolution, a collection of components for the formal analyses of both qualitative and quantitative properties, and an automated tool for discovering DoS attacks. Our formal framework represents an important step towards a substantially more secure and reliable DNS infrastructure.

References

[1]

Yehuda Afek, Anat Bremler-Barr, and Lior Shafir. 2020. NXNSAttack: Recursive DNS Ineffciencies and Vulnerabilities. In USENIX Security 2020. USENIX Association, 631--648. https://www.usenix.org/conference/usenixsecurity20/presentation/afek

[2]

Gul Agha and Karl Palmskog. 2018. A Survey of Statistical Model Checking. ACM Trans. Model. Comput. Simul. 28, 1 (2018), 6:1--6:39.

Digital Library

[3]

Gul A. Agha. 1985. Actors: a Model of Concurrent Computation in Distributed Systems (Parallel Processing, Semantics, Open, Programming Languages, Artificial Intelligence). Ph.D. Dissertation. University of Michigan, USA. http://hdl.handle.net/2027.42/160629

[4]

Gul A. Agha, José Meseguer, and Koushik Sen. 2006. PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. Electron. Notes Theor. Comput. Sci. 153, 2 (2006), 213--239.

Digital Library

[5]

Musab AlTurki and José Meseguer. 2011. PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. In CALCO 2011 (LNCS, Vol. 6859). Springer, 386--392.

[6]

Mark P. Andrews. 1998. Negative Caching of DNS Queries (DNS NCACHE). RFC 2308 (1998), 1--19.

Digital Library

[7]

Roy Arends, Rob Austein, Matt Larson, Dan Massey, and Scott Rose. 2005. Protocol Modifications for the DNS Security Extensions. RFC 4035 (2005), 1--53.

Digital Library

[8]

Theophilus Benson, Aditya Akella, and David A. Maltz. 2010. Network traffic characteristics of data centers in the wild. In IMC'10. ACM, 267--280.

[9]

Rakesh Bobba, Jon Grov, Indranil Gupta, Si Liu, José Meseguer, Peter Csaba Ölveczky, and Stephen Skeirik. 2018. Survivability: design, formal modeling, and validation of cloud storage systems using Maude. Assured cloud computing (2018), 10--48.

[10]

Stephane Bortzmeyer. 2016. DNS Query Name Minimisation to Improve Privacy. RFC 7816 (2016), 1--11.

Digital Library

[11]

Stephane Bortzmeyer, Ralph Dolmans, and Paul Hoffman. 2021. DNS Query Name Minimisation to Improve Privacy. RFC 9156 (2021), 1--11.

Digital Library

[12]

Stephane Bortzmeyer and Shumon Huque. 2016. NXDOMAIN: There Really Is Nothing Underneath. RFC 8020 (2016), 1--10.

Digital Library

[13]

Jonas Bushart and Christian Rossow. 2018. DNS Unchained: Amplified Application-Layer DoS Attacks Against DNS Authoritatives. In Research in Attacks, Intrusions, and Defenses - 21st International Symposium, RAID 2018 (LNCS, Vol. 11050). Springer, 139--160.

[14]

Martin C. Carlisle and Barry S. Fagin. 2012. IRONSIDES: DNS with no single-packet denial of service or remote code execution vulnerabilities. In GLOBECOM 2012. IEEE, 839--844.

[15]

Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, and Helmut Veith. 2018. Model checking, 2nd Edition. MIT Press. https://mitpress.mit.edu/books/model-checking-second-edition

[16]

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott (Eds.). 2007. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, Vol. 4350. Springer.

[17]

PowerDNS contributors. Accessed 2022-06-01. DNS Camel. https://powerdns.org/dns-camel/.

[18]

Tushar Deshpande, Panagiotis Katsaros, Stylianos Basagiannis, and Scott A. Smolka. 2011. Formal Analysis of the DNS Bandwidth Amplification Attack and Its Countermeasures Using Probabilistic Model Checking. In HASE 2011. IEEE Computer Society, 360--367.

[19]

Danny Dolev and Andrew Chi-Chih Yao. 1983. On the security of public key protocols. IEEE Trans. Inf. Theory 29, 2 (1983), 198--207.

Digital Library

[20]

Huayi Duan, Rubén Fischer, Jie Lou, Si Liu, David Basin, and Adrian Perrig. 2023. RHINE: Robust and High-performance Internet Naming with E2E Authenticity. In Proc. of USENIX Symposium on Networked Systems Design and Implementation (NSDI).

[21]

Robert Elz and Randy Bush. 1997. Clarifications to the DNS Specification. RFC 2181 (1997), 1--14.

Digital Library

[22]

Avishek Ghosh and Kannan Ramchandran. 2018. Faster Data-access in Large-scale Systems: Network-scale Latency Analysis under General Service-time Distributions. In 56th Annual Allerton Conference on Communication, Control, and Computing, Allerton 2018, Monticello, IL, USA, October 2-5, 2018. IEEE, 757--764.

Digital Library

[23]

Joseph A. Goguen and José Meseguer. 1992. Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theor. Comput. Sci. 105, 2 (1992), 217--273.

Digital Library

[24]

Hans Hansson and Bengt Jonsson. 1994. A Logic for Reasoning about Time and Reliability. Formal Aspects Comput. 6, 5 (1994), 512--535.

Digital Library

[25]

Donald E. Eastlake III. 2012. xNAME RCODE and Status Bits Clarification. RFC 6604 (2012), 1--5.

Digital Library

[26]

Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd D. Millstein, and George Varghese. 2020. GRooT: Proactive Verification of DNS Configurations. In SIGCOMM '20. ACM, 310--328.

Digital Library

[27]

Siva Kesava Reddy Kakarla, Ryan Beckett, Todd Millstein, and George Varghese. 2022. SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers. In NSDI '22. USENIX Association, Renton, WA, 307--323. https://www.usenix.org/conference/nsdi22/presentation/kakarla

[28]

M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In CAV'11 (LNCS, Vol. 6806). Springer, 585--591.

[29]

Edward P. Lewis. 2006. The Role of Wildcards in the Domain Name System. RFC 4592 (2006), 1--20.

Digital Library

[30]

Edward P. Lewis and Alfred Hoenes. 2010. DNS Zone Transfer Protocol (AXFR). RFC 5936 (2010), 1--29.

Digital Library

[31]

Si Liu, José Meseguer, Peter Csaba Ölveczky, Min Zhang, and David A. Basin. 2022. Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6, OOPSLA2 (2022), 315--344.

Digital Library

[32]

Si Liu, Peter Csaba Ölveczky, and José Meseguer. 2016. Modeling and analyzing mobile ad hoc networks in Real-Time Maude. J. Log. Algebraic Methods Program. 85, 1 (2016), 34--66.

[33]

Florian Maury. 2015. The "Indefinitely" Delegating Name Servers (iDNS) Attack. https://indico.dns-oarc.net/event/21/contributions/301/attachments/272/492/slides.pdf. Accessed 2022-04-30.

[34]

Catherine A. Meadows. 2001. A Cost-Based Framework for Analysis of Denial of Service Networks. J. Comput. Secur. 9, 1/2 (2001), 143--164.

Digital Library

[35]

José Meseguer. 1992. Conditional rewriting logic as a unified model of concurrency. Theoretical computer science 96, 1 (1992), 73--155.

[36]

Paul V. Mockapetris. 1987. Domain names - concepts and facilities. RFC 1034 (1987), 1--55.

Digital Library

[37]

Paul V. Mockapetris. 1987. Domain names - implementation and specification. RFC 1035 (1987), 1--55.

Digital Library

[38]

Giovane C. M. Moura, Sebastian Castro, John S. Heidemann, and Wes Hardaker. 2021. TsuNAME: exploiting misconfiguration and vulnerability to DDoS DNS. In IMC '21. ACM, 398--418.

Digital Library

[39]

Olivier Poitrey. Accessed 2023-02-07. Consider disabling CNAME scrubbing for forwarded queries #132. https://github.com/NLnetLabs/unbound/issues/132.

[40]

Scott Rose and Wouter C. A. Wijngaards. 2012. DNAME Redirection in the DNS. RFC 6672 (2012), 1--22.

Digital Library

[41]

Christian Rossow. 2014. Amplification Hell: Revisiting Network Protocols for DDoS Abuse. In NDSS 2014. The Internet Society. https://www.ndss-symposium.org/ndss2014/amplification-hell-revisiting-network-protocols-ddos-abuse

[42]

Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2005. On Statistical Model Checking of Stochastic Systems. In CAV (LNCS, Vol. 3576). Springer.

Digital Library

[43]

Ravinder Shankesi, Musab AlTurki, Ralf Sasse, Carl A. Gunter, and José Meseguer. 2009. Model-Checking DoS Amplification for VoIP Session Initiation. In ESORICS 2009 (LNCS, Vol. 5789). Springer, 390--405.

[44]

Sooel Son and Vitaly Shmatikov. 2010. The Hitchhiker's Guide to DNS Cache Poisoning. In ICST 2010 (Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, Vol. 50). Springer, 466--483.

[45]

Chuck Stearns, Vicky Risk, Suzanne Goldlust, and Cathy Almond. [n.d.]. BIND Best Practices - Recursive. https://kb.isc.org/docs/bind-best-practices-recursive. Accessed 2022-07-19.

[46]

Sam Thielman and Chris Johnston. Accessed 2023-02-07. Major cyber attack disrupts internet service across Europe and US. https://www.theguardian.com/technology/2016/oct/21/ddos-attack-dyn-internet-denial-service.

[47]

Uppaal. 2023. Uppaal 4.0.15. http://www.uppaal.org.

[48]

Abraão Aires Urquiza, Musab A. AlTurki, Max I. Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, and Carolyn L. Talcott. 2019. Resource-Bounded Intruders in Denial of Service Attacks. In CSF 2019. IEEE, 382--396.

[49]

Paul Vixie, Susan Thomson, Yakov Rekhter, and Jim Bound. 1997. Dynamic Updates in the Domain Name System (DNS UPDATE). RFC 2136 (1997), 1--26.

Digital Library

[50]

Anduo Wang, Alexander J. T. Gurney, Xianglong Han, Jinyan Cao, Boon Thau Loo, Carolyn L. Talcott, and Andre Scedrov. 2014. A reduction-based approach towards scaling up formal analysis of internet configurations. In INFOCOM 2014. IEEE, 637--645.

[51]

Thilo Weghorn, Si Liu, Christoph Sprenger, Adrian Perrig, and David Basin. 2022. N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures. In CSF 2022. IEEE.

[52]

Zack Whittaker. Accessed 2023-02-07. A DNS outage just took down a large chunk of the internet. https://techcrunch.com/2021/07/22/a-dns-outage-just-took-down-a-good-chunk-of-the-internet/.

Cited By

Hu KDu HWang Y(2024)Heracles: A Novel State-based Distributed Verification Framework for DNS ConfigurationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673890(27-32)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673890
Wang YYu KWang ZHu KDu HXiang QFang XLi GZhou RKong LShu J(2024)Rethinking DNS Configuration Verification with a Distributed ArchitectureProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663412(23-30)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663412
Larisch JThijm TAhmad SWu PArnfeld TFayed MSekar VYu MSeneviratne AVeitch D(2024)Topaz: Declarative and Verifiable Authoritative DNS at CDN-ScaleProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672240(891-903)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672240

Index Terms

A Formal Framework for End-to-End DNS Resolution
1. Networks
  1. Network properties
    1. Network security
      1. Denial-of-service attacks
  2. Network protocols
    1. Application layer protocols
    2. Protocol correctness
      1. Formal specifications
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Counteract DNS Attacks on SIP Proxies Using Bloom Filters
ARES '13: Proceedings of the 2013 International Conference on Availability, Reliability and Security

SIP proxies play an important part in VoIP services. A Denial of Service (DoS) attack on them may cause the failure of the whole network. We investigate such a DoS attack by exploiting DNS queries. A SIP proxy needs to resolve domain names for ...
Maude Object-Oriented Action Tool

Object-Oriented Action Semantics (OOAS) incorporates object-oriented concepts to the Action Semantics formalism. Its main goal is to obtain more readable and reusable semantics specifications. Moreover, it supports syntax-independent specifications, due ...
Denial of service attack and prevention on SIP VoIP infrastructures using DNS flooding
IPTComm '07: Proceedings of the 1st international conference on Principles, systems and applications of IP telecommunications

A simple yet effective Denial of Service (DoS) attack on SIP servers is to flood the server with requests addressed at irresolvable domain names. In this paper we evaluate different possibilities to mitigate these effects and show that over-provisioning ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

September 2023

1217 pages

ISBN:9798400702365

DOI:10.1145/3603269

Chairs:
Henning Schulzrinne,
Vishal Misra,
Program Chairs:
Eddie Kohler,
David Maltz

Copyright © 2023 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

SNSF for project RHINE

Conference

ACM SIGCOMM '23

Sponsor:

SIGCOMM

ACM SIGCOMM '23: ACM SIGCOMM 2023 Conference

September 10, 2023

NY, New York, USA

Acceptance Rates

Overall Acceptance Rate 462 of 3,389 submissions, 14%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
662
Total Downloads

Downloads (Last 12 months)420
Downloads (Last 6 weeks)19

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hu KDu HWang Y(2024)Heracles: A Novel State-based Distributed Verification Framework for DNS ConfigurationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673890(27-32)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673890
Wang YYu KWang ZHu KDu HXiang QFang XLi GZhou RKong LShu J(2024)Rethinking DNS Configuration Verification with a Distributed ArchitectureProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663412(23-30)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663412
Larisch JThijm TAhmad SWu PArnfeld TFayed MSekar VYu MSeneviratne AVeitch D(2024)Topaz: Declarative and Verifiable Authoritative DNS at CDN-ScaleProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672240(891-903)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672240

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents