Informatikai tudományok doktori iskola

BME VIK, Híradástechnikai Tanszék, Villamosmérnöki és Informatikai Kar

Témavezető: Dr. Buttyán Levente

Biztonsági protokollok formális analízise

A kutatási téma néhány soros bemutatása

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 ezen protokollok tervezése komoly 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 ezt a megközelítést nem tekintjük kellően megbízhatónak. 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 ellenőrzés automatizálását.

Kutatásom célja, hogy  olyan hatékony  formális és automatikus ellenőrzési módszereket javasoljak, amelynek segítségével a rendszer biztonságát tudjuk bizonyítani, vagy adott esetben a biztonsági hibákat tudjuk detektálni.  Eddigi kutató munkám három fő témája a következő: biztonsági API-k formális analízise; biztonságos útválasztó protokollok automatizált ellenőrzése; és állapottartó tűzfalak hibás konfigurálásának automatizált vizsgálata. 

A kutatóhely rövid bemutatása

A kutatásomat a Híradástechnikai tanszéken található CrySyS  Adatbiztonság Laboratóriumban  végzem, amely nemzetközi szinten kiemelkedő és elismert kutatást és oktatást folytat a kriptográfia és rendszerbiztonság területén. A laboratórium vezetői tudományos konzulensem, Dr. Buttyán Levente  és Dr. Vajda István. 

A laboratórium fő kutatási területei a vezeték nélküli hálózatok és rendszerek valamint a beágyazott rendszerek biztonsága. Bővebb információk a laboratóriumról itt találhatók.          

A kutatás történetének, tágabb kontextusának bemutatása

A hardver biztonsági modulok (HSM) rendkívül fontos szerepet játszanak olyan területeken mint  a banki ATM hálózatok vagy az elektronikus kereskedelem.  A HSM-ek bontásvédettek emiatt alkalmasak titkos adatok, például kriptográfiai kulcsok tárolására. A HSM-ek elleni támadások célja a bennük tárolt titkos adatok megszerzése. A klasszikus támadási módszerek  fizikai támadások, amelyek hátránya, hogy költséges berendezéseket igényelnek. A közelmúltban azonban megjelentek a jóval kisebb költségű szoftveralapú támadók, amelyek a HSM alkalmazásprogramozói felületében (API) rejlő hibákat aknázzák ki. A bankok által használt több HSM-típus elleni API-támadás során sikerült a felhasználók PIN kódját megszerezni [3,5]. Mivel az API-k komplexek, informális elemzésük általában nehéz feladat.(Bővebben)

Az ad-hoc hálózatok egyik jellemzője, hogy nincs előre definiált topológia a kommunikáló felek között, ezért az adatcsere előtt a feleknek fel kell deríteniük a köztük levő aktuális útvonalakat. Ennek folyamatát az útválasztó protokollok specifikálják. Számos, útválasztó protokollok elleni támadást publikáltak, amelyek során a támadó, kihasználva a protokoll gyengeségét elérheti azt, hogy a becsületes felek tudtukon kívül olyan útvonalon próbáljanak kommunikálni, amely valójában nem létezik. A nem létező útvonalakon való kommunikációk azért kritikusak, mert ezáltal a rendszer teljesítménye jelentősen csökkenhet [9].  Az útválasztó protokollok hibáinak megtalálása informálisan nagyon nehéz, mivel a topológia változatossága miatt nagyon sok eset fordulhat elő. (Bővebben)

A  tűzfalak  fontos szerepet játszanak a hálózatok közötti forgalom adott stratégia alapján történő szabályozásában. A tűzfalak azonban csak megfelelően konfigurálva hatékonyak, amikor a kívánt stratégiát valósítják meg. A tűzfalak működését a rendszergazdák által szerkesztett szabályhalmaz  határozza meg. A szabályok nagy száma, a köztük lévő komplex összefüggések és a szabályokat frissítő több rendszergazda miatt előfordulhat inkonzisztencia a szabályok között, ami biztonsági hibákhoz vezethet [6,7]. (Bővebben)

    Mind a három területen szükség van tehát formális és automatikus ellenőrző módszerekre.

       

