This article has been written by Synereo CEO Dor Konforty.
Designing expressive distributed protocols that can gracefully withstand attacks and manipulation is not a trivial task. Even solving a relatively simple use case, Bitcoin’s success in providing currency free of central control was certainly cause for celebration. When dealing with more complex problems, like financial contracts and governance, we have to step up our game.
Whether one believes the attack on the DAO was a problem in the contract or a flaw in Ethereum’s smart contracting language Solidity itself, it certainly highlights the need for better tools to help with the analysis of contracts deployed in mission-critical situations. To have such tools, a candidate for a smart contracting language needs to have a much greater level of precision in its specification. In fact, it needs a mathematically precise specification, usually called a formal semantics, to provide tools to analyze contracts that are to serve as dependable, production-quality services.
Without a formal semantics, it is impossible to reason about the code and specify what it does or to utilize any formal verification method to assure that it complies with any specification. For all intents and purposes, the only specification of Solidity’s semantics is its compiler to byte code for the Ethereum virtual machine (EVM). This compiler has not been formally verified. Likewise, the virtual machine running the code has not been verified, and so it is next to impossible to say anything meaningful about what contracts in Solidity are supposed to do.
Ethereum’s less rigorous approach has been cause for concern from day one, casually dismissed because most of us were ecstatic even just with the idea of a contracting system completely independent of any central entity or friction caused by middle-men. As has been predicted, we’re now at a point where a naive implementation free of a formal semantics can’t supply the sort of precision needed for proper analysis of mission-critical contracts. Further, as more and more smart contracts get written and deployed, it becomes more and more important to be able to analyze them, and even to analyze how they work together.
Synereo has been driving a mathematically rigorous approach to smart contracts since its inception so that it can provide the proper tool set for this kind of analysis. In a paper published by Jack Pettersson, Synereo’s language expert, and Greg Meredith, CTO, our approach is described through an example showing that Synereo’s Rholang smart contracting language would not allow the re-entrancy bug. This means that the security breach which allowed the attacker to drain The DAO of funds wouldn’t ever materialize in an equivalent Synereo implementation – all through automated checks during compilation.
Rholang is a language developed by Synereo specifically to support fine-grained concurrency inside smart contracts, with semantics derived from a mobile process calculus called the rho-calculus. As such, the Rholang compiler can use model checkers and theorem provers, useful particularly for checking and verifying contracts making use of concurrent and distributed processing of events. As Jack and Greg show, a modest type declaration, roughly similar to the kinds of types one finds in modern programming languages like Java and Scala, turns into a check in a model-checker — which when incorporated into the compiler pipeline as it is in Rholang — causes the compiler itself to prevent the malicious contract from ever existing in run-time.
Before looking at some of the details, it’s useful to compare contract development to other fields. Consider the electrician’s job. Running current through a household is absolutely mission-critical. Get it wrong and the house burns down. There was a time when electricians were more like artisans, handcrafting wiring solutions, many of which were completely unsafe. Now, there are standardized components and best practices that not only allow electricians to assemble a wiring solution for a household out of well-understood components but also allow teams of electricians to cooperate to wire much larger buildings with power.
The approach Rholang adopts is a lot like that. Contracts and even smaller units of logic inside contracts use types to say whether it’s safe to plug things together. Programmers familiar with languages like Java, C# or other popular languages are very familiar with this approach to assembling programs out of components that come with descriptions for how to use them safely. The only new thing here is that Rholang’s types capture more information about what constitutes safe use.
How does it work?
In Rholang, developers may specify which contracts the applications they create can accept through defining the contracts’ behavioral types.
What are behavioral types? This is a new development in programming, where more information about the behavior and structure of the code is captured at a higher level than of the code itself. Types define certain rules and forms that the code must abide by; for example that an update to the contract’s state is carried out to completion before allowing the contract to be called on again.
The above, in essence, is the core of the flaw the attacker exploited in the DAO: the contract handling a request for withdrawal was called on again and again before it was allowed to finish updating its balance. In a concurrent setting, like Rholang, the update and the re-entrance to the contract are racing, and the compiler checks the type to see if such a race is considered safe. In Jack and Greg’s paper, the type for the contract explicitly declares that that race is not safe, and rightly so, the compiler rejects the contract code as not respecting the type. In the Solidity contract for the DAO, the problem is even worse because the code path for re-entering the contract is not just racing, it’s always favored over the completion of the update.
We wholeheartedly acknowledge that reasoning about concurrent and distributed computing is hard. The approach taken by Synereo looks to make developers’ lives easier, and in ways that don’t interrupt their flow. By integrating tools for compile-time formal verification and relying on behavioral types, we achieve three goals: 1, the developer gets two views of the program, one at the level of the code and another at the level of the type; 2, the compiler itself informs the developer that his intention, as manifested through the defined types, is not captured in the actual code; and 3, the verification is part of the development process. Developers are well accustomed to compilers type-checking their code.
This holistic view of formal verification as part of the development process from start to finish has other benefits. For example, it gives rise to a design-by-type discipline which, in the case of the DAO bug, would bring more attention to the essential issue. As we can see in the paper, the type abstracts away much of the details of the contract and focuses on where concurrency and non-determinism is allowed – and where it must be prevented. These, and other benefits of Synereo’s approach lend themselves well to creating completely decentralized applications and protocols which are both simple and robust.
In conclusion
It is only when the right tools are in place that we can expect the decentralized economy to materialize – and to start becoming relevant to people outside of the cryptocurrency movement.
Formal verification must become standard practice in mission-critical decentralized applications, in the finance realm and beyond. Alongside it, Synereo reputation mechanisms ensure humans are still involved in the mix, acting as sanity checks in edge cases that even the best-written code and most-refined contracts could not predict.
We believe our dialogue with Ethereum continues to be extremely fruitful and productive for the entire ecosystem. All of us can benefit from the different expertise each party can bring to the table. We believe Synereo has the leading platform for creating secure and scalable decentralized contracts and applications and are committed to bringing these tools to the developer community post-haste.
If you liked this article follow us on Twitter @themerklenews and make sure to subscribe to our newsletter to receive the latest bitcoin and altcoin price analysis and the latest cryptocurrency news.
