Výzkumníci Zcash zveřejnili soubor více než 2 700 strojově ověřených teorémů navržených k eliminaci neodhalitelných chyb padělání v připravovaném upgradu protokolu Ironwood. Práce, kterou zveřejnil tým stojící za kryptoměnou zaměřenou na soukromí, si klade za cíl matematicky dokázat, že nový kód nelze zneužít k vytváření falešných coinů bez odhalení.
Na co se teorémy zaměřují
Teorémy se soustředí na Ironwood, plánovaný upgrade pravidel konsenzu Zcash. Chyby padělání jsou třídou zranitelností, které útočníkovi umožňují vytvářet coiny z ničeho – což je pro jakoukoli kryptoměnu katastrofální selhání. Pomocí formální verifikace mohou výzkumníci matematicky dokázat, že určité vlastnosti platí pro každé možné provedení kódu, namísto spoléhání se pouze na manuální audity nebo testování.
2 700 teorémů pokrývá základní logiku Ironwoodových soukromých transakcí, kde jsou zůstatky a částky transakcí šifrovány. Důkazy ověřují, že systém vynucuje invarianty zásob – což znamená, že nelze vytvořit více Zcash, než protokol povoluje – a to i za nepřátelských podmínek. Výzkumníci tvrdí, že tento přístup zachycuje okrajové případy, které by tradiční kontrola kódu mohla přehlédnout.
Proč na strojově ověřených důkazech záleží
Formální verifikace je ve vývoji kryptoměn vzácná, protože je časově náročná a vyžaduje specializované odborné znalosti. Většina projektů se spoléhá na odměny za nalezení chyb a manuální audity, které mohou mít mezery. Zcash již dříve použil formální metody – pro svůj původní upgrade Sapling – ale úsilí v rámci Ironwood je dosud největší aplikací tohoto druhu pro síť.
Teorémy jsou napsány v jazyce zvaném Lean, což je asistent důkazu, který kontroluje každý krok úvahy. Pokud teorém projde, znamená to, že vlastnost je zaručena pro všechny vstupy. Výzkumníci zveřejnili celou sadu důkazů spolu se specifikací Ironwood, což umožňuje nezávislé ověření komunitou.
„Jde o to poskytnout co nejsilnější záruku, že matematika za Ironwood je správná,“ uvedl tým v prohlášení. „Chceme, aby uživatelé věděli, že zásoba je prokazatelně pevně daná, ne jen předpokládaná.“
Ironwood je stále ve vývoji. Práce na formální verifikaci je klíčovým milníkem, ale upgrade musí ještě projít procesem správy Zcash a být přijat těžaři a provozovateli uzlů. Výzkumníci plánují dále rozšiřovat sadu teorémů, jak budou přidávány nové funkce.
Zveřejnění teorémů nemění nic pro současné uživatele Zcash. Síť nadále běží na stávajícím protokolu. Tato práce však vytváří precedens pro to, jak by mohly být budoucí upgrady validovány – s matematickou jistotou, nikoli pouze s důvěrou.
Dalším krokem je období komunitního přezkumu, po kterém bude kód Ironwood navržen k aktivaci. Zatím nebyl stanoven žádný termín.