A kutatás célja, a megválaszolandó kérdések

Kutatásom egyik célja, hogy mindhárom kutatási területen hatékony formális és automatizált analízis módszert javasoljak, és annak gyakorlati alkalmazását bemutassam. Mindhárom területen azonban komoly kihívások vannak:   

A gyakorlatban a biztonsági API-k több ezer függvényhívást tartalmazhatnak, ami nagy állapotteret generál az ellenőrzés során. Ezenkívül a függvények speciális műveleteket tartalmaznak, ami nagyban megnehezíti a formális modellezést. A korábban publikált módszerek nem elég hatékonyak, ezért célom ezeknél hatékonyabb megoldást keresni. (Bővebben)      

Mivel az ad-hoc hálózatok topológiája változhat, az automatizált ellenőrzés során nagyszámú topológiát kell figyelembe venni. Emellett az eddig ismeretlen támadások észleléséhez erős támadó modelljét kell feltételeznünk ahol a támadó(k) bármit megtehet(nek). Ez akkora állapotteret indukál, amelyet egy számítógép gyakran nem tud vizsgálni. Az eddig közzétett megoldások nem működnek tetszőleges topológia és erős támadó modell mellett, ezért célom elsőként ilyen megoldást javasolni. (Bővebben)         

Az állapottartó tűzfalak dinamikus jellege miatt az ellenőrzés során óriás méretű esethalmazt kell figyelembe venni, valamint a tűzfalszabályok olyan elemeket tartalmaznak amiknek a  modellezése nem egyértelmű. Az eddigi megoldások a statikusabb állapotmentes tűzfalak esetével foglalkoztak. Célom olyan megoldást javasolni, amely hatékonyan kezeli a nagyméretű állapothalmazt és lehetővé teszi állapottartó tűzfalak ellenőrzését. (Bővebben)

        

Módszerek

A biztonsági API-k formális ellenőrzésére egy algebraalapú módszert javasoltam, legjobb tudomásom szerint elsőként. A jól ismert spi-kalkulust [2] és az erre épülő automatikus ProVerif [1] eszközt alkalmaztam. A spi-kalkulust és a ProVerif eszközt eredetileg nem API-k ellenőrzésére, hanem biztonsági protokollok analízisére fejlesztetették ki. Kutatásom során megmutattam, hogy az említett módszerek egy kis változtatással alkalmazhatóak egy újabb területen, a biztonsági API-k formális vizsgálatára is.  Módszerem előnye más, nem algebrai módszerekkel szemben az, hogy sokkal kifejezőbb modellezési nyelvet használ és egyben hatékonyabb automatizált ellenőrzést nyújt. (Bővebben) 

Az útválasztó protokollok formális ellenőrzésére egy algebrán és formális logikán alapuló módszert javasoltam. Célom egy, az útválasztó protokollokra optimalizált,  új algebrai nyelv és  új hatékony automatizált ellenőrző eszköz keresése. Korábban ilyen nyelv és eszköz nem volt, és az irodalomban található módszerek általános célú modellellenőrző eszközöket használtak útválasztó protokollok ellenőrzésére. Mivel az általános célú  modellellenőrzők nem ad-hoc hálózatokra lettek kifejlesztve, hiányzik bennük az útválasztó protokollok specifikálásához szükséges legtöbb modellezési elem. Ezenkívül, a bennük implementált ellenőrzési algoritmus nincs optimalizálva az útválasztó protokollokhoz, így a javasolt megoldásomnál lassabb ellenőrzést nyújtanak. Módszerem egyrészt a három ismert algebra, a CMAN, az alkalmazott pi-kalkulus és az omega-kalkulus [10,11,12] kombinálásából és bővítéséből áll, másrészt a hatékony ProVerif eszköz módosítása. (Bővebben)

