Biztonsági API analízis a spi-kalkulussal
Buttyán Levente, Ta Vinh Thong
buttyan@crysys.hu, thong@crysys.hu
CrySyS Adatbiztonsági Laboratórium
BME Híradástechnikai Tanszék
buttyan@crysys.hu, thong@crysys.hu
CrySyS Adatbiztonsági Laboratórium
BME Híradástechnikai Tanszék
Az API szintű támadások komoly veszélyt jelentenek a hardver biztonsági modulokra nézve, ezért fontos követelmény az API-ban rejlő biztonsági lyukak felfedezése és foltozása. Az API analízis egyik ígéretes iránya a formális verifikációs módszerek alkalmazása. Cikkünkben ezt az irányt követjük, s egy processz-algebra alapú API verifikációs módszert javaslunk, mely különösen alkalmasnak látszik a biztonsági API-k működésének formális leírására, a biztonsági követelmények precíz definiálására, és a megfogalmazott követelmények teljesítésének ellenőrzésére. Munkánk motiválása céljából ismertetünk nénány konkrét API szintű támadást is egy a gyakorlatban elterjedten használt hardver biztonsági modul ellen.