Simplicity: een alternatief voor Script

Bitcointransacties maken gebruik van Script: een eenvoudige en zeer veilige programmeertaal. Script is met opzet beperkt in zijn functionaliteit om veiligheidsrisico's zo klein mogelijk te houden. Toch is er de wens om uitgebreidere 'slimme contracten' te kunnen maken. Simplicity is hier mogelijk een oplossing voor.

Bitcointransacties als kleine programma's

Een bitcointransactie is in essentie een lijst met instructies die beschrijven hoe de volgende persoon die de bitcoins wil uitgeven toegang tot de bitcoins kan krijgen. Je kunt een bitcointransactie zien als een klein programmaatje dat uitgevoerd moet worden, en bij succesvolle uitvoering toegang geeft tot de bitcoins. Bitcointransacties maken gebruik van Script: een eenvoudige en zeer veilige programmeertaal.

Script is met opzet beperkt in zijn functionaliteit om veiligheidsrisico's zo klein mogelijk te houden; de taal is niet Turing compleet en staat geen lussen toe. Door het simpele ontwerp van de taal weet je zeker dat elk programma (lees: elke bitcointransactie) dat in deze taal geschreven is eindig is. Dit wil zeggen: je kunt met zekerheid zeggen dat het programma niet op hol zal slaan of oneindig door blijft draaien. Daarnaast zijn de mogelijke veiligheidsrisico's door de beperkte functionaliteit goed te bestuderen. Het is immers makkelijker om wat te zeggen over de mogelijke uitkomsten van een programma wanneer de toegestane operaties beperkt zijn dan wanneer er een groot aantal mogelijke operaties is.

Een programmeertaal wordt Turing compleet genoemd als elke berekening of gegevensbewerking die geprogrammeerd kan worden uit te drukken is in de betreffende programmeertaal. Er wordt ook wel gezegd dat de taal een Turing machine moet kunnen simuleren.

Wanneer iemand een bitcointransactie aan wil maken is alleen de transactiedata zelf van invloed op de geldigheid van de transactie. Hierdoor is het voor de verzender gemakkelijk om vooraf de geldigheid van de transactie te berekenen. Zo kan de verzender garanderen dat er geen onnodig hoge hoeveelheid operaties nodig is voor het verwerken van de transactie. Het is mogelijk om, zonder het programma uit te voeren, met zekerheid te zeggen hoeveel operaties er nodig zijn om het programma tot een succesvol einde te laten komen. Het op deze manier bestuderen van een programma om uitspraken te doen over de kwaliteiten van het programma heet statische analyse en wordt in formele verificatie gebruikt om de correctheid van een programma aan te tonen.

Door zijn beperkte functionaliteit leent Script zich goed voor statische analyse. Dit is wenselijk: we willen vooraf met zekerheid uitspraken kunnen doen over de programma's die we gaan uitvoeren. Wanneer we dit niet kunnen wordt het lastig om aan te tonen dat een programma (of transactie) geldig zal zijn, zal doen wat de bedoeling is en zal doen wat we verwachten dat het doet. Hoewel Script dus beperkt is tot het maken van simpele bitcointransacties, is het wel een erg veilige programmeertaal voor het maken van transacties met (grote) waarde.

Een behoefte aan 'slimme contracten'

Toch is er de wens om uitgebreidere 'slimme contracten' te kunnen maken. De exacte definitie van een slim contract staat nog niet vast. Sommigen pleiten dat de multi-signature transacties die mogelijk zijn met Script te beschrijven zijn als slimme contracten. Anderen, zoals Tadge Dryja, definiëren slimme contracten als 'betalingen die afhankelijk zijn van bepaalde externe data'.

Deze laatste definitie is wat de meeste mensen zullen kennen van de slimme contracten die mogelijk zijn met Ethereum. Een simpel voorbeeld hiervan is bijvoorbeeld het afsluiten van een weddenschap over de uitkomst van een schaakwedstrijd, waarbij het contract na afloop van de wedstrijd zelf het resultaat opvraagt en uitbetaalt aan de winnende partij.

De aanpak van Ethereum laat op het gebied van formele verificatie echter te wensen over. De programmeertaal waarin slimme contracten op Ethereum geschreven worden, Solidity, is namelijk Turing compleet. Hoewel dit betekent dat er van alles mogelijk is met Ethereum, en dus vaak aangehaald wordt als voordeel ten opzichte van Bitcoin, zorgt dit ook voor een aantal inherente zwaktes. Doordat de programmeertaal waarin de slimme contracten op Ethereum geschreven worden Turing compleet is, kan door middel van statische analyse niet aangetoond worden dat het contract correct geïmplementeerd is of dat het contract eindig is.

Een gebruiker weet hierdoor niet precies wat het resultaat van de transactie zal zijn, en of dit het gewenste resultaat is. In essentie komt hierdoor het doen van een transactie neer op een verzoek aan de miners om een mogelijk oneindig programma te draaien. Om te voorkomen dat een contract oneindig door blijft draaien (in een oneindige lus geraakt) maakt Ethereum gebruik van gas.

