Ki lesz a következő? A rejtett hibák és az MI fenyegetése
Az ügy egyre több kérdést vet fel: ha ma már egy MI-modell néhány óra alatt ilyen hibát talál, vajon hány hasonló, láthatatlan veszély lapul a kriptovilág és a hagyományos banki rendszerek mélyén? Az Anthropic következő generációs modellje, amelyet hamarosan piacra dobhatnak, várhatóan még könnyebben fogja láncba fűzni és összekapcsolni a hibákat, ezért a biztonsági szakértők szerint a pénzügyi szektor egészének meg kell újulnia.
Az MI nem ellenség, hanem eszköz lehet
A neves kriptós befektetőcég, a Dragonfly, valamint ügyvezető partnere, Haseeb Qureshi azonban inkább lehetőséget látnak ebben, mint fenyegetést. Qureshi szerint, ha az MI képes hibát találni, az azért jó hír, mert így végre meg is javíthatja azt – méghozzá a formális verifikáció nevű eljárás segítségével. Ez a módszer matematikailag bizonyított, és minden, komoly következményekkel járó szoftver védelmét biztosíthatja hosszú távon.
A Dragonfly továbbra is bízik a Zcashben és abban, hogy az MI javítani fogja a kriptoipari szoftverbiztonságot. Más szakértők, például Ben Goertzel, a SingularityNET vezetője szerint ugyancsak masszív sérülékenységek bújhatnak meg a hagyományos banki rendszerekben, amelyeket az MI hamarosan felfedhet.
A formális verifikáció lehet a megoldás kulcsa
A formális verifikáció során matematikai tételbizonyításokat írnak – ezek ellenőrizhetők, így elvileg kizárhatók az olyan egyszerű, de veszélyes hibák, amilyet most is találtak. Vitalik Buterin, az Ethereum társalapítója is hangsúlyozta, hogy az MI-vel támogatott formális verifikáció a kibervédelem egyik legfontosabb eszközévé válhat. Qureshi is kiemelte: a formálisan ellenőrzött kriptográfiai szoftverekben a hibák gyakorlatilag megszűnnek, és ez az egyedüli út a mindenki által használt pénzügyi rendszerek védelméhez.
Ugyanakkor Goertzel azt is elmondta: bár például a Rust programnyelv jól ellenőrizhető lenne, a fejlesztők ritkán alkalmazzák ezt a módszert, mert jelentős pluszmunkával jár. Sőt, a Rust alapkönyvtáraiban még mindig nehezen ellenőrizhető, „nem biztonságos” elemek találhatók. Ezek átalakítása ugyan lassítja a szoftvert, de fejlett optimalizálási technikákkal, például „szuperkompilációval”, ellensúlyozható a teljesítményromlás.
Aszimmetrikus harc: a hackerek erősebbek?
A védekezés azonban nem egyszerű. Ronghui Gu, a CertiK biztonsági cég vezetője szerint jelenleg valódi MI-háború zajlik: a támadók egy-egy célpont – például egy okosszerződés – feltörésére hatalmas számítási kapacitást áldoznak. A biztonsági cégek viszont több száz ügyfelet kénytelenek egyszerre védeni, ezért náluk ez a koncentráció tetemes többletköltséget jelent.
Gu szerint csak úgy lehet felvenni a versenyt, ha automatizált szkennereket építenek a mindennapi fejlesztői folyamatokba, és minden új kódot kisebb, gyors, eseti vizsgálatokkal néznek át – a biztonság kulcsa pedig a matematikailag bizonyított helyesség lehet. Az igazi kihívás már nem az, ki talál hibát előbb, hanem az, ki tud gyorsabban és hatékonyabban védekezni az új típusú támadásokkal szemben.
Egyedül a formális verifikáció segíthet
Ahogy az MI egyre fejlettebb, hamarabb, gyorsabban és rutinosabban leplez majd le rejtett sebezhetőségeket, így minden fejlesztő legfontosabb feladata lesz, hogy ezek a hibák soha többé ne fordulhassanak elő. Josh Swihart, a volt Electric Coin Company vezérigazgatója szerint is: az igazán érdekes kérdés az, hogyan érjük el, hogy ezek a hibák örökre eltűnjenek. A legjobb válasz: a formális verifikáció.
