Transcript Model of Dynamic Configuration of Link Local address

Analysis of a Protocol for Dynamic
Configuration of IPv4 Link Local
Addresses Using Uppaal
Miaomiao Zhang
Frits W. Vaandrager
Department of Computer Science
University of Nijmegen
Contents
•
•
•
•
•
Informal explanation of the protocol
Purpose of our work
Model in UPPAAL
Results and analysis
Future work
Contents
•
•
•
•
•
Informal explanation of the protocol
Purpose of our work
Model in UPPAAL
Results and analysis
Future work
Protocol
• Nondeterministically select an IP address
Wait time: 0~2 seconds.
• Claim the IP address
–
4 probes
2 seconds before sending next probe
number of collision(10)
Reselect a new IP address after 60 seconds
– 2 gratuitous ARP packet
2 seconds waiting
After 8~10 seconds, host uses the IP address.
Protocol
•
Address collision and defense(ongoing process).
As to conflicting ARP packet
–
–
Either immediately configure a new IP address.
Or receives 2 conflicting ARP packets within 10
seconds, reconfigurate. Otherwise, send gratuitous
ARP.
Note:
(1)All ARP packets are sent using broadcast instead of unicast.
(2)Any probe sent from one host will not become a conflicting ARP
packet to the other hosts.
Contents
•
•
•
•
•
Informal explanation of the protocol
Purpose of our work
Model in UPPAAL
Results and analysis
Future work
Purpose of our work
• Makes a detailed model in Uppaal with several hosts
run concurrently. If possibly the protocol allows for
some unexpected scenarios, such as two hosts
acquiring the same IP address in a setting without
message loss.
• Improve the performance
(1)No two host get the same IP address
(2)Less time to get an IP address.
Some assumptions
1.
2.
3.
4.
The underlying network consists of a single “wire” and
contains no routers, keep FIFO rule.
At any time there is at most only one message on the
wire. So this means that we do not consider bus
collisions.
There is a nonzero message delay. Also, we assume
there is a known upper bound on the transmission delay.
As soon as a packet arrives at some host, it will be
processed at once. We assume processing time is zero.
Note a host can not receive two packets at the
same time.
Structure of the system
input buffer
ive
rece
e
rec
eiv
rec
e iv
packet2
packet1
packet1
input buffer
zk
output buffer
packet1
packet2
packet2
output buffer
d
packet1
host k
n
se
z1
d
packet1
n
se
packet1
...
host 1
nd
se
e
host 0
input buffer
output buffer
bus
Three tasks
Host task
Input handler task
Request
se
n
dp
ac
ke
t
r
ffe
to
o
utp
ut
b
uff
er
n
se
Broadcast task
d
et
ck
pa
to
u
tb
pu
t
ou
broadcast packet to other hosts
Incoming packet fom other hosts
Contents
•
•
•
•
•
Informal explanation of the protocol
Purpose of our work
Model in UPPAAL
Results and analysis
Future work
Main global constants
• N (4): number of probes a host needs to send before using an IP
address.
• M (3): number of available IP addresses.
• k (2): number of hosts in the network.
• d (2): time interval between the sending of consecutive probes.
• D (1): upper bound on the transmission time delay.
• S(10):number of packets the output buffer can accommodate
Global variables for output buffer
•
int[0,3] OutBType[S][k];
This array denotes packet type in output buffer. Let h be an integer denoting
packet number stored in output buffer and let i be a host. Then:
OutBType[i][h]==0 means there is no packet on position h in i’s output
buffer.
OutBType[i][h]==1 means packet h in i’s output buffer is a probe.
OutBType[i][h]==2 means packet h in i’s output buffer is a gratuitous ARP.
OutBType[i][h]==3 means packet h in i ’s output buffer is a probe reply.
•
int[0,m] OutBIP[S][k];
This array contains the IP addresses of packets placed in output buffer.
OutBIP[i][h]==2 means the IP address contained in packet h in host i’s output
buffer is 2.
Host template
Broadcast template
Input handler template
Contents
•
•
•
•
•
Purpose of our work
Informal explanation of the protocol
Model in UPPAAL
Results and analysis
Future work
Results and analysis
• Two restrictions:
(1) Host will never choose the same IP address as
it failed before.
(2) Without message lost.
• For two hosts, property to be verified. Prop1:
A[](UseIP[0]==1 and UseIP[1]==1
and IP[0]==IP[1])
n
1
2
3
4
5
1
2
3
4
1
2
3
4
1
2
3
4
k==2, m==2, no message loss
d(s)
D(s)
1
1
1
1
1
1
1
1
1
1
2
1
2
1
2
1
2
1
21(0.21)
10 (1)
21 (0.21)
10 (1)
21 (0.21)
10 (1)
21 (0.21)
10 (1)
3 (0.3)
1 (0.1)
3 (0.3)
1 (0.1)
3 (0.3)
1 (0.1)
3 (0.3)
1 (0.1)
Satisfied
No
No
No
No
Yes
No
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Let r =d/D, When r>2 to any value of n it is impossible to reach a state
in which two hosts have acquired the same IP address, so host may
spend less time (d*n,n<=4) to acquire an IP address by changing d
and n. When r<=2, we can avoid the phenomenon that two hosts get
the same IP address by increasing n.
Three hosts
A Two hosts(host1 and host2) are using the same IP
address, the third host (host0) is used to trigger
collision.
B One host(host0) is using IP address “1”, two other
hosts attempt(host1 and host2) the same IP
address “1”
C Two hosts(host1 and host2) are using different IP
addresses, the third one(host0) needs to configure
an IP address.
Analysis (A)
• Both host1 and host2 will be forced to reconfigure
and we managed to give the upper bound on the
timing for various instances of the parameters.
• we found that it is possible one host(host1 or
host2) will never be killed.
n=1, d==1, D==4 and no change of other
parameters in the model.
Analysis(B)
• When r>2, for any n (n<=4), host0 will
successfully defend its IP address even when other
hosts(host1and host2)attempt the same IP address.
• When r<=2 and n is smaller, though host0 could
lose its IP address. However, it can be avoided by
increasing the number of probes n.
Analysis(C):
When k=3, under the constraint r>=3, to any value of n, host0 can’t
configure the same IP address as those of host1’ and host2’. In
addition, host1 and host2 will not lose their IP addresses.
t0
t  10x
probe
0
1
probe reply
t  10x  (0    x)
t : 0
t  10x  
probe
0
t  20x  
2
probe reply
t  30x   why r<3 Prop1 is invalid, while r=3 is valid. We can prove
that the latest time host receives the probe reply from the
time it sent out its probe is dd=3*D-infinitely small value.
Results of case C
• For a network with several hosts having used their different IP
addresses, one host connecting on it at some time, when r>=3, for any
value of probe numbers n, no two hosts can have the same IP address.
Any old host who has had its IP address initially will never lose its initial
I P address
• When r>=3, n=1 is ok for a new host to configure a new IP address.
Meanwhile, if d is more than three times of D, we can reduce d under
the constraint r>=3. Therefore the time for a new host to acquire a new
IP address can be decreased by decreasing these two parameters (d, n).
For a new host on the first try, in d*1~(d*1+2) seconds it can acquire a
new IP address..
Comments on 05.txt
“…shorter time values may be used on network technologies… On these network
technologies the recommended time values are: The host should first wait for a
random time interval selected uniformly in the range 0-200 milliseconds, and
then send four probe packets, waiting 200 milliseconds after each probe,
making a total delay of 800-1000 milliseconds before a chosen IP address may
be used…”.
• Why 200 milliseconds should be chosen? not others?
If transmission time delay D is still 1, the performance is not pleasant
since we can verify two hosts may have the same IP address.
• We deem that to let two hosts don’t have the same IP address has the
priority to be first satisfied, after that we can talk about the aspect that
how to reduce time to get a new IP address.
• Under the condition that r is satisfied by some constraint, d can be
decreased when D is smaller enough. Therefore, d is not necessary to
be 200 milliseconds, but may be the values (smaller or greater than 200
milliseconds) that meet the constraints we have found.
Comments on 05.txt
• In summary, according to different Ethernet we may improve the
performance by modifying the parameters d, and n under the constraint
condition of rate r. This is conformed to the following statement:
“…Link-layer network technologies that support ARP but operate at rates below
1Mb/s or latencies above one second may need to specify different values for
the following parameters described in Sections 2.2, 2.3 and 2.4:
(a) the number of, and interval between, ARP probes,
(b) the number of, and interval between, ARP announcements,
(c) the maximum rate at which address claiming may be attempted, and
(d) the time interval between conflicting ARP below which a host
MUST reconfigure instead of attempting to defend its address.
Contents
•
•
•
•
•
Purpose of our work
Informal explanation of the protocol
Model in UPPAAL
Verification results and analysis
Future work
Future work
• Reduce state space.
• We have found several parametric constraints to improve
performance, some have proved, for others how to prove them
?
• Need to send two gratuitous ARP packets, are there other
parametric constraints related with the number of gratuitous
ARP?
Thank you!