Iceberg: Automated Verification of DNS Authoritative Engines via Just-in-Time...
summary
Iceberg implements just-in-time summarization over LLVM IR with Z3 to verify DNS authoritative engines automatically, using state splitting, symbolic regions, summary optimization and stub interposing. It runs as a Rust tool (≈16K LOC), verifies core lookup logic in CoreDNS, BIND, PowerDNS and Knot, and finds 12 new bugs (8 in CoreDNS). Porting costs about one person-week, inspect-to-code ratios 5.8–9.6%, and runs complete in minutes for small zones, ~30 minutes for complex zones, and a few hours for production zones.
AI-written summary · about
chapters (11)
- 0:00Iceberg and DNS verification
- 1:23DNS correctness challenges
- 2:50Limitations of ahead-of-time summarization
- 4:16Just-in-time summarization with Iceberg
- 7:05Automatic summary building
- 9:31Core algorithms in Iceberg
- 10:56Iceberg workflow details
- 12:00Real-world DNS verification
- 13:46Evaluation results vs SCALE
- 15:30Broader implications and future
- 15:51Summary and Q&A
related talks
16mSCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers
41mErlang for Authoritative DNS
01h 27mDNS at 30
27mA Longitudinal, End-to-End View of the DNSSEC Ecosystem
29mGlobal Measurement of DNS Manipulation
15mRHINE: Robust and High-performance Internet Naming with E2E Authenticity
16mAttacking with Something That Does Not Exist: 'Proof of Non-Existence' Can Exhaust DNS...
33mZero Trust with Iceberg REST Catalog and Policy Engines