DNS/hitch-hikerについて、ここに記述してください。

/Shmatikov   /bailiwick-checking   /bailiwick-rule   /taxonomy  

Contents

  1. 6 Formal Model of DNS Resolver
    1. 6.1 Modeling methodology

DNS/毒盛/Shmatikov

The Hitchhiker’s Guide to DNS Cache Poisoning

https://www.cs.utexas.edu/~shmat/shmat_securecomm10.pdf 

Conference Paper · September 2010 with 27 Reads
DOI: 10.1007/978-3-642-16161-2_27 · Source: DBLP
Conference: Security and Privacy in Communication Networks - 6th Iternational ICST Conference, SecureComm 2010, Singapore, September 7-9, 2010. Proceedings

https://www.researchgate.net/publication/221273067_The_Hitchhiker's_Guide_to_DNS_Cache_Poisoning

SecureComm 2010 LNICST 50 pp.466-483 (2010) にもある。

/bailiwick-checking

Abstract. 

DNS cache poisoning is a serious threat to today’s Internet. 

We develop a formal model of the semantics of DNS caches, including the bailiwick rule 
and trust-level logic, and use it to systematically investigate different types
of cache poisoning and to generate templates for attack payloads. 

We explain the impact of the attacks on DNS resolvers such as BIND, MaraDNS, and Unbound
and their implications for several defenses against DNS cache poisoning.

ここに書かれていることから見てもMaraDNS(deadwood) だけが見込みありそう。

1. 6 Formal Model of DNS Resolver

1.1. 6.1 Modeling methodology

As shown in Sections 4 and 5, the semantics of DNS caches are quite complicated.

To understand the potential impact of cache poisoning attacks, we construct a formal model of the default bailiwick-checking and cache-overwriting rules of BIND v9.4.1 and Unbound v1.3.4. 

We do not build a formal model for MaraDNS because it does not
cache the authority and additional sections of responses containing an answer RRset and
does not use trust levels for overwriting existing records.

We do show attacks against all three implementations, including MaraDNS, in Table 4

We use the ProVerif protocol analysis tool, due to its success in practical formal verification of security protocols (e.g., [2]). The details of ProVerif are beyond the scope of this paper and can be found in [6]. The behavior of each protocol participant is modeled as a set of Horn clauses, which represent sending or receiving messages on specified communication channels.

ProVerif then uses a sound, resolution-based algorithm to determine whether a specified property holds over all executions of the protocol.

Fig. 3 shows the abstract model of DNS resolver. We use it to check whether or not a cached resource record with a certain label and trust level is secure against cache poisoning conducted by the active adversary who has complete control of the network.

This attacker model may appear strong, but we emphasize once again that our goal is to model the internal behavior of DNS resolvers, not the details of the network protocol through which DNS messages are exchanged. By modeling the network as a public channel, we can focus on the semantics of the cache and abstract from the particulars of the forgery method through which attacker packets are introduced.

The initial state of the model asserts that three valid records of types A, NS, and CNAME, respectively, have been cached. Their labels are determined via network in- puts. (In reality, the attacker can insert an arbitrary label into the cache by tricking a client of the resolver into asking to resolve the corresponding name.) Trust levels are specified manually. The model then receives a query from the network. If recursive res- olution is required, the model sends out a recursive query and receives a response from the network. The bailiwick rule in the model determines which records in the response 10 Sooel Son and Vitaly Shmatikov should be cached.

If a malicious record satisfies the bailiwick conditions, the model asserts that a cache poisoning event has occurred.