Kutatási cél
Az infokommunikációs hálózatok és számítástechnikai rendszerek biztonsága egyre fontosabb követelmény napjainkban. A hagyományos adatbiztonsági célokat (titkosság, integritás, és hitelesség) különböző biztonsági protokollok alkalmazásával érhetjük el. Sajnos azonban ezen protokollok tervezése messze nem triviális feladat, amit az is bizonyít, hogy több, széles körben alkalmazott biztonsági protokollban találtak súlyos biztonsági hibákat.
A biztonsági protokollok és rendszerek informális analízise számos hibalehetőséget rejt magában, ezért nem tekintjük kellően megbízhatónak ezt a hozzáállást. Kívánatos lenne a biztonsági analízis támogatása különböző formális analízis módszerekkel, melyek szisztematikus vizsgálatot tesznek lehetővé, ezért kevesebb hibalehetőséget rejtenek magukban. A formális módszerek alkalmazásának egy másik előnye, hogy lehetővé teszik az analízis automatizálását.
Kutatásunk célja, hogy olyan hatékony formális és automatikus ellenőrzési módszereket javasoljunk, amelynek segítségével a rendszer biztonságát tudjuk bizonyítani, vagy adott esetben a bennük rejlő biztonsági hibákat tudjuk detektálni. A közeljövőben kutatómunkánk a következő két fő témára fókuszál: (i) vezeték nélküli szenzor hálózatokra (WSN) tervezett transzport protokollok automatizált ellenőrzése; (ii) biztonsági útvonalválasztó protokollok automatizált ellenőrzése.
WSN transzport protokollok automatizált ellenőrzése
A vezeték nélküli szenzor hálózatok néhány alkalmazásában, mint például a multimédiás szenzor hálózatokban, a szenzoroknak QoS (Quality of Service) követelményt biztosítva kell nagy mennyiségű adatokat továbbítaniuk. Ezek az alkalmazások megkövetelik a transzport protokollok használatát, amik képesek biztosítani az adatok megbízható kézbesítését, valamint a megfelelő torlódáskezelést. Számos, vezeték nélküli szenzor hálózatokra optimalizált, transzport protokollt javasoltak eddig. A WSN transzport protokollok tervezésének két fő kritériuma a megbízhatóság és az energia hatékonyság biztosítása. Sajnos azonban a legtöbb létező WSN transzport protokoll tervezése során figyelmen kívül hagyták a biztonsági kérdéseket, és ennek az a következménye, hogy ezek a protokollok csak olyan ártalmatlan környezetben, ahol nincs szándékos támadás, tudják biztosítani a megbízhatósági és az energia hatékonysági követelményeket.
A WSN transzport protokollok elleni támadások két nagyobb csoportba sorolhatók: megbízhatósági (reliability) követelmény elleni támadások, és az úgynevezett energia kimerítő (energy depleting) támadások. A megbízhatósági követelmény elleni támadások akkor tekinthetőek sikeresnek, ha azokban a támadó eléri, hogy a csomagok (csomagrészek) észrevétlenül elvesznek. Az energia kimerítő támadások esetében a támadó célja, hogy rávegye a szenzorokat nagy energiát emésztő műveletek végrehajtására, s ezáltal kimeríti az elemüket. Ilyen támadás lehet, például amikor a támadó ráveszi a szenzorokat bizonyos csomagok (csomagrészek) felesleges újra küldésére.
A kutatás célja az első teljesen automatizált ellenőrzési módszer és szoftver eszköz kifejlesztése WSN transzport protokollok analizálására, és támadások detektálására.
Biztonsági útvonalválasztó protokollok automatizált ellenőrzése
Az ad-hoc hálózatok egyik jellemzője, hogy nincs előre definiált topológia a kommunikáló felek között. Emiatt mielőtt adatokat cserélnek a felek, felfedezik a köztük levő aktuális útvonalakat. Ezt a folyamatot útvonal választó protokollok specifikálják. Az útvonal választó protokollok ellen számos támadást publikáltak, amelyek során a támadó, kihasználva a protokollokban rejlő tervezési hibákat, elérheti azt, hogy a becsületes felek egy olyan útvonalon kommunikáljanak, ami valójában nem létezik. A nem létező útvonalakon való kommunikációk kritikusak mivel ezáltal a rendszer teljesítménye jelentősen csökkenhet. Az útvonal választó protokollokban rejlő hibák detektálása informálisan nagyon nehéz mivel a topológia változatossága miatt rengeteg eset fordulhat elő.
A kutatás célja egy a biztonsági útvonalválasztó protokollokra optimalizált, és teljesen automatizált ellenőrzési módszer és szoftver eszköz publikálása. Ezt a célt részben sikerült megvalósítani egy új és hatékony automatikus módszer és szoftver eszköz publikálásával. Azonban a jelenlegi módszer csak egy támadót (attacker node) feltételez, így nem képes detektálni azokat a trükkös támadásokat, amelyek több támadónak az együttműködését igénylik. A közeljövőben tehát a kutatási munka célja továbbfejleszteni az eddigi módszert, lehetővé téve az ellenőrzést a több együttműködő támadó esetére is.
Technikai leírás
WSN transzport protokollok automatizált ellenőrzése
A WSN transzport protokollok automatizált ellenőrzésére olyan formális módszerre van szükség, amely lehetővé teszi (szintaktikai és szemantikailag) a következő elemek modellezését: valós idejű rendszerek, probabilisztikus és elosztott működés, kriptográfiai primitívek és műveletek, a tároló cache működése, az üzenetküldés és fogadás műveletek, műveleti költségek. Sajnos azonban jelenleg egyik elérhető módszer és szoftver eszköz sem képes erre, így nem lehet őket közvetlenül alkalmazni erre a problémára. A legígéretesebb módszer a PAT process analysis toolkit, amely erős kifejező szintaktikával és szemantikával van felruházva. A PAT toolkit egy keretrendszernek tekinthető, amelyben sok ismert modell-ellenőrző algoritmust és formális nyelvi elemeket implementáltak. Egyik nagy előnye a többi eszközzel szemben, hogy könnyen bővíthető. Célunk tehát, hogy újabb, probléma specifikus, nyelvi elemekkel és algoritmusokkal bővítsük a PAT toolkit-et.
Az egyik nagy kihívás ebben a feladatban, hogy a vezeték nélküli szenzor hálózatokban küldött csomagok száma hatalmas, ami könnyen állapotrobbanáshoz vezethet, és amit az ellenőrző eszköz nem tud kezelni. Erre olyan módszert fogunk javasolni, ami az állapotokat valamint az adatstruktúrákat nem explicit módon, hanem szimbolikusan ábrázolja és tárolja. Ezenkívül úgy próbáljuk továbbcsökkenteni az ellenőrzés során keletkező hatalmas állapothalmazt, hogy az ekvivalens állapotbejárásokat azonosítjuk, és figyelmen kívül hagyjuk. Mindemellett, a bonyolultabb transzport protokollok ellenőrzéséhez szükségünk van a szuperszámítógép alkalmazására, amely elegendő memóriával és számítási kapacitással rendelkezik a hatalmas állapottér tárolásához és gyors bejárásához.
Biztonsági útvonalválasztó protokollok automatizált ellenőrzése
A biztonsági útvonalválasztó protokollok automatizált ellenőrzéséhez továbbfejlesztettük a jelenlegi módszerünket ahhoz, hogy képes legyen több együttműködő támadó esetet is kezelni. Egy olyan szoftver eszközt tervezünk, amelynél a protokollokat, mint inputot, processz algebra nyelven adjuk meg. Processz algebrát széles körben használják rendszerek működésének formális modellezésére. Legnagyobb előnye a többi informális specifikációs nyelvvel szemben, hogy a protokollok működésének minden lépését egyértelműen definiálja. A processz algebrai nyelven megadott protokollokat a program automatikusan lefordítja logikai szabályokra, amiken aztán automatizált következtetési lépéseket (rezolúciót) végez. A formális logikában előforduló rezolúciós módszerek közismerten alkalmasak automatizált ellenőrzők és deklaratív programnyelvek létrehozására.
Az egyik nagy kihívás ebben a feladatban, hogy mivel a támadók nagyszámú műveletet végezhetnek, így számuknak a növelése könnyen kezelhetetlen állapotrobbanáshoz vezethet az ellenőrzés során. Erre a problémára olyan megoldást fogunk javasolni, amivel redukálni tudjuk a támadók által generált állapotteret. Nevezetesen a több együttműködő támadót úgy fogjuk modellezni, mint egy darab szupertámadót, ami több helyről és több helyre tud adatokat szerezni és küldeni, ezzel vélhetően több ekvivalens állapotbejárást zárhatunk ki. Mindemellett, a bonyolultabb útvonalválasztó protokollok ellenőrzéséhez szükségünk van a szuperszámítógép alkalmazására, amely elegendő memóriával és számítási kapacitással rendelkezik a hatalmas állapottér tárolásához és a gyors bejárásához.
A várt eredmények összefoglalása
WSN transzport protokollok automatizált ellenőrzése
A kutatási témában várhatóan olyan ellenőrzési algoritmust és módszert fogunk javasolni és publikálni, amely teljesen automatizáltan, egy gombnyomásra, képes hatékonyan támadásokat detektálni az WSN transzport protokollok ellen vagy bebizonyítani, hogy biztonságosak. Szeretnénk legalább egy cikket publikálni ebben a témakörben. Elsősorban egy konferenciacikket tervezünk benyújtani, de ha úgy adódik, akkor kibővítjük folyóiratcikkre.
A biztonsági útvonal választó protokollok automatizált ellenőrzése
A kutatási témában várhatóan olyan módszert és szoftver eszközt fogunk javasolni és publikálni, amely képes több együttműködő támadók esetére is teljesen automatizáltan ellenőrizni. Az eredményeket legalább egy konferenciacikk formájában tervezzük publikálni.
Az elérni kívánt eredmények jelentősége, alkalmazása
WSN transzport protokollok automatizált ellenőrzése
Legjobb tudomásunk szerint eddig még nem publikálták olyan módszert, amely automatizáltan ellenőriz WSN transzport protokollokat. A probléma megoldására ezért elsőként szeretnénk megoldást javasolni. Egy további lényeges jelentősége a várható eredménynek, hogy következő lépésként úgy lehet a módszert továbbfejleszteni, hogy képes legyen általánosabb, nem csak vezeték nélküli szenzor hálózatokra tervezett, transzport protokollokat is ellenőrizni. Mivel a transzport protokollok széles körben elterjedtek és igen bonyolultak így informálisan nehéz támadásokat detektálni, így egy automatizált módszernek nagyon nagy jelentősége van. A javasolt automatizált ellenőrzési módszert a gyakorlatban alkalmazni fogjuk ismert WSN transzport protokollok, mint például a DTSN (Distributed Transport Protocol for Sensor Networks) és SDTP (Secured Distributed Transport Protocol), ellenőrzésére. Előbbi esetben várhatóan támadásokat találunk, míg utóbbi esetben a protokoll biztonságosságának bizonyítását várjuk.
A biztonsági útvonal választó protokollok automatizált ellenőrzése
Legjobb tudomásunk szerint eddig még nem javasolták olyan módszert, amely képes a biztonsági útvonalválasztó protokollok automatizált ellenőrzésére, több együttműködő támadó esetén. Az eddigi cikkek és munkák csak olyan megoldásokat javasoltak, amik egy speciális (korlátozott erejű) támadót képesek kezelni. Ezenkívül utaltak arra, hogy a több együttműködő támadó esetének a kezelése egy nagyon bonyolult feladat, mert az ad-hoc hálózatok és a támadók ereje miatt nehéz elkerülni az állapotrobbanást. Reményeink szerint az optimalizálási lépésekkel és a szuperszámítógép alkalmazásával képesek leszünk leküzdeni ezt a problémát. A javasolt módszert a gyakorlatban alkalmazzuk publikált útvonalválasztó protokollok ellenőrzésére, mint például az ismert Ariadne protokoll és az endairA protokoll ellenőrzésére. Elvárásainknak megfelelően a módszer képes lesz új (eddig nem ismert) támadások detektálására, aminek óriási jelentősége lesz. Tudniillik például, az endairA protokollra bebizonyították, hogy egy támadó esetén biztonságos, de több együttműködő támadó esetén még előfordulhat támadás.
Projekt előrehaladási jelentés
WSN transzport protokollok automatizált ellenőrzése
A vezeték nélküli szenzor hálózatok néhány alkalmazásában, mint például a multimédiás szenzor hálózatokban, a szenzoroknak QoS (Quality of Service) követelményt biztosítva kell nagy mennyiségű adatokat továbbítaniuk. Ezek az alkalmazások megkövetelik a transzport protokollok használatát, amik képesek biztosítani az adatok megbízható kézbesítését, valamint a megfelelő torlódáskezelést. Sajnos azonban a legtöbb létező WSN transzport protokoll tervezése során figyelmen kívül hagyták a biztonsági kérdéseket, és ennek az a következménye, hogy ezek a protokollok csak olyan ártalmatlan környezetben, ahol nincs szándékos támadás, tudják biztosítani a megbízhatósági és az energia hatékonysági követelményeket.
Eddigi munkánk során egy teljesen új biztonsági transzport protokollt, az SDTP protokollt, dolgoztunk ki. A protokoll olyan ismert kriptográfiai primitíveknek, mint a hash-lánc és a Merkle-fa, egy új kontextusban való alkalmazását foglalja magába, ami nagyon hatékonnyá teszi a működését. Másrészt egy általunk javasolt automatizált, biztonsági ellenőrzési módszerrel bebizonyítottuk, hogy a protokoll biztonságos. Az automatizált ellenőrzési módszerünk szimbólikus modell-ellenőrzés és temporális logika alkalmazásán alapul. Az eredmények publikálásra kerültek.
Biztonsági útvonalválasztó protokollok automatizált ellenőrzése
Legjobb tudomásunk szerint eddig még nem javasoltak olyan módszert, amely képes a biztonsági útvonalválasztó protokollok automatizált ellenőrzésére, több együttműködő támadó esetén. Az eddigi cikkek és munkák csak olyan megoldásokat javasoltak, amik egy speciális (korlátozott erejű) támadót képesek kezelni. Ezenkívül utaltak arra, hogy a több együttműködő támadó esetének a kezelése egy nagyon bonyolult feladat, mert az ad-hoc hálózatok és a támadók ereje miatt nehéz elkerülni az állapotrobbanást.
Eddigi munkánk során egyrészt javasoltunk egy új, általunk kidolgozott, algebrai nyelven és logikai dedukción alapuló algoritmust az automatizált biztonsági ellenőrzésre. A javasolt elméleti módszert JAVA nyelven implementáltuk, és sikeresen alkalmaztuk ismert protokollok (SRP, Ariadne protokollok) elleni támadások detektálására. A munkát publikáltuk technikai riport formájában, és hamarosan egy újság cikk formájában is.