Az állapottartó tűzfalak szabályhalmazaiban található inkonzisztenciák detektálására egy automatizált ellenőrző módszert javasoltam  az ismert FIREMAN [8] eszköz  használatával. A FIREMAN eszközt az állapotmentes tűzfalak szabályhalmazaiban található inkonzisztenciák detektálására javasolták. Az állapotmentes  tűzfalaktól eltérően az állapottartó tűzfalak szabályhalmaza állandóan változik működésük során, és emiatt utóbbiak ellenőrzése sokkal nehezebbnek tűnhet. Publikációmban megmutattam, hogy ez nem feltétlenül igaz. Megmutattam, hogy a sokkal bonyolultabb tűnő állapottartó tűzfalak ellenőrzése visszavezethető az állapotmentes esetre, ahol a FIREMAN eszköz már alkalmazható. (Bővebben)

Eddigi eredmények

A biztonsági API analízisére egy matematikailag precíz és automatizált módszert javasoltam [18,19,22,25]. Módszeremet a SeVeCom - Secure Vehicular  Communication EU kutatási projektben alkalmaztam először, amely a járművek  közti biztonságos kommunikációt hivatott megoldani a balesetek megelőzése végett. A  biztonságos kommunikációhoz kriptográfiai protokollokat alkalmaznak, amelyek titkos kulcsokat használnak. A titkos kulcsok tárolására minden autóba hardver biztonsági modult (HSM) szerelnek. Módszeremmel az ezekhez a modulokhoz implementált biztonsági API-t analizáltam. (Bővebben) 

Az útválasztó protokollok formális ellenőrzésére egy új, algebrán és formális logikán alapuló, automatizált ellenőrzőt javasoltam [21,23,24, 26]. Módszerem egyik előnye, hogy ad-hoc hálózatokra optimalizált, szintaktikai és szemantikai modellezési nyelvet  és hatékony automatizált ellenőrzési algoritmust biztosít. A javasolt automatizált ellenőrzőt az ismert útválasztó protokollok, az SRP [13] és az Ariadne [14] protokollok, vizsgálatára használtam. Alkalmazták módszeremet a WSAN4CIP- Securing Tomorrow's Critical Infrastructures EU kutatási projektben is. (Bővebben)

 

Az állapottartó tűzfalak szabályhalmazaiban található inkonzisztenciák detektálására egy automatizált ellenőrző módszert és szoftver eszközt javasoltam [20]. Módszeremmel a kutató laboratóriumunk tűzfalát ellenőriztem.  (Bővebben)                

Várható impakt, további kutatás

Eddigi eredményeim nagyon jó visszajelzéseket kaptak mind a tanszéki kollégáktól, mind a cikkeim bírálóitól. Ezek azonban főként elméleti eredmények, és a jövőben szeretnék a gyakorlatban is alkalmazni módszereimet. Módszereim hatékonyságát szeretném növelni, és a vállalatok tűzfalait, illetve a bankok által használt  biztonsági API-kat velük ellenőrizni.

Úgy gondolom, hogy a  biztonsági API-analízis területe elméleti szempontból nagyon ígéretes, mivel számos új kutatási irány fogalmazható meg. API-támadások ugyanis nem csak hardver biztonsági modulok esetén fordulnak elő, hanem számos más területen. Módszeremet olyan irányban szeretném bővíteni, hogy közvetlenül használható legyen más API-k, például webes, facebook  és android alkalmazásfejlesztők számára készült API-k vizsgálatára.

Végül, jelenleg egy negyedik területen is kutatok: a transzport protokollok automatizált biztonsági ellenőrzésének problémáján.  

Saját publikációk, hivatkozások, linkgyűjtemény

Hivatkozások listája.

[1] M. Abadi and B. Blanchet, Analyzing Security Protocols with Secrecy Types and Logic Programs, Journal of the ACM (JACM), 52(1):102–146, 2005. január (PDF)

[2] M. Abadi and A. Gordon, A calculus for cryptographic protocols: the Spi calculus, Technical Report SRC RR 149, Digital Equipment Corporation, Systems Research Center, 1998. január (PDF)

[3] R. Anderson, M. Bond, J. Clulow, and S. Skorobogatov, Cryptographic processors – a survey, Technical Report UCAM-CL-TR-641, University of Cambridge, Computer Laboratory, 2005. augusztus (PDF)