De gebruiker betaalt voor het uitvoeren van het contract een bepaalde hoeveelheid gas, waarbij elke operatie die uitgevoerd moet worden een vaste prijs in gas kost. Als er meer operaties nodig zijn dan voor betaald is in gas, dan wordt de uitvoering van het contract beeïndigd.

Om te garanderen dat het contract wel volledig wordt uitgevoerd moet de gebruiker de maximaal benodigde hoeveelheid gas meesturen; er is geen praktische manier om voor het draaien van het contract aan te tonen wat de computationele kosten hiervan zullen zijn. Tevens weet een gebruiker niet altijd of de meegegeven hoeveelheid gas überhaupt voldoende is om het contract succesvol te laten draaien. Daarnaast is de uitkomst van transacties naar een contract niet alleen afhankelijk van de transactiedata, maar ook van de huidige staat van de blockchain. Dit maakt de precieze uitvoering van het contract moeilijk voorspelbaar.

Omdat statische analyse niet kan worden toegepast om te bewijzen dat een contract correct geïmplementeerd is kan het zijn dat een contract ongewenste resultaten heeft. Dit is in het verleden al meerdere malen voorgekomen. Verscheidene contracten zijn het slachtoffer geworden van hackers die op een slimme manier de zwakke contracten manipuleren om zo geld aan het contract te onttrekken. Recentelijk werden door een fout in het contract per ongeluk alle tegoeden in de multi-signature contracten van Parity permanent bevroren, wat heeft geleid tot verlies van honderden miljoenen euro's. Hoewel Ethereum heeft laten zien van wat voor mooie toepassingen men durft te dromen, is ook gebleken dat de gekozen aanpak erg kwetsbaar is.

Simplicity

Simplicity is mogelijk een oplossing om slimme contracten, die bewijsbaar correct zijn geïmplementeerd, op Bitcoin mogelijk te maken. Simplicity werd onlangs aangekondigd door Russell O'Connor, ontwikkelaar bij Blockstream. Simplicity kan, in de toekomst na grondige controle, eventueel toegevoegd worden aan Bitcoin via een soft-fork. Met Simplicity will O'Connor het mogelijk maken om de Script-taal van Bitcoin uit te breiden om bredere functionaliteit mogelijk te maken, maar met behoud van een aantal van de waardevolle eigenschappen van Script.

Allereerst is Simplicity niet Turing compleet, waardoor het zich, net als Script, goed leent voor statische analyse. Programma's geschreven in Simplicity kunnen vooraf aan uitvoering worden bestudeerd om te bepalen wat de maximaal benodigde computationele middelen zijn, waardoor nodes die de programma's uitvoeren niet overmatig belast worden. In Simplicity is het niet mogelijk om programma's onbegrensd te laten lussen en kan er geen recursie toegepast worden. Wél is het mogelijk om elke eindige operatie te definiëren, waardoor de programmeertaal voldoende expressief is om nuttige slimme contracten te schrijven. Ook blijft het mogelijk om aantoonbaar eindige lussen uit te voeren, waarbij vooraf aangetoond kan worden wat de benodigde computationele middelen zijn voor uitvoering.

Ten tweede behoudt Simplicity de eigenschap van Script waarbij transacties, of slimme contracten, geen toegang hebben tot externe data. Hiermee zorgt Simplicity ervoor dat de uitvoering van contracten niet afhankelijk is van data anders dan die van de transactie zelf. Wanneer een programma aan de kant van de verzender is gevalideerd kan de (bewijsbare!) uitkomst hiervan makkelijk geverifieerd worden door andere deelnemers in het netwerk. Het contract hoeft, na opname in de blockchain, dan ook niet meer opnieuw uitgevoerd te worden.

Tot slot, dankzij de insteek van Simplicity gericht op formele verificatie, is het voor ontwikkelaars mogelijk om te redeneren over de correctheid van de programma's die zij schrijven. Dit kan met zogenaamde proof-assistant software, zoals Coq. Ontwikkelaars kunnen de programma's schrijven in Coq, welke statische analyse toepast om de correctheid van het programma te verifiëren zonder het programma daadwerkelijk te draaien. Hiermee kunnen logische fouten, zoals het geval bij de vele hacks die Ethereum-contracten hebben geleden en de recente Parity multi-signature fout, voorkomen worden.

Simplicity is een aanpak voor slimme contracten die geheel in lijn is met de filosofie die ontwikkelaars achter Bitcoin aanhouden: veiligheid en degelijkheid voorop. In het wilde westen van de cryptocurrency-wereld worden hacks zoals die bij Ethereum plaatsvinden snel vergeten, maar deze zouden idealiter geheel voorkomen worden. Met Simplicity wordt in ieder geval alles gedaan om ontwikkelaars in staat te stellen om slimme contracten te schrijven die veilig zijn. Daarnaast is Simplicity een uitbreiding voor Bitcoin, wat het Bitcoin-ecosysteem en het gebruik van Bitcoin ten goede komt.

De geïnteresseerde lezer kan in het paper over Simplicity de technische diepte induiken.