How to use Synereo’s smart contract language to prevent hacking

Designing decentralized protocols that gracefully resist attack and manipulation is not a trivial task. Even solving a relatively simple use case, Bitcoin deserves praise for its success in providing a currency that is free from central control. When dealing with more complex problems such as financial contracts and governance, we need to establish our rules.

Whether one believes that the DAO attack was due to problems with the contract or to flaws in Ethereum's smart contract language Solidity itself, it undoubtedly highlights the need for better tools to assist in the analysis of contracts deployed in mission-critical situations. In order to have such tools, candidates for smart contract languages ​​need to have a higher level of precision in their specifications. In fact, it requires a mathematically precise specification - usually called a formal semantics - to provide tools to analyze contracts as reliable, production-grade services.

Without formal semantics, it is impossible to reason about the code, to specify what it does, or to use any form of formal verification to ensure compliance with any specification. For all intents and purposes, the only specification of Solidity's semantics is the byte code it compiles to the Ethereum Virtual Machine (EVM). This compiler has not been formally verified. Moreover, the code that this virtual machine runs has not been verified, so we can say very little about what a Solidity contract should do.

Ethereum’s lack of rigor in its approach has been a cause for concern since day one, with casual dismissals as most of us are already ecstatic at the mere idea of ​​a contract system that is completely independent of any central entity or friction caused by middlemen. As expected, we are at a stage where a bare-bones implementation of formal semantics does not provide the kind of precision required to properly analyze mission-critical contracts. And, as more and more smart contracts are written and deployed, it becomes increasingly important to be able to analyze them, and even how they work together.

Synereo has been pushing for a mathematically rigorous approach to smart contracts since its inception, so it can provide the right tooling for this type of analysis. In a paper published by Synereo’s language expert Jack Pettersson and CTO Greg Meredith, our approach is described through an example showing that Synereo’s Rholang smart contract language does not allow reentrancy vulnerabilities.
This means that the security gaps that allowed hackers to loot DAO funds would never materialize in an equivalent Synereo implementation — everything is automated and checked during the writing process.

Rholang is a language specifically developed by Synereo to support fine-grained concurrency within smart contracts, with semantics derived from a move-processing calculus called the rho-calculus. As such, the Rholang compiler can use model checkers and theorem provers, which is particularly useful for validating and verifying contracts that exploit concurrent, distributed event processing. As Jack and Greg explain, a modest type declaration, almost similar to what one sees in modern programming languages ​​like Java and Scala, becomes a model checker that — like in Rholang, includes the compiler pipeline — results in the compiler itself preventing malicious contracts from existing at runtime.

Before looking at some of the details, it is helpful to contrast contract developments with other fields. Think about the job of an electrician. Getting electricity running in a home is an absolutely mission-critical job. One wrong connection could burn the house down. There was a time when electricians were more like craftsmen, tackling wiring by hand, many of which were very dangerous. Now, standardized parts and best practices not only allow electricians to distribute electricity to services using well-understood parts, but also allow electricians to work in teams to wire larger buildings.

Rholang takes a very similar approach. Contracts, and even smaller units of logic within contracts, use types to indicate whether it is safe to pull things together. This approach of assembling program instructions from parts accompanied by safe usage descriptions will be very familiar to programmers who know Java, C#, or other popular languages. The only new thing is that Rholang's types capture more information about what constitutes safe usage.

How does it work?

On Rholang, developers specify the contracts that are acceptable to the applications they create by defining the behavior types of the contracts.

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, rather than just the code itself. Type definitions are certain rules and constraints that the code must follow; for example, an update to the state of a contract must be executed before the contract is allowed to be requested again.

This is, in fact, the core flaw that the attacker exploited in the DAO: the contract that handles withdrawal requests was repeatedly requested before being allowed to complete its update. In a parallel environment, such as Rholang, contract updates and reentry will race, and the compiler checks types to see if the race is safe. In Jack and Greg’s article, the contract types clearly indicated that the race was unsafe, and as it should be, the compiler rejected code that did not follow the contract types. In the DAO’s Solidity contract, the problem is even worse, because the code path that reenters the contract does not simply race, it always allows the update to complete.

We sincerely acknowledge that reasoning about parallel and distributed computer operations is difficult. The approach taken by Synereo seems to make developers' lives easier, and in a way that does not interfere with their lives. By integrating tools for compile-time formal verification, and relying on behavioral types, we are able to achieve three goals: 1) Developers get two views of the program, one at the code level and the other at the type level; 2) The compiler itself informs the developer of its intentions, which are exposed through defined types and are not captured by the actual code; 3) Verification is part of the development process. Developers are very accustomed to the compiler type checking their code.

A holistic view of formal verification as part of the development process from beginning to end has other benefits. For example, it leads to a disciplined approach to designing with types, which, in the case of the DAO vulnerability, brings more focus to the underlying issues. As we have seen in the article, types abstract away many of the details of contracts and focus on where concurrency and non-determinism are allowed - and where they are not. These and other benefits of Synereo’s approach lend themselves to the simple and brute force creation of fully decentralized applications and protocols.

Summarize

Only when the right tools are used correctly can we expect the decentralized economy to materialize — and start becoming relevant to people outside the cryptocurrency movement.

Formal verification must become common practice in mission-critical decentralized applications, in the economy and beyond. Moreover, Synereo’s reputation mechanism ensures that people are still involved, providing sanity checks on edge cases that even the best-written, most polished contracts cannot predict.

We believe our dialogue with Ethereum remains extremely productive for the entire ecosystem. We can all benefit from the different expertise each of our peers brings to the table. We believe Synereo has the leading platform for creating secure, scalable, and decentralized contracts and applications, and are committed to bringing these tools to the developer community as quickly as possible.

(Note: The author of this article is Dor Konforty, CEO of Synereo)