Formal Analysis of the Kaminsky DNS Cache-Poisoning Attack Using Probabilistic Model Checking

Nikolaos Alexiou1, Tushar Deshpande2, Stylianos Basagiannis1
Scott A. Smolka2 and Panagiotis Katsaros1

1Department of Informatics, Aristotle University of Thessaloniki,
Thessaloniki, 54124, Greece
Email: {nalexiou,basags,katsaros}@csd.auth.gr
2Department of Computer Science, Stony Brook University
Stony Brook, NY 11794-4400, USA
E-mail: {tushard,sas}@cs.sunysb.edu


Abstract

We use the probabilistic model checker PRISM to formally model and analyze the highly publicized Kaminsky DNS cache-poisoning attack. DNS (Domain Name System) is an internet-wide, hierarchical naming system used to translate domain names such as google.com into physical IP addresses such as 208.77.188.166. The Kaminsky DNS attack is a recently discovered vulnerability in DNS that allows an intruder to hijack a domain; i.e. corrupt a DNS server so that it replies with the IP address of a malicious web server when asked to resolve the URL of a non-malicious domain such as google.com. A proposed fix for the attack is based on the idea of randomizing the source port a DNS server uses when issuing a query to another server in the DNS hierarchy.

We use PRISM to introduce a Continuous Time Markov Chain representation of the Kaminsky attack and the proposed fix, and to perform the requisite probabilistic model checking. Our results, gleaned from more than 240 PRISM runs, formally validate the existence of the Kaminsky cache-poisoning attack even in the presence of an intruder with virtually no knowledge of the victim DNS server’s actions. They also serve to quantify the effectiveness of the proposed fix, demonstrating an exponentially decreasing, long-tail trajectory for the probability of a successful attack with an increasing range of source-port ids, as well as an increasing attack probability with an increasing number of attempted attacks or increasing rate at which the intruder guesses the source-port id.

Click to read the full text of the paper

Click here to download the PRISM Model Checker

Download Model Files
Model Source FileDownload
CSL FileDownload

Parameter Settings for PRISM Models

We used following command line options provided by PRISM

Command Line SwitchUsage
-fixdlAutomatically put self-loops in deadlock states
-cuddmaxmem <n>Set max memory for CUDD package (KB) [default 200x1024]
-const <vals>Run an experiment using constant values <vals>

e.g. Here's a sample command line to execute the model.

PRISM -fixdl -cuddmaxmem 819200 kaminsky.sm kaminsky.csl -const TIMES_TO_REQUEST_URL=10,popularity=9,port_id=100,guess=30,other_legitimate_requests_rate=35

This command allocates 800 Mbyte memory to PRISM. Then PRISM executes the model defined in the file kaminsky.sm and checks it against the assertions defined in kaminsky.csl.
The model is executed with following values of parameters

  1. TIMES_TO_REQUEST_URL=10
  2. popularity=9
  3. port_id=100
  4. guess=30
  5. other_legitimate_requests_rate=35

Note: We observed that the amount of memory required by PRISM varied between 8 Mbyte to 800 Mbyte. We suggest that 800 Mb memory should be allocated to PRISM while running our models. This would allow all models to run successfully without causing out of memory error.

Result of Model Execution

These results correspond to the Figs. 2-7 from the paper.

Result Set #1: Varying times_to_request_url with max_port_id =1

times_to_request_urlguess=30 (low)guess=60 (medium)guess=130 (high)
1 0.013 0.025 0.052
2 0.025 0.050 0.101
4 0.050 0.096 0.192
6 0.073 0.140 0.274
8 0.097 0.182 0.347
10 0.119 0.222 0.413
12 0.141 0.261 0.473
14 0.163 0.297 0.526
16 0.184 0.331 0.574
18 0.204 0.364 0.617
20 0.224 0.395 0.656
22 0.244 0.425 0.691
24 0.263 0.453 0.722
26 0.281 0.480 0.750
28 0.300 0.506 0.775
30 0.317 0.530 0.798

Result Set #2: Varying other_legitimate_requests_rate with max_port_id =1

other_legitimate_re-
quest_rate
times_to_request_url = 2 times_to_request_url = 6
10 0.01 0.04
20 0.02 0.07
40 0.05 0.13
60 0.07 0.19
80 0.09 0.25
100 0.11 0.3
120 0.13 0.34
140 0.15 0.38
160 0.17 0.42
180 0.18 0.46
200 0.2 0.49
220 0.22 0.52
240 0.23 0.55
260 0.25 0.57
280 0.26 0.6
300 0.28 0.62

Result Set #3: guess with max_port_id =1

guess times_to_request_url = 2 times_to_request_url = 6
10 0.035 0.103
20 0.069 0.193
40 0.130 0.341
60 0.184 0.456
80 0.232 0.548
100 0.276 0.620
120 0.315 0.679
140 0.351 0.726
160 0.383 0.765
180 0.412 0.797
200 0.440 0.824
220 0.464 0.846
240 0.487 0.865
260 0.508 0.881
280 0.527 0.894
300 0.545 0.906

Result Set #4: Results for different times_to_request_url values while varying max_port_id values

max_port_id times_to_request_url = 2 times_to_request_url = 6
10 0.069 0.193
25 0.029 0.083
50 0.014 0.043
75 0.010 0.029
100 0.007 0.022
125 0.006 0.017
150 0.005 0.015
175 0.004 0.013
200 0.004 0.011
225 0.003 0.010
250 0.003 0.009
275 0.003 0.008
300 0.002 0.007
325 0.002 0.007
350 0.002 0.006
375 0.002 0.006
400 0.002 0.006

Result Set #5: Results for different guess rates while varying max port id values while varying max_port_id values

max_port_id guess=50 guess=100 guess=150 guess=250
100 0.006 0.011 0.016 0.022
125 0.004 0.009 0.013 0.017
150 0.004 0.007 0.011 0.015
175 0.003 0.006 0.009 0.013
200 0.003 0.005 0.008 0.011
225 0.002 0.005 0.007 0.010
250 0.002 0.004 0.007 0.009
275 0.002 0.004 0.006 0.008
300 0.002 0.004 0.006 0.007
325 0.002 0.003 0.005 0.007
350 0.002 0.003 0.005 0.006
375 0.002 0.003 0.004 0.006
400 0.001 0.003 0.004 0.005

Result Set #6: Results for different popularity values while varying max port id values while varying max_port_id values

max_port_id popularity = 2 (low) popularity = 5 (medium) popularity = 9 (high)
10 0.426 0.290 0.065
25 0.205 0.133 0.028
50 0.110 0.070 0.014
75 0.075 0.047 0.010
100 0.057 0.036 0.007
125 0.046 0.029 0.006
150 0.038 0.024 0.005
175 0.033 0.021 0.004
200 0.029 0.018 0.004
225 0.026 0.016 0.003
250 0.023 0.015 0.003
275 0.021 0.013 0.003
300 0.019 0.012 0.002
325 0.018 0.011 0.002
350 0.017 0.010 0.002
375 0.016 0.010 0.002
400 0.015 0.009 0.002