Note on Mechanised Governance
Some thoughts regarding governance, simulations, semantics and complexity
Disclaimer: Before you roast me, this post is not meant to judge any person or organisation and what they did or did not do. In particular, I have nothing against ETH, ETC, the DAO team or the hacker. All of them did and are doing incredibly useful things.
There are ongoing online discussions regarding “blockchain governance”. I want to add a few cents to this, from the point of view of someone understanding a thing or two about foundations of mathematics and security engineering.
For some context regarding the governance discussion, check:
- The blogpost “Against Szabo’s law”
- A response “In Defense of Szabo’s Law”
- This recent twitter thread which made me write this
What is the point of Szabo’s law / ethos?
> Zamfir: “Do not implement changes to the blockchain protocol unless the changes are required for the purpose of technical maintenance.”
> Shapiro: Szabo’s ethos: a “social trust minimisation approach”
Code is Law
Before we dive into that, let’s talk about “code is law”. This notion refers to smart contracts and suggests that “the law” is not coming from what is written down in a natural language contract and the lawyers and court’s interpretation of it, but instead a “smart contract” blindly and mechanically executes its code and nobody can do anything about it. Because the code is public and because the execution is deterministic*, you know exactly what kind of contract you are interacting with. (*same input, same behaviour)
So the most important aspect of *code is law* is that -but hold on- it makes it unambiguous how the contract should be interpreted, unlike the natural language version of a contract.
At this stage, we need to understand the code that creates the ‘simulation’, namely the runtime, the smart contract host, (for example the Bitcoin or Ethereum daemons).
The runtime in principle does not distinguish between smart contracts, they are all on equal footing. So you could write a very simple, safe contract, or you could have a very complicated, buggy contract. The runtime does not care and just executes the code as is.
In order to understand unambiguously what a SC does, you need to understand exactly what the machine does AND what the smart contract tells the machine to do. The instructions in the smart contract are a form of “machine code” running on a virtualised process, called a virtual machine. (EVM, Ethereum virtual machine in ETH case).
Roughly, we call the machine code in smart contracts ‘syntax’ and the behaviour or meaning that we expect the “semantics”.
There are two ways to describe the semantics of this virtual machine precisely:
- operationally, or a step-by-step description. If you see instruction A and you are in state X, then go to state Y and change the memory at location…
The nice part of operational semantics is that it is very close to how the machine actually operates. For example, here you see this in action; it’s how a Turing machine works / is described:
The not so nice part is that it is very difficult to understand what it’s happening if you zoom out from the local view, to the effect of the entire calculation. For instance, in the video it is not exactly clear right away that all the erasing and writing ones and zeros is actually adding or counting, etc.
- the other way of describing semantics is denotational.
Here, instead of giving the step by step instructions, you show that your syntax is just another way of speaking about a specific mathematical structure. Without going into too much detail (could be a whole blog series), the point here is that you can use existing theories about this structure to reason about the “global” behaviour.
I am mentioning this to show you that even though it is exactly known for each input what the contract does, depending on the complexity of the virtual machine it may still be impossible for a human, or even a computer to reason about all possible things that can happen with the contract.
Mathematics may look complicated, but it is really mainly formed to be easy to reason about. You just look at the transition table of a Turing machine, and you see each step. Easy to understand what this does! But you cannot create a conjecture about all possible ways it can run, let alone proof that conjecture easily, except for some very special situations.
In fact, a famous theorem states that a universal Turning machine (a TM that can simulate any other Turing machine, having this property in a VM or programming language is called Turing completeness) is that there are programs for which there does not exist an algorithm that can decide if the program will terminate or not.
Very concretely, this means that you could construct a transaction for a blockchain and all the nodes in the network would never finish processing the transaction and there is no way to detect this before you start working.
This is one of the reasons Ethereum has Gas (which I am going to call fuel). If you are out of fuel, the computation stops. So trivially the EVM is not Turing complete.
But this still does not help with making reasoning about SC behaviour any easier. You can also read this as more generally: **if you have Turing completeness, it becomes impossible to exclude unwanted behaviour automatically in all cases.**
This is why I have always argued against Turing completeness in the EVM and why I argue for formal semantics. It is an easy way out to take a TM and restrict it with fuel. But I want to be able to reason in the large about the behaviour of smart contracts.
Back to Governance
There is another very (in)famous example of governance in action, “the DAO fork”, probably better called the “DAO bailout”.
Let’s quickly summarise what happened there.
A particular smart contract running on the Ethereum blockchain (the DAO contract) was implemented in a rather complicated way and it turned out that there was some ‘emergent behaviour’ that was not exactly clear from the code immediately. In fact, it was even pointed out to the smart contract developers that their code was very complicated and might have bugs, but they brushed it off with “we don’t see any bugs with it, so it’s probably fine”. But it was not and had a critical security flaw which was eventually exploited by someone.
This is where the friction starts.
If “code was law”, then the DAO contract (which anyone was free to “sign into”) said in a not-immediately-obvious way that anyone could take all the money if they followed a very specific protocol.
Anyone with some security training (either offensive or defensive) knows that large complicated codebases are a Bad Thing(tm).
Would you sign a huge contract written in legalspeak where all pages refer back and forth to conditions in other pages etc, and on top of that you barely understand the legalspeak in the first place (machine code/solidity), let alone the implications of the laws holding particular jurisdiction this ‘legal code’ applies to? (the EVM semantics) **You probably won’t, because you don’t want to get into deep trouble signing something you don’t understand.**
Furthermore, if you are the organisation that is handing out the contracts (DAO), and you decide to write the legalese yourself instead of hiring expensive/experienced lawyers (~ someone that formalizes your contract first using paper math and then on a computer, ie. us) and then it turns out your amateur contract has some very bad unintended side effects and the signing party uses those to their benefit, well, … who’s at fault here?
Now, clearly with a paper contract, you can say: “Hey wait, you are interpreting this text wrong, I didn’t mean that”. And this is what expensive lawyers and courts are for, to figure out who is wrong.
Even so, in the DAO case, are you really sure the SC behaviour used by the “attacker” was unintentional? Crazy suggestion, you say? Consider this:
- structural issues about the security process and code base were pointed out to the team before attack was engaged, the team brushed this off
- imagine you are the only person in a team trying to point out there is a security issue or the approach is wrong and they laugh you repeatedly; you could turn around and exploit it at some point, so you silence yourself and instead say: “yeah let’s keep hacking on this reentrant code, looks good to me”
- at that time not many people would have the background to understand reentrancy bugs in EVM, likely the attacker had some stash ETH (if he/she didn’t, you’d probably attack straight away)
- so maybe the DAO was the ETH biggest scam so far?
FWIW, I really don’t think this happened, but I just want to point out the possibility and how non-obvious the intended behaviour was.
You might also say that clearly everyone that was investing into the DAO wanted it not to get hacked, the terms & conditions of the investment contract clearly gave a different impression about the behaviour of the code.
But this is the point, you DO-NOT-WANT to have a piece of natural language text that says what the code _should_ do and if later it turns out there are discrepancies, you just resolve that in court instead (as a form of governance).
Firstly, this problem already exists in the non-decentralised software world.
It is very inefficient and expensive to go from imprecise specification to precise code. As the programmers have to turn the spec into code, usually they discover incomplete specifications, inconsistencies or plain impossibilities. So they need to give feedback to the spec author, which then updates specs, etc. very time consuming and waterfall vs agile is exactly about making this iteration loop as fast as possible.
So how was this DAO situation resolved?
Let’s call the runtime ‘the simulation’, because as far as a smart contract is concerned this is all it sees and all interactions come from this environment. Zooming out, we see it’s simulations (formalised “virtual” worlds) all the way down:
If we then look at the user-defined ones, we can distinguish different levels of ambiguity in those contracts.
The green box represents the simplest contracts that have very limited functionality and for which you can (and have) proof that there is no other behaviour *at all* possible than what is in the contract. I call this closed, because it assumes a “closed universe”, every possible thing that can happen in *The Simulation* is considered in the security proof, interaction with other contracts, but also all things in ‘The Real World’, etc.
You can also have (yellow) very simple contracts that are fully understood, but because they interact in a more complicated way with the rest of the simulation, we cannot include everything in the security proof, so it is maybe possible that some undescribed and unconsidered outside mechanism breaks the contract. But you are still following the rules of the simulation.
Then there is the Turing complete contract, where nobody bothers really to proof anything; and a fancy website, flimsy white-paper and pseudo rigorous arguing should be enough to convince some people to sign the contract. IMHO* all hope is lost.
What the Ethereum Foundation did was what I’d call *governance at the simulation level*. Some “hand of a (pretending) God” decided to change the rules of the simulation, to take a very specific smart contract and bail them out.
*This violated Szabo’s law directly**. What is now called Ethereum classic is the chain that kept running the unmodified simulation code, the ETH chain is the one that runs exceptional code that gives the funds back to the DAO contract, ie. the one where governance changes the rules of the universe.
Conclusion
A different reading of Szabo’s law could be something like this.
In general, less code = fewer opportunities for bugs or emergent behaviour.
But that is not all, as in algebraic methods, we seek to have well behaved, very restricted systems that have nice properties and are “reasonable” (= able to reason mathematically about it).
A small amount of code does not imply that, per se. For instance, in a few lines of code one can write a Turing complete virtual machine, the extreme case where we have a proof that there are unreasonable programs (halting problem).
Or in the other direction, **at Statebox we spend a nearly-insane amount of effort on avoiding Turing completeness, exactly for this reason**, but with a tiny addition (`AND NOT IS ZERO`) to a single if statement, we would gain the ability to simulate a Turing machine.
If you are a programmer and you don’t have an understanding of these subtle issues, you’d think, what’s the problem, a single line change and it does not make the semantics really any more complicated. Well, operationally speaking it doesn’t, but denotationally we are looking at a very different beast suddenly.
Some examples
Many great examples of hacks or exploits that use this fact are around. For instance, people playing Super Mario in Starcraft.
(screenshots from RECON-BRX2018 talk “Starcraft, emulating a buffer overflow for fun and profit”)
This is not supposed to be possible, Starcraft maps are Starcraft maps and the game should reject illegal maps. but the Super Mario map is legal, it just exploits the fact that it can simulate ANY kind of program. once the Turing machine is found, you can build tools on top to work in the *new simulation*:
This is more or less how such “privilege escalation” exploits usually work.
Furthermore, legal governance is something that *itself* is a contract, namely the ‘real world laws’.
So you want to move this up into the smart contract world, and not apply it to the simulation. Doing this at the simulation level is similar to backdoor-ing crypto.
If we cannot rely on the precise behaviour of the simulation and the smart contracts, then we cannot rely on our proofs anymore and we can NEVER build a fully secure system.
If *instead* we say code is the law, there is no bailout/undo unless you build it in, then we have something to rely on. This also immediately implies that you only want to have _the utmost max A-grade level security_ for smart contracts, similar to when you launch a satellite. Because you cannot easily go up into space and press the reset button, the effort is put upfront because the software MUST NEVER fail, precisely because there is no undo button or big brother that you can go to to bail you out of your own mistake.
