Waar de stellingen op gericht zijn
De stellingen richten zich op Ironwood, een geplande upgrade van de consensusregels van Zcash. Vervalsingsfouten zijn een type kwetsbaarheid waarmee een aanvaller uit het niets munten kan aanmaken — een catastrofale fout voor elke cryptocurrency. Door formele verificatie te gebruiken, kunnen de onderzoekers wiskundig bewijzen dat bepaalde eigenschappen gelden voor elke mogelijke uitvoering van de code, in plaats van alleen te vertrouwen op handmatige audits of tests.
De 2.700 stellingen bestrijken de kernlogica van Ironwood's afgeschermde transacties, waarbij saldi en transactiebedragen versleuteld zijn. De bewijzen controleren of het systeem aanbodsinvarianten handhaaft — wat betekent dat er geen Zcash kan worden gecreëerd buiten wat het protocol toestaat — zelfs onder vijandige omstandigheden. De onderzoekers zeggen dat de aanpak randgevallen kan opsporen die traditionele codebeoordeling over het hoofd zou zien.
Waarom machinaal gecontroleerde bewijzen ertoe doen
Formele verificatie is zeldzaam in de ontwikkeling van cryptocurrency omdat het tijdrovend is en gespecialiseerde expertise vereist. De meeste projecten vertrouwen op bugbounties en handmatige audits, die gaten kunnen laten vallen. Zcash heeft eerder formele methoden gebruikt — voor de oorspronkelijke Sapling-upgrade — maar de Ironwood-inspanning is tot nu toe de grootste toepassing voor het netwerk.
De stellingen zijn geschreven in een taal genaamd Lean, een bewijsassistent die elke redeneerstap controleert. Als een stelling wordt goedgekeurd, betekent dit dat de eigenschap gegarandeerd is voor alle invoerwaarden. De onderzoekers hebben de volledige set bewijzen samen met de Ironwood-specificatie gepubliceerd, zodat de gemeenschap onafhankelijke verificatie kan uitvoeren.
“Dit gaat over het geven van de sterkst mogelijke garantie dat de wiskunde achter Ironwood solide is,” aldus het team in een verklaring. “We willen dat gebruikers weten dat het aanbod aantoonbaar vastligt, niet alleen wordt aangenomen.”
Ironwood is nog in ontwikkeling. Het formele verificatiewerk is een belangrijke mijlpaal