[4] B. Blanchet, Automatic Proof of Strong Secrecy for Security Protocols, IEEE Symposium on Security and Privacy, 86–100, Oakland, California, 2004. május (PDF)

[5] M. Bond, Understanding security APIs, PhD thesis, University of Cambridge, 2004 (PDF)

[6]  E. Al-Shaer and H. Hamed, Design and Implementation of Firewall Policy Advisor Tools, Technical Report CTI-techrep0801, School of Computer Science Telecommunications and Information Systems, DePaul University, 2002. augusztus (PDF)

[7] Ehab Al-Shaer, Hazem Hamed, Raouf Boutaba and Masum Hasan, Conflict Classification and Analysis of Distributed Firewall Policies, IEEE Journal on selected areas in communications, 23. kötet, 10. szám, 2005. október (PDF)

[8] L. Yuan, J. Mai, Z. Su, H. Chen, C. Chuah, and P. Mohapatra, FIREMAN: A toolkit for firewall modeling and analysis. IEEE Symposium on Security and Privacy, 199–213, 2006 (PDF)

[9] Gergely Ács, Secure Routing in Multi-hop Wireless Networks, PhD Thesis. 2009 február, BME (PDF)

[10] C. Fournet, M. Abadi, Mobile values, new names, and secure communication,  Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages,104–115,  2001 (PDF)

[11] A. Singh, C. R. Ramakrishnan, S. A. Smolka, A process calculus for mobile ad hoc networks, Sci. Comput. Program., 75(6) :440–469, 2010 (PDF)

[12] J. C. Godskesen, A calculus for mobile ad hoc networks. COORDINATION Journal, 132–150, 2007 (PDF)

[13] P. Papadimitratos, Z. Haas, Secure routing for mobile ad hoc networks, Networks and Distributed Systems Modeling and Simulation, 2002 (PDF)

[14] Y.-C. Hu, A. Perrig, D. B. Johnson, Ariadne: a secure on-demand routing protocol for ad hoc networks, Wirel. Netw., 11(1-2):21–38, 2005 (PDF)

Saját publikációk

Konferenciák és folyóiratok

[18] L. Buttyán, T. V. Thong, Security API analysis with the spi-calculus, Hiradástechnika, LXIII. kötet, 1. szám, 2008, 16–21. (PDF) 

[19] L. Buttyán, T. V. Thong, Biztonsági API analízis a spi-kalkulussal, Hiradástechnika, LXII. kötet, 8. szám, 2007, 43–49. (PDF) 

[20] L. Buttyán, G. Pék, T. V. Thong, Consistency verification of stateful firewalls is not harder than the stateless case, Infocommunications Journal, LXIV. kötet, 2009/2-3. szám, 2–3, 2009 (PDF)

[21] L. Buttyán, T. V. Thong, Formal verification of secure ad-hoc network routing protocols using deductive model-checking, IFIP Wireless and Mobile Networking Conference (WMNC’2010). (PDF)

[22] F. Kargl, P. Papadimitratos, L. Buttyan, M. Mueter, E. Schoch, B. Wiedersheim, Ta Vinh Thong, G. Calandriello, A. Held, A. Kung, J.-P. Hubaux, Secure Vehicular Communication Systems: Implementation, Performance, and Research Challenges, IEEE Communications Magazine, 46. kötet, 11. szám, 2008. november (PDF)

[23] L. Buttyán, T. V. Thong, Formal verification of secure ad-hoc network routing protocols using deductive model-checking, Periodica Polytechnica Journal, 2011 (PDF)

[24] T. V. Thong, L. Buttyán, On automating the verification of secure ad-hoc network routing protocols, Telecommunication Systems Journal, 2011 (PDF)                                                               

Egyéb

[25 ] T. V. Thong, Security API analysis with the spi-calculus, 2008, BME. (PDF)

[26] L. Buttyán, T. V. Thong, Formal verification of secure ad-hoc network routing protocols, 2010 (PDF)