Reachability Analysis of the Domain Name System
summary
Provides a decision procedure for DNS verification with worst-case complexity 2ExpTime decision procedure, using a concrete-to-abstract homomorphism that collapses domain names into a finite monoid abstraction via syntactic congruences. Introduces a novel generalized bisimulation to prove soundness and completeness, shows DNS is eager so it reduces to pushdown systems, and models NXNS, amplification, and rewrite blackholing. Reports doubly-exponential complexity and a prototype implementation in progress that can produce concrete witnesses.
AI-written summary · about
chapters (14)
- 0:00DNS reachability analysis
- 1:10DNS with real-world analogy
- 4:02DNS name server hierarchy
- 5:28NXNS attack impact
- 6:51DNS DDoS attacks
- 7:33Formalizing DNS with zone files
- 8:35Testing and formal methods limits
- 10:01Modeling DNS resolvers
- 11:48Domain name abstraction challenges
- 12:53Domain congruence in DNS
- 13:55DNS eagerness and decidability
- 14:37Reachability via push-down systems
- 15:19Summary and future work
- 16:06Q&A on temporal properties
related talks
15mYou Depend on DNS, This Is How It Works and You Won't...
26mMisuse of DNS, the Second Most Used Protocol
01h 27mDNS at 30
10mLet’s implement DNS to learn history!
40mScaling DNS
28mDarwin & Protocols
16mAttacking with Something That Does Not Exist: 'Proof of Non-Existence' Can Exhaust DNS...- 28mDarwin & Protocols