Formal verification of distance vector routing protocolsRouting in a networkOutlineDistance-vector routing in RIPRIPCount to InfinityPoisoned reverseInfinity = 16ConvergenceSome definitionsMore definitionsSlide 12ToolsLemmas in convergence proofAbstractionAbstraction of universeBound on convergence timeWeak stabilityLemmas in Proof of timing boundProof continuedAODVSlide 22Searching for loop formationWays of loop formationGuaranteeing AODV loop freedomAbstractionAdding to abstractionConclusionFormal verification of distance vector routing protocolsRouting in a network(Find the cheapest route from Source to Destination)SourceDestinationL(i, j) = Cost of direct link i --- j.R(a, b) = Cost of route from a to b.R(a, b) = min{ L(a, k) + R(k, b) }Outline•RIP (Routing Information Protocol)–Internet routing protocol•AODV (Ad-hoc On-demand Distance Vector routing)–Used for mobile ad-hoc networking.Distance-vector routing in RIP5 7A B CA: 0B: 5C: ∞A: 5B: 0C: 7A: ∞B: 5C: 0InitiallyA: 0B: 5C: 12A: 5B: 0C: 7A: 12B: 5C: 0AfterexchangeRIPRouting table: Each node maintains the cost of route to every other nodeInitially: All nodes know cost to neighborsDesired Final Goal: All nodes know cost to all other nodeswhile(1) { Nodes periodically send their routing table to every neighbor; R(a, b) = min{ L(a, k) + R(k, b) };}Count to Infinity5A B CA: 0B: 5C: 12A: 5B: 0C: 7A: 12B: 5C: 0AfterexchangeC: 12C: 12+5=17C: 17+5=22Poisoned reverse5A B CC: ∞ Works for loops of two routers (adds more cases for Verification)RIP limitation: Doesn’t work for loops of three or more routersInfinity = 16•Since we can’t solve the loop problem–Set Infinity to 16•RIP is not to be used in a network that has more than 15 hops.Convergence•Convergence:–All nodes eventually agree upon routes•Divergence:–Nodes exchange routing messages indefinitely.•Ignore topology changes–We are concerned only with the period between topology changes.Some definitions•Universe is modeled as a bipartite graph–Nodes are partitioned into routers and networks–Interfaces are edges.–Each routers connects to at least two networks.–Routers are neighbors if they connect to same network•Actually, we can do away with bipartite graph by assuming that router = network (i.e. each network has one router) .•An entry for destination d at a router r has:–hops(r): Current distance estimate–nextR(r): next router on the route to d.–nextN(r): next network on route to d.More definitions•D(r) = 1 if r is connected to d = 1 + min{ D(s)| s is a neighbor of r }•k-circle around d is the set of routers: Ck = { r | D(r) ≤ k}•Stability: For 1 ≤ k ≤ 15, universe is k-stable if: (S1): Every router r in Ck has hops(r) = D(r) Also, D(nextR(r)) = D(r) – 1. (S2): For every router r outside Ck, hops(r) > k.Convergence•Aim of routing protocol is to expand k-circle to include all routers•A router r at distance k+1 from d is (k+1)-stable if it has an optimal route:– Hops(r)=k+1 and nextR(r) is in Ck.•Convergence theorem (Correctness of RIP)–For any k < 16, starting from an arbitrary state of the universe, for any fair sequence of messages, there is a time tk, such that the universe is k-stable at all times t ≥ tk.Tools•HOL (higher order logic)–Theorem prover (more expressive, more effort)•SPIN –Model checker (less expressive, easier modeling)•Number of routers is infinite–SPIN would have too many states–States reduced by using abstractionLemmas in convergence proof•Proved by induction on k.–Lemma 1: Universe is initially 1-stable. (Proved in HOL).–Lemma 2: Preservation of Stability. For any k < 16, if the universe is k-stable at some time t, then it is k-stable at any time t’ ≥ t. (Proved in HOL).–Lemma 3: For any k < 15 and router r such that D(r)=k+1, if the universe is k-stable at some time tk, then there is a time tr,k ≥ tk such that r is (k+1)-stable at all times t ≥ tr,k. (Proved in SPIN)–Lemma 4: Progress. For any k < 15, if the universe is k-stable at some time tk, then there is a time tk+1 ≥ tk such that the universe is (k+1)-stable at all times t ≥ tk+1. (Proved in HOL).Abstraction•To reduce state-space for SPIN•Abstraction examples:–If property P holds for two routers, then it will hold for arbitrarily many routers.–Advertisements of distances can be assumed to be k or k+1.•Abstraction should be:–Finitary: should reduce system to finite number of states– Property-preserving: Whenever abstract system satisfies the property, concrete system also satisfies the propertyAbstraction of universe Concrete system with many routersRouter processes UpdatesHop-count is {LT, EQ, GR}Advertiser sendupdatesAbstract system with 3 routershops > k+1hops = k+1hops < k+1Bound on convergence time•Theorem: A universe of radius R becomes 15-stable within time = min{15, R}* Δ. (Assuming there were no topology changes).After Δ weakly 2-stableAfter 2Δ weakly 3-stableAfter 3Δ weakly 4-stableAfter 4Δ weakly 5-stable… …After (R-1)Δ weakly R-stableAfter RΔ R-stableWeak stability•Universe is weakly k-stable if:–Universe is k-1 stable–For all routers on k-circle: either r is k-stable or hops(r) > k.–For all routers r outside Ck (D(r) > k), hops(r) > k.• By using weak stability, we can prove a sharp boundLemmas in Proof of timing bound•Lemma 5: Preservation of weak stability. For any 2 ≤ k ≤ 15, if the universe is weakly k-stable at some time t, then it is weakly k-stable at any time t’ ≥ t.•Lemma 6: Initial Progress. If the topology does not change, the universe becomes weakly 2-stable after Δ time.•Lemma 7: For any 2 ≤ k ≤ 15, if the universe is weakly k-stable at some time t, then it is k-stable at time t + Δ.Proof continued•Lemma 8: Progress. For any 2 ≤ k ≤ 15, if the universe is weakly k-stable at some time t, then it is weakly (k+1)-stable at time t + Δ.AODVSDSDRoutes are computed on-demand to save bandwidth.AODVA B D•Each route request has a sequence number for freshness.•Among two routes of equal freshness, smaller hop-count is preferred.•Property formally verified is loop freedom•Above conditions mean a lot of cases need to be checkedSearching for loop formation•The 3-node network shown previously, is run in SPIN.•(!((nextῺD(A)==B) /\ (nextD(B)==A))) •Four ways of loop formation are found.•Standard does not cover these cases.•Formal
View Full Document
Unlocking...