In Code We Trust, or Do We?

Everyone in DeFi has heard it: “Don’t trust the people, trust the code”. Not surprisingly, this resonated with me as a programmer. However, this phenomenon seems to not only appeal to techies; it resonates with all sorts of people. To be honest, this has always kind of perplexed me. Would you live in a house built by some anonymous stranger just because you can see all the blueprints? I surely wouldn’t! I have no idea what it takes to build a house safely, so the blueprints are pretty meaningless to me. Nonetheless, this phrase is being tossed around on basically every occasion when the topic trends toward trust.

After having spent quite some time in DeFi, having read tons of code, and even writing some myself, it feels like the time has come to reflect on this interesting idea that we cannot rely on people but should instead trust the technical blueprint, also called code.

In theory, anyone can access and thus read the source code of the contracts they interact with. All verified smart contracts are publicly accessible, so there are no secrets or hidden backdoors. Sounds beautiful so far! However, as with everything in life, there are some caveats to it. Of all the people who are supposed to interact with DeFi — which could potentially be 99.9% of people on earth —, how many can read source code? How many can actually understand what the smart contracts are doing, let alone think of all the attack vectors these contracts could potentially be exposed to? After having dealt with a lot of the Balancer codebase, I would argue that the chances of people capable of doing this, and more importantly, having the time to do this for any contract they interact with, is rather slim to non-existent. With this in mind, I think we have to accept that verifying the source code yourself is simply not an option for the majority of people. Even for those who would be capable of doing so, it would be too much of a time-sink in a fast-changing ecosystem like DeFi.

So, what can we do? Is this open-source thing any good or is it all just smoke and mirrors?

The good news is: it’s not that grim. The code is there, so we should be able to do something with it, right?

The main question to be answered is: How can we build a high confidence level with a minimum amount of human trust? Why do we even want to minimise human trust? Not necessarily because humans generally want to screw you over — the human species is not that evil by nature. A more viable explanation may be: making no mistakes is just so incredibly difficult!

So all this basically means, it would be sweet if there was a code to verify the code we use, right? Wait, but who verifies the code that verifies the code that we want to be verified? There might be another solution entirely, yet, as far as I can tell, at some point, we have to trust humans to break the cycle. With the goal to minimise the human trust factor, we should aim for this second verification layer to be applicable to any contract without adjustments. If this is true — and feasible —, the verification code would be static and could be very well audited.

Luckily, such a solution already exists in the form of ‘formal verification’. Formal verification is already used in the process of designing mission-critical software systems such as nuclear power plants and spacecraft. Never heard of it? Don’t worry, let’s have a look at a brief definition (ethereum.org docs):

Formal verification refers to the process of evaluating the correctness of a system with respect to a formal specification. In simpler terms, formal verification allows us to check if the behaviour of a system satisfies some requirements, i.e., it does what we want.

Formal verification techniques can then verify that the implementation of a contract complies with its specification and derive mathematical proof of the former’s correctness.

A mathematical proof of its correctness? That sounds promising! The idea is, as far as I understand, that we define and specify what a program should do. The program thereupon generates a mathematical proof for doing exactly that; nothing more and nothing less. Boom! So, if this exists, why do we still have bugs and exploits in DeFi?

Fair question, which I can also just speculate about. First, there is complexity and time required to set up all the rules the contract should adhere to. Second, and closely intertwined with setting up those rules, there appears another big source of errors: humans. We might have misconfigured something, might have forgotten to include some rules, or just didn’t have enough time to do it as carefully as we should have. Not a good argument, I know, but that’s just what happens. Also, complexity rises exponentially as protocols interact with each other. This is the case, for example, when Balancer deposits the idle assets from boosted pools into Yearn vaults, which in turn reinvest into yield-generating strategies. To make things worse, there are further factors that additionally challenge our goal of writing bug-free contracts. One of them is Solidity being a Turing complete language. This could be a topic for another article; but please have a look at this blog if you want to know more about it.

Now we know, there are tools available that can minimise the need for human trust by maximising confidence that a contract does — and only does — what it was supposed to do. Nonetheless, it’s still extremely challenging to produce bug-free contracts as it requires dedicated effort from protocols and auditing companies.

Despite all these hurdles, we should strive to maximise the overall confidence level of smart contracts at all times. Because ultimately, these contracts may be dealing with people’s life savings. And dealing with people’s life savings should be treated with just as much care as sending people into space. Telling people to “go read the code” is pretty silly in my opinion. The following advice seems more appropriate: Go check the formal verification method that has been applied, and make sure the rules have been verified by a credible source.