Speaker
Description
DNS zone misconfigurations are a notorious source of outages and frustration, particularly when DNSSEC is involved. Previous research has attempted to address the problem of zone misconfigurations using formal reasoning methods, but all existing proposals (i) suggest verifying only the absence of specific, known classes of misconfiguration and (ii) do not consider DNSSEC.
We have developed a new formal model of recursive resolution in the DNS that, to our knowledge, is the most complete model to date, capturing the full complexity of DNSSEC. The model was designed to reason about the resolvability of zones: which queries can be resolved under a given configuration. Instead of verifying the absence of a predefined set of undesirable properties, we verify the desirable property of resolvability. Our model compares how changes to a zone configuration impact which queries can be resolved, allowing it to naturally detect many misconfigurations without explicitly searching for them.
In this talk, we will present our new model and its implementation and demonstrate how it can naturally discover DNS zone misconfigurations. We validate our methodology both formally, proving the soundness of its reasoning, and empirically, testing its conformance with major recursive resolver implementations. This testing is only possible because our model incorporates all relevant standards, including those that specify DNSSEC. Finally, we outline how our approach could be integrated into operational practice to support real-world DNS management.
| Talk duration | 20 Minutes (+5 for Q&A) |
|---|
