PA159, přednáška 3 9. 10. 2009 Co jsme dělali minule... • Popis AP notace + příklady • Elementární složky protokolů pro zajištěný přenos – typy potvrzování – řízení toku (dle příjemce, dle kapacity sítě) • TCP – základní chování – problémy na tlustých dlouhých linkách ... a co nás dnes čeká • Verifikace protokolů v AP notaci • Směrování – elementy směrovacích protokolů – distance vector protokoly – link state protokoly • Běžné směrovací protokoly – OSPF, BGP Verifikace protokolů Verifikace protokolu • Chceme dokázat žádané chování protokolu • Minimalistická verifikace programů – anotace • kdykoli program dosáhne nějaké definované místo v kódu, hodnoty proměnných splňují nějaký predikát – ukončení • obecně nerozhodnutelné • Minimalistická verifikace protokolů – uzávěra (closure) – opakování (recurrence) Uzávěra (closure) • stavový predikát r – vrací true nebo false • r-stav – stav, v němž je hodnota predikátu r rovna true • uzávěra – stavový predikát r je uzávěra iff • alespoň jeden stav protokolu P je r-stav • každý běh protokolu P začínající v r-stavu je nekonečný a všechny jeho stavy jsou r-stavy Uzávěra (2) • uzávěra r – definuje neprázdnou uzavřenou doménu běhu protokolu P – doména má alespoň jeden stav vyskytující se v protokolu nekonečněkrát Opakování (recurrence) • přechod (b,t) – b ... predikát obsahující pouze lokální proměnné procesu P t ... akce téhož procesu P – (b,t) je povoleno ve stavu r iff (b Ù stráž(t)) = true • redukovaná množina přechodů – každý pár různých přechodů má různé akce – redukce: (b[1],t), (b[2],t) ® (b[1]  b[2], t) Opakování (2) • T ... redukovaná množina přechodů v P r ... uzávěra v P • T se opakuje v P iff " běhy (stav1; akce1; ...) kde stav1 je r-stav splňují podmínku: (b,t)T. i. j>i. (b,t) je povoleno ve stavu stav[j ]a akce[j] je t • pokud se T opakuje uvnitř r v P a vykonávání P začíná v r-stavu, pak alespoň jeden přechod z T bude vykonáván nekonečněkrát Verifikace • Vlastnosti protokolu jsou popsány – r je uzávěra v P – T[1] se opakuje uvnitř P ... T[n] se opakuje uvnitř P • r definuje uzavřenou doménu běhu protokolu a T[i] definují přechody, z nichž se alespoň jeden vyskytuje nekonečně často • Tyto 2 vlastnosti potřebujeme ověřit. Verifikace uzávěry • Postup důkazu 1. svědek (witness): ukázat, že protokol P má r-stav 2. živost (liveness): dokázat, že pro " r-stavy existuje alespoň jedna povolená akce (což garantuje, že r-stav nemůže být koncovým stavem konečného běhu protokolu) 3. stabilita (stability): dokázat, že pokud je v r-stavu povolená nějaká akce, pak tato akce vede do r-stavu Verifikace opakování • Komplement T º ~T – pro redukovanou množinu přechodů T – ~T = { (~b,t) | $ přechod (b,t) v T } È { (true, t) | "t, pro něž není přechod v T } • Ohodnocovací funkce f pro r-stavy – fÎN pro " r-stavy – f(s) = k; $ss’; s,s’ ... r-stavy přechod snižuje f iff f(s’) < k přechod zvyšuje f iff f(s’) > k Verifikace opakování (2) • Postup důkazu: 1. žádný návrat (no-retreat): je-li v ~T povolen přechod v r-stavu procesu P, potom jeho provedení nezvýší f 2. postup (progress): pro k > 0: $ přechod v T, který je povolen v každém r-stavu kde f=k nebo $ přechod v ~T, který je povolen v každém r-stavu kde f=k a jeho vykonání snižuje f Verifikace opakování (2) • 3. závěr (conclusion) dokázat, že pro každý r-stav f=0, $ přechod v T, který je povolen • kombinace 1. a 2. říká, že v r-stavu f>0 buď bude vykonán nějaký přechod v T, nebo bude sníženo f • kombinace 1. a 3. říká, že pro r-stav f=0 bude vykonán přechod v T • ohodnocovací funkci je možné rozšířit i na vektor přirozených čísel Verifikace v případě výskytu chyb • Typy chyb: přeuspořádání, poškození nebo ztráta dat – chyby jsou definované jako akce • Verifikace zůstává stejná • Přibývá verifikovat stabilitu pro výskyt chyb – pokud je v r-stavu definována akce nebo chyba, tak jak pod akcí tak i pod chybou musí protokol P přejít do r-stavu Příklad • Převrácené kódování Manchester Příklad (2) Příklad (3) • Stavový predikát r = (first Ù dbl.c  seq.(data, i-1) = seq.(rcvd, j-1); even.c)  (~first Ù ~dbl.c  seq.(data, i-1) = seq.(rcvd, j-1); odd.c) • c ... obsah ch.p.q dbl.c = true iff #ch.p.q = 0  #ch.p.q mod 2 = 0 dbl.c = false iff #ch.p.q mod 2 = 1 Příklad (3) • Stavový predikát r = (first Ù dbl.c  seq.(data, i-1) = seq.(rcvd, j-1); even.c)  (~first Ù ~dbl.c  seq.(data, i-1) = seq.(rcvd, j-1); odd.c) Příklad (3) • Stavový predikát r = (first Ù dbl.c  seq.(data, i-1) = seq.(rcvd, j-1); even.c)  (~first Ù ~dbl.c  seq.(data, i-1) = seq.(rcvd, j-1); odd.c) • seq.(y, k-1) = empty pro k=0 seq.(y, k-1) = y[0];...;y[k-1] pro k>0 Příklad (4) • Podmínka svědka (tj. existuje r-stav): první stav: (i = 0 Ù #ch.p.q = 0  j = 0  first) ... splňuje • Podmínka živosti: akce v procesu p je vždy aktivována • Podmínka stability proces p má akci, která nemůže negovat r proces q vždy splňuje jeden ze dvou termů Příklad (5) • Definice T: T = { (first, t.q) } t.q ... je jediný přechod v q • Komplement: ~T = {(~first, t.q) , (true, t.p) } • Ohodnocovací funkce f = 0 if r Ù first  #ch.p.q > 0 1 if r Ù first  #ch.p.q = 0 2 if r Ù ~first  #ch.p.q > 1 3 if r Ù ~first  #ch.p.q = 1 Příklad (6) Příklad (6) • Podmínka žádného návratu: splněna - pouze přechody z T zvětšují f • Podmínka postupu: splněna - čtyři přechody nahoře • Podmínka závěru: splněna, dva přechody dole Elementy směrování Hierarchické směrování • Dělení adres: oblasti (region) - obvody (district) - procesy • rgn[x] definuje souseda, přes nějž se dostanu do regionu x dstr[y] definuje souseda, přes nějž se dostanu do obvodu y prs[z] definuje souseda, přes nějž se dostanu do procesu z – každý proces jednoznačně definován trojicí (region, obvod, proces) • up[k] definuje, jestli je soused k naživu Hierarchické směrování (2) RTMSG Použití implicitní brány Náhodné směrování • Příklad se směrovací tabulkou, kde pro každý cíl máme 2 možné uzly, přes něž se bude posílat rtb[d, 0] = nejaky_soused1 rtb[d, 1] = nejaky_soused2 Náhodné směrování (2) RTMSG Distribuované směrování • rtb[d] nejlepší soused pro směrování zprávy do p[d] cost[d] počet skoků při poslání zprávy přes p[rtb[d]] • počet procesů v síti je n, číslováno 0..n-1 => nekonečno můžeme definovat jako n • demonstrujeme na síti se všemi hranami ohodnocenými 1 • = distance vector směrování (např. RIP, BGP) Distribuované směrování (2) RTMSG SNDCOST • funkce NEXT(N, h) vrací následující prvek z množiny N po prvku h (umí množinou cyklit) • h je libovolný prvek z N UPDRTB • Aktualizace rtb[] a cost[] Backward learning routing RTMSG UPDRTB UPDRTB’ Udržování topologie • procesy si posílají zprávy st(cislo_procesu, up_pole, casova_znacka) • pro proces i – net[k,l] = true iff k-l jsou sousedi a spoj k-l obousměrně funguje vp[j] = true iff i-j jsou sousedi a up[j] = true ts[j] = maximální časová značka zprávy st(j, ...) Udržování topologie (2) Udržování topologie (3) Směrování v Internetu Základní úrovně směrování v Internetu • Směrování v podsítích/lokálních sítích • Směrování v autonomních systémech • Směrování mezi autonomními systémy • Páteřní směrování – páteř (backbone) je soubor speciálních směrovačů, které znají cestu do každé podsítě na Internetu (v rámci agregace adres) Směrování v lokální síti • IP.s - adresa odesílatele M.s - maska sítě odesílatele IP.d - adresa cíle • hledání nejdelšího prefixu ve směrovací tabulce – např. hledám 192.168.1.140 v: 192.168.0.0/16, 192.168.1.0/24, 192.168.1.128/25 Exkurze - rozborka adres sítí Směrování uvnitř AS • S ... autonomní systém r ... směrovač • směrovač zná – IP adresu a masku každé podsítě v S – pro každou podsíť s v S definuje nejlepší sousední směrovač pro předání – pro sítě t mimo S • explicitní záznamy pro sítě blízké S • implicitní záznam pro ostatní Směrování uvnitř AS (2) • Rozhodnutí, jestli IP.d leží v S v síti IP.s s maskou M.s • Směrovací algoritmy: – distance vector - např. RIP • distribuovaný směrovací protokol – link state - např. OSPF • protokol pro udržování topologie OSPF verze 2 • Definováno v RFC 2328 • Používá vysílání LS informací a Dijkstrův algoritmus • Každý směrovač získá kompletní mapu topologie AS (jako orientovaný graf!) a strom cest s nejmenší cenou • Nastavení ceny spoje (pokud všechny 1, tak je to i strom nejkratších cest) • Vysílání LS informací – číslo vyšší vrstvy v IP hlavičce: 89 – při změně stavu spoje – periodicky minimálně 1x za 30 min. OSPF verze 2 (2) • Zabezpečení zpráv mezi OSPF směrovači • Více cest se stejnou váhou – vyvažování zátěže – problém s přeuspořádáním paketů • Směrování multicastu – MOSPF (RFC1584) – využití znalostí topologie z OSPF pro konstrukci multicastových stromů OSPF verze 2 (3) • Hierarchizace jednoho AS – oblasti (areas) – vysílání LS informací je omezeno na oblast – pro směrovače v jiné oblasti AS je oblast black-box • Hraniční směrovače oblastí – jedna oblast uvnitř AS je označena jako páteřní – hraniční směrovače náleží do páteřní oblasti a do nejméně jedné další oblasti OSPF verze 2 (4) • Informace o ceně mezi oblastmi není přenášena jako informace o ceně spoje, ale jako kumulativní cena cesty • Páteřní směrovače v AS – náleží pouze do páteřní oblasti • Hraniční směrovače AS – používají OSPF (příp. I-BGP) dovnitř AS a BGP-4 na směrování mezi AS Směrování mezi AS • Typy autonomních systémů – koncové (stub) AS – multihomed AS – transit AS • Autonomous system number (ASN) (RFC1930) – 16-bitový identifikátor – koncové AS jej nemusí mít přiřazené – přiřazuje ICANN (www.icann.org) Internet Corporation For Assigned Names and Numbers BGP-4 • Path-vector protocol – nevyměňují se pouze ceny cest, ale celé cesty zahrnující všechny skoky • Pracuje na úrovni sítí, nikoli jednotlivých uzlů/směrovačů • Základem jsou oznamy (advertisments) – zasílají se přes point-to-point spoje – oznam obsahuje: adresu cílové sítě (CIDR) + atributy cesty (např. atribut path (seznam všech AS na cestě) a identita next-hop směrovače BGP-4 (2) • 3 základní operace – příjem a filtrování oznamů – výběr cesty – zasílání oznamů • Příjem a filtrování oznamů – peer směrovač hlásí, do jakých AS je schopen doručovat – předpokládá se, že peerové nelžou! – možnost filtrovat (např. takové cesty, kde AS-PATH je ASN vlastního AS - problém cyklů) BGP-4 (3) • Výběr cesty – z více možných cest z různých oznamů pro daný AS vybrat jeden, a jeho next-hop směrovač zapsat do směrovacích tabulek – způsob výběru definuje směrovací politika (SP) – když pro daný AS není nastavena SP, použije se nejkratší cesta – www.cisco.com/warp/public/459/25.shtml BGP-4 (4) • Zasílání oznamů – administrátor definuje politiku oznamů – umožňuje kontrolu nad tím, do jakých AS potečou data přes adminův AS • Politiky peerování – neexistují psané standardy – u typických komerčních ISP: přes AS tečou pouze ta data, která mají zdroj nebo cíl v daném AS – peerovací smlouvy jsou velký business ;-) BGP-4 (5) • Komunikace mezi BGP peery – potřeba spolehlivé komunikace (na rozdíl od OSPF, které si spolehlivost nad IP řeší samo) – TCP port 179 – 4 typy zpráv: OPEN, UPDATE, KEEPALIVE, NOTIFICATION • OPEN – ustavení spojení mezi BGP peery – obsahuje typicky autentizační informace – pozitivní odpověd na OPEN je KEEPALIVE BGP-4 (6) • UPDATE – šíření oznamů o cestách • oznámení, že lze přeze mne směrovat do daného AS • stažení takového oznamu (oznam je platný až do jeho explicitního stažení!) • KEEPALIVE – positivní odpověd na OPEN – udržování spojení • NOTIFICATION – oznámení o chybě nebo o ukončení spojení I-BGP • Distribuce informací o přilehlých AS mezi směrovači uvnitř AS – všechny směrovače uvnitř AS se považují za peery z pohledu I-BGP – I-BGP směrovače mohou oznamovat pouze cesty, které se dozvědely přímo od jiného I-BGP směrovače Velkosti BGP tabulek • Ukázka velikosti BGP tabulek: http://bgp.potaroo.net/ Proč rozlišovat mezi směrováním uvnitř AS a mezi AS? • Mezi AS hrají roli mnohem více následující faktory – politiky (protože typicky jde o peníze) – škálovatelnost (velikosti BGP tabulek) • Uvnitř AS hraje spíše roli výkon