Speaker
Description
This paper presents a cross-RFC formal analysis of DNSSEC specifications, built on the SAPIC+ symbolic verifier, modeling cross-RFC interactions including cryptographic operations and stateful caching. We verify four core security guarantees: data origin authenticity, integrity, chain of trust, and authenticated denial of existence. Our analysis shows that core authentication properties hold as specified, while wildcard expansion, the mechanism that bridges positive and negative authentication, exhibits a cross-RFC interaction vulnerability that defeats DNSSEC's integrity guarantee.
Specifically, we discover Cross-Zone Wildcard Cache Poisoning: a new attack in which a malicious zone operator exploits a gap in the DNSSEC specifications to poison resolver caches with forged records for domains outside its authority, served to clients as DNSSEC-authentic. All four major resolvers that implement the affected caching optimization are vulnerable under default configurations, and all four vendors have confirmed the vulnerability and adopted our proposed fix. To our knowledge, this is the first protocol-level attack in which a conformant validator completes validation and serves attacker-chosen positive data when the Authenticated Data (AD) bit in a response is 1: prior attacks instead exhausted availability, downgraded to AD=0, or skipped validation.
Our models additionally surface two cross-RFC denial-of-service flaws and rediscover three known attack classes. We confirm real-world impact through testing of six DNS resolvers and an Internet-scale scan of 2.24 million open resolvers, and propose updates to four RFCs to close these gaps.
| Talk duration | 20 Minutes (+5 for Q&A) |
|---|
