Vitalik Buterin: Umělá inteligence a formální ověřování mohou kritický kód učinit nehacknutelným
Stručně
Vitalik Buterin tvrdí, že formální ověřování s pomocí umělé inteligence může matematicky prokázat správnost kódu a nabízí tak důvěryhodnou cestu k zabezpečení kritického softwaru před kybernetickými útoky poháněnými umělou inteligencí.
Spoluzakladatel Etherea Vitalik Buterin se nikdy nestyděl velkých nápadů. Jeho nejnovější esej se však vydává za hranice blockchainu a jde o něco, co by mohlo změnit základy samotné softwarové bezpečnosti: formální ověřování, praxi psaní matematicky ověřitelných důkazů o tom, že počítačový kód se chová přesně tak, jak má. Tváří v tvář stále silnější umělé inteligenci, která dokáže najít a zneužít softwarové chyby ve velkém měřítku, Buterin tvrdí, že tento staletí starý přístup k matematickým důkazům není jen užitečný – může být jedinou důvěryhodnou cestou k důvěryhodné digitální budoucnosti.
Tento argument je aktuální. Odhalování chyb s pomocí umělé inteligence rychle naklání hru ve prospěch útočníků. Kód, jehož kontrola dříve trvala týmům lidských auditorů týdny, lze nyní prohledat na zranitelnosti během několika minut. Některé hlasy ve světě bezpečnosti reagovaly na tuto realitu rezignovaně a naznačují, že deterministické softwarové záruky jsou v podstatě pryč, nebo že jedinou schůdnou reakcí je ústup za zdi uzavřeného zdrojového kódu. Buterin oba závěry rozhodně odmítá.
Jeho optimismus nespočívá v zbožném přání, ale ve specifickém technologickém spojení: umělé inteligence a formálního ověřování. Umělá inteligence dokáže generovat obrovské objemy kódu, včetně vysoce optimalizovaného nízkoúrovňového assemblerového kódu, jehož psaní by pro lidi bylo pracné. Formální ověřování pak může s matematickou jistotou ověřitelnou strojem dokázat, že tento kód má požadované vlastnosti. Výsledkem je, jak Buterin naznačuje, návrat k psaní maximálně efektivního kódu – takového, jaký programátoři psali před padesáti lety v raw assemblerovém kódu – ale tentokrát s připojeným důsledným důkazem správnosti. Výzkumník Yoichi Hirai to nazývá „konečnou formou vývoje softwaru“. Buterin se s tím přiklání.
Co formální ověření skutečně dělá – a co nedělá
Abychom pochopili Buterinovu argumentaci, je dobré si ujasnit, co je formální verifikace. V podstatě to znamená napsat matematické věty o vašem softwaru a poté tyto věty automaticky ověřovat. Místo testování, zda kód funguje na vzorku vstupů, dokážete, že funguje na všech možných vstupech, za daných určitých podmínek. defipředpoklady. Primárním nástrojem je zde programovací jazyk Lean, stále častěji používaný jak v čisté matematice, tak v softwarovém inženýrství. Mezi již probíhající projekty patří formálně ověřené implementace kryptografických protokolů, jako je výměna klíčů X3DH od Signalu, systémy ZK-STARK proof a dokonce i plnohodnotný EVM (virtuální stroj Ethereum) postavený přímo v sestavě RISC-V s připojenými důkazy správnosti.
Tohle je skutečně silné. Nejhorší softwarové chyby jsou často interakční chyby – chyby, které se nacházejí na hranici mezi dvěma subsystémy, které byly považovány za samostatně spolehlivé. Lidští auditoři prostě nedokážou udržet v paměti celý komplexní systém současně. Automatizovaný systém kontroly důkazů to dokáže. Formální ověřování je také jedinečně vhodné pro typy systémů, které Ethereum nejvíce potřebuje správně zvládnout: kvantově odolné podpisy, systémy s nulovými znalostmi a konsenzuální algoritmy – to vše jsou oblasti, kde jsou bezpečnostní vlastnosti koncepčně snadno stanovitelné, i když implementace jsou ďábelsky složité na sestavení.
Buterin si ale dává pozor, aby to nepřeceňoval. „Prokazatelná správnost“ neznamená to, co si většina lidí myslí. Důkaz pouze ukazuje, že kód splňuje formálně stanovenou specifikaci. Pokud je specifikace neúplná, je důkaz neúplný. Pokud kritické předpoklady zakotvené v důkazu v praxi neplatí – řekněme, že hardwarový postranní kanál uniká informace způsoby, které model hrozby nikdy nezohlednil – důkaz je stále platný, ale systém je stále nejistý. Historie nabízí střízlivé příklady: formálně ověřené kompilátory jazyka C se dodávaly s chybami; formálně ověřené kryptografické protokoly byly později prolomeny pod nepřátelskými modely, které jejich autoři nepředpokládali. Formální ověřování, zdůrazňuje Buterin, není zázračné řešení. Je to jedna z několika účinných technik a selhává, když je použita nedbale, částečně nebo se specifikací, která neodpovídá tomu, co uživatelé skutečně potřebují.
Cesta vpřed: Bezpečné jádro v kočárkovitém světě
Buterin se dostává k nuancem, ale skutečně nadějné vizi. Budoucnost softwarové bezpečnosti podle jeho názoru není světem, kde je veškerý kód dokonale ověřen – to není ani dosažitelné, ani nutné. Je to svět rozdělený mezi zpevněné, zmenšující se „bezpečné jádro“ a volnější, sandboxovou periferii. Periferní kód – aplikace, pluginy, skripty generované umělou inteligencí – může zůstat chaotický a náchylný k chybám. To je přijatelné, pokud běží s minimálními oprávněními a nemůže ohrozit jádro. Bezpečné jádro – jádra operačního systému, samotné Ethereum, kryptografická infrastruktura, základy IoT – musí být naopak drženo zcela jiného standardu a formální ověřování je klíčové pro jeho splnění.
V této architektuře umělá inteligence mění rovnici ne tím, že by kód ve výchozím nastavení byl bezpečnější, ale tím, že poprvé v historii umožňuje rigorózní ověřování. Ruční psaní důkazů je notoricky obtížné a formální metody po celá desetiletí zůstaly jen okrajovou disciplínou. Pokud však umělá inteligence dokáže napsat jak optimalizovanou implementaci, tak i doprovodný důkaz, s lidským dohledem zaměřeným úzce na kontrolu, zda uvedené věty skutečně zachycují to, na čem záleží, kalkulus se posouvá. Náročná práce s ověřováním se stává automatizovanou; lidská role se stává rolí specifikace a úsudku, nikoli dřiny řádek po řádku.
Podle Buterina je v sázce více než jen Ethereum nebo dokonce kryptoměny. Tradice cypherpunku – přesvědčení, že v digitální síti mají obránci strukturální výhodu, protože budování kryptografické ochrany je snazší než její prolomení – je ve skutečném ohrožení ze strany útočníků s využitím umělé inteligence. Formální ověřování v kombinaci s umělou inteligencí je jedním z mála dostupných nástrojů, které dokáží tuto výhodu obnovit. Ne odstraněním všech chyb všude, ale tím, že se nejdůležitější systémy skutečně prokazatelně zabezpečí proti formálně napadeným systémům. defitřída hrozeb. Ve světě stále autonomnější a stále schopnější umělé inteligence by to mohl být přesně ten druh tvrdé záruky, kterou potřebujeme.
Odmítnutí odpovědnosti
V souladu s Pokyny k projektu Trust, prosím vezměte na vědomí, že informace uvedené na této stránce nejsou určeny a neměly by být vykládány jako právní, daňové, investiční, finanční nebo jakékoli jiné formy poradenství. Je důležité investovat jen to, co si můžete dovolit ztratit, a v případě pochybností vyhledat nezávislé finanční poradenství. Pro další informace doporučujeme nahlédnout do smluvních podmínek a také na stránky nápovědy a podpory poskytnuté vydavatelem nebo inzerentem. MetaversePost se zavázala poskytovat přesné a nezaujaté zprávy, ale podmínky na trhu se mohou bez upozornění změnit.
O autorovi
Alisa, oddaná novinářka v MPost, specializuje se na kryptoměny, umělou inteligenci, investice a rozsáhlou oblast Web3. S velkým okem pro nové trendy a technologie poskytuje komplexní pokrytí, aby informovala a zapojila čtenáře do neustále se vyvíjejícího prostředí digitálních financí.
Další články
Alisa, oddaná novinářka v MPost, specializuje se na kryptoměny, umělou inteligenci, investice a rozsáhlou oblast Web3. S velkým okem pro nové trendy a technologie poskytuje komplexní pokrytí, aby informovala a zapojila čtenáře do neustále se vyvíjejícího prostředí digitálních financí.
