A Concept of Automated Vulnerability Search in Contactless Communication Applications

Návrh a implementace bezpečných aplikací, které využívají bezkontaktní komunikaci, je těžké, i když je použit bezpečný hardware. Mnoho současných bezkontaktních zařízení má verifikovánu bezpečnost na vysoké úrovni, nicméně nesprávná implementace komunikačního protokolu může vést k úniku citlivých informací, přestože samotný protokol je také bezpečný. V tomto článku představujeme koncept automatického hledání zranitelností v implementaci protokolu pomocí verifikačních metod, který by měl pomoci vývojářům verifikovat jejich aplikace. Dále ukazujeme jednoduchý příklad možného útoku na zdánlivě bezpečný platební protokol, který je implementován pomocí zdánlivě bezpečné čipové karty, abychom ukázali způsob, jakým může útočník využít chybu v implementaci. Zranitelnost, kterou může útočník využít, může být v jednom příkazu, nebo v kombinaci příkazů, které nejsou zranitelné samy o sobě. Není jednoduché najít takové kombinace manuálně, zde se mohou použít automatizované verifikační metody. Složité zranitelnosti se dají nalézt pomocí model checkingu. Chtěli jsme ukázat, že útočník nemusí mít k dispozici zdrojové kódy, tak jsme vyvinuli platformu pro analýzu protokolu z bezkontaktní komunikace. Tato platforma umožňuje odposlech, změnu dat a dokáže emulovat obě zúčastněné strany. Když je pomocí model checkingu nalezena zranitelnost, může být proveden útok. Útok je buď úspěšný, čímž se potvrdí nalezení zranitelnosti, nebo neúspěšný, potom se zpřesní model a můžeme znovu použít model checking.