Before this theft event that shook Ethereum community not many people cared about security issues related to any part of Ethereum ecosystem. Hypes dictate own rules which is natural.
Since almost the beginning of my posting on DAOhub I constantly tried to raise security awareness among the community members in many areas: legal, code related, governance. I was ignored or assured that everything is under control. Not crying here, it’s just a confirmation of fact. I’m too old to be surprised by people’s lack of responsibility.
As I tend to trust no one I just waited when security deficiencies will be exploited. My expectations were largely exceeded — the fuck up level was far higher that I ever predicted. I expected some small scams, not a theft of this scale.
What was scariest in this theft was the fact that it exploited theDAO contract vulnerability together with faulty reward mechanism. Contract purportedly audited by best guys in this trade (no traces of serious evidence supporting this claim can be found) and written in solid as rock Solidity.
My thesis here is that with no durable replacement in place of Solidity more or less costly disasters will plague this ecosystem. Coders are often lazy, often stupid, sometimes both. Best practices, curator guarded standards and alike half-measures aren’t enough.
I focus here on Solidity, regardless I’m conscious that there are other languages created for smart contracts as Serpent or Mutan. Actually only Solidity is now developed on a regular basis.
Language choice
I understand why Solidity was designed in a way it looks now. It was easy. Solidity inherits its syntax and character from Javascript (or ECMAscript to be strict). With vast resources available that enable sub-setting Javascript in a number of ways it was really good candidate for lightning fast development.
Another factor that was mentioned by authors themselves was the immense Javascript popularity among coders. This assures that a coder won’t flee seeing strange syntax. While this way opens the world of smart contracts to the large community of coders it comes with an adverse effect of attracting people who often code on a very basic level and have poor understanding of how coding works in a broader perspective.
I will be harsh, but if even an idiot can use a certain tool, mostly idiots will use it, as they are so numerous. Nature acts here against responsible development.
Permissiveness
What is wrong with Solidity can be summed up with the above — it’s way too permissive. Solidity sits atop of EVM giving an abstraction layer allowing making contracts in a human readable form. The choice of Turing complete EVM is a matter of debate, but most of problems with it could be mitigated by using a language that enforces tight constraints.
In terms of constraints, Solidity cannot offer much. Mostly because it’s a language that enables (or even encourages) procedural coding style. What is wrong with it?
Among scores of arguments supporting functional languages in process-critical applications, discouraging procedural style at the same time, I can pinpoint one that speaks to me most. Purely functional languages can be analyzed with absolute certainty (except few degenerated cases easy to mitigate), while any complex structure done in a procedural one can be analyzed only with limited certainty depending on how much side effects are under control.
In reality, the more depends on humans the worse. Humans are supposed to take care about side effects. They failed exactly here in the case of theDAO theft. The fact that they failed not only with regard to contract isn’t an excuse. Solidity failed to be transparent enough to show possible threats, exactly where a language should be the first line of defense.
Recently I saw some articles proposing ways to mitigate problems with Solidity. For instance, Gavin Wood has written an article titled “Condition-Orientated Programming”. It addresses one of techniques that can actually be used to collapse side effects of procedures into easily traceable streams of exchanged data. However, what Gavin proposed is to use modifiers without any language enforced rules that would allow only this style of coding. While modifiers raise always many caveats in terms a language flow and ambiguity they can potentially serve as a good solution here, but only if the language itself enforces their use.
Otherwise curators or auditors will be given jobs, which is of course a nice gift to them, but solves no problem.
There are also many news about tools enabling formal analysis of both bytecode and Solidity contracts. In this second case since a year solc uses why3 to process a proof. As proved by the recent theft it mitigated nothing. What is interesting it first translates Solidity code into OCaml subset WhyML. Which isn’t surprising as Solidity itself cannot be deductively analyzed. Must be translated into a provable language. Of course something can be lost in the process. It’s a prosthetic solution, expression of the “patching culture” so common in Ethereum ecosystem.
Solutions proposed to date give no real outcome simply because it’s like reviving a corpse. Depending on them will yield problems sooner or later. Just sayin’.
What then can serve as a real solution?
Deduction is better than luck
Solidity is neither the first language addressing contracts nor the best one. It’s the first that deals with Ethereum ecosystem smart contracts. In the outside world both theoretical and applied solutions with regard to contract matters exist since many years. Companies like Citrix for instance deal with it successfully since almost thirty years. They just don’t call it smart contracts. Contract programming isn’t a fresh invention, Eiffel is over thirty years old by now. In fact most risks could be mitigated in Solidity if some concepts from Eiffel were borrowed, for example once routines.
The term “contract” wasn’t taken out from thin air too. It comes from analogy to legally regulated contracts. This area of law is over 2000 years old and even if the law can be fuzzy and mathematically hard to process some basic deduction principles exist there since millenia.
Legal analogy
If one looks into a properly made contract several easily discernible parts can be spotted. First definitions should be there. They should cover all axioms used later, descriptions of material entities, relations and a purpose of the contract. Next, what Romans called “essentialia negotii” (essential terms) should be easily identifiable depending on the purpose of the contract already defined. A sale contract must include price, otherwise it’s not the sale anymore, but a transfer of property being subject to different rules. Finally there must be an outcome of the contract and indication when it resolves.
Not all contracts are structured as above simply because either the law in a certain jurisdiction already defines some axioms and rules or lawyers/contract parties are dumb.
The purpose of this structure is to enable deduction of the outcome of contract from what is written. Of course, as natural languages are far from being strict, laws are fuzzy and people are the weakest part in this process courts are needed to resolve misunderstandings.
Define!
What is apparent from the above is that there is a safely deductible structure that gives strict results provided that all inputs can be strictly defined. While it’s impossible in real world contracts because human relations are just too complex to be strictly defined, such approach is achievable in blockchain contracts.
What is needed are axioms and definitions, processes, outcome and conclusion (termination). This structure, while totally absent in Solidity, can be achieved with help of other languages.
One attempt that drawn my attention was published by Yoichi Hirai here: https://github.com/pirapira/evmverif/blob/master/sketch.v. It uses Coq, a theorem prover, thirty years old by the way, so pretty stable. While I don’t think it could be used as a replacement of Solidity, it’s an interesting step toward building a provable and reliable language for smart contracts. It applies the above mentioned scheme with added value of processing a proof.
What is really needed is a language replacing (or being developed aside of) Solidity that encompasses this provable approach. Purely functional? Rather yes, I’d suggest. Maybe with built in support for mutexes or other objects to simulate side effects while retaining control. With requirements to define all involved entities. With no space for implied values. Explicit to the brim. With guarantees of termination and outcomes. With recurrence strictly supervised. All that Solidity cannot employ.
I saw somewhere an info that Vlad Zamfir builds a functional language for smart contracts. Cannot find any more detailed info though.
I always embrace news that inform about attempts to implement Ethereum solutions by big industry. But I’m also aware that whenever an audit will happen on these solutions one of passages in post-audit recommendations will be more or less:
“Due to unpredictable nature of the language used primarily in smart contracts development it is advisable to consider this solution as a proof of concept only until more reliable tools are created or adopted from other industry tested ones. Smart contracts that are a feature making Ethereum solution so attractive should be predictable if any production environment application is concerned. Otherwise risks in terms of business continuity seem to be too high.”
Moreover, given the fact that inside jobs are not uncommon in the big industry and auditors are aware of this, wording of above paragraph could be even more negative.
We need a new language with strong principles. Possibly won’t be so easy to code, but won’t be easy to abuse too.
