Vitalik Buterin május 18-án közzétett blogbejegyzésében arról írt, hogy a mesterséges intelligenciával támogatott formális verifikáció a kiberbiztonság egyik meghatározó eszközévé válhat. Az Ethereum társalapítója az Arklib projektet emelte ki példaként, amely egy formálisan ellenőrzött STARK-megvalósításon dolgozik.
Buterin a vitalik.eth.limo oldalon publikált írásában a formális verifikációt olyan matematikai bizonyítási módszerként írta le, amely biztosítja, hogy a szoftver pontosan a tervezett módon működjön. Megfogalmazása szerint a mesterséges intelligencia és a formális verifikáció kombinációja lehetővé teheti, hogy a fejlesztők még a támadók előtt azonosítsák a sérülékenységeket.
A bejegyzésben példaként említette a Claude Mythos nevű mesterségesintelligencia-modellt, amelyet az Anthropic fejlesztett. Buterin szerint az egyre fejlettebb MI-rendszerek felgyorsíthatják a sérülékenységek felderítését és kihasználását is. Az Anthropic 2026 márciusában erősítette meg a Claude Mythos létezését egy véletlen adatszivárgást követően, majd áprilisban korlátozott hozzáférésű előzetest tett elérhetővé partnerei számára.
A formális verifikáció korlátaira is figyelmeztetett
Buterin hangsúlyozta, hogy a formális verifikáció önmagában nem szünteti meg az összes kockázatot. A bizonyítási rendszerek figyelmen kívül hagyhatnak kritikus feltételezéseket, és nem feltétlenül fedik le a hardveres sérülékenységeket vagy más kapcsolódó támadási felületeket.
Arra is kitért, hogy a mesterséges intelligencia csökkenti a nagy mennyiségű szoftver előállításának technikai akadályait. Ez növelheti annak veszélyét, hogy nem megfelelően ellenőrzött vagy kevéssé ismert kód kerül éles rendszerekbe. Ennek ellenére úgy fogalmazott, hogy a formális módszerek alkalmazása a hagyományos szoftverfejlesztéshez képest mérsékelheti a súlyos biztonsági kockázatokat.
Buterin az Arklib projektet az Ethereum ökoszisztémában alkalmazott formális módszerek konkrét példájaként említette. Az Arklib egy nyílt forráskódú kezdeményezés, amely egy teljes mértékben formálisan ellenőrzött STARK-bizonyítási rendszer létrehozását tűzte ki célul. A STARK egy olyan kriptográfiai bizonyítási technológia, amelyet az Ethereum skálázási infrastruktúrájában is alkalmaznak.
Az Ethereum Foundation finanszírozást biztosított a Nethermind számára, hogy az Arklib projektben a Lean bizonyítási asszisztens segítségével formalizálják a FRI-protokollot. Buterin emellett olyan Ethereum Virtual Machine implementációkra is hivatkozott, amelyeket közvetlenül RISC-V assembly nyelven írtak és formálisan ellenőriztek.
Érdekes lehet: A Santiment szerint 11,2 százalékkal nőtt a nagy Bitcoin-tárcák száma
A kriptomagazin.hu oldalon található információk és elemzések a szerzők magánvéleményét tükrözik. A jelen oldalon megjelenő írások, cikkek nem valósítanak meg a 2007. évi CXXXVIII. törvény (Bszt.) 4. § (2). bek 8. pontja szerinti befektetési elemzést és a 9. pont szerinti befektetési tanácsadást. Bármely befektetési döntés meghozatala során az adott befektetés megfelelőségét csak az adott befektető személyére szabott vizsgálattal lehet megállapítani, melyre a jelen oldal nem vállalkozik és nem is alkalmas. Az egyes befektetési döntések előtt éppen ezért tájékozódjon részletesen és több forrásból, szükség esetén konzultáljon befektetési tanácsadóval!
A cikkekben megjelenő esetleges hibákért, téves információkból eredendő anyagi károkért a kriptomagazin.hu felelősséget nem vállal.
A cikkben előfordulhatnak partnerlinkek, amelyek után jutalékot kaphatunk.
