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 befektetési elemzést vagy 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, valamint a téves információkból eredő anyagi károkért a kriptomagazin.hu felelősséget nem vállal.
