When it comes to DLT contract languages you must choose, but choose wisely

In our previous article Distributed ledgers need more than traditional application design patterns, Shaul pointed out that most DLT vendors deliberately choose to “pair their ledgers with programming languages that are general-purpose and familiar in an effort to appeal to the most widespread developer skills.” This approach is understandable, and reduces the learning curve, but features of those languages can cause unpleasant issues when used for writing DLT smart contracts. Tony Hoare refers to null pointers as his billion dollar mistake — in this post we’ll discuss some of the language features that have already led to multi-million dollar mistakes when used in a DLT setting, and suggest some properties that a contract language should exhibit to help avoid similar mistakes in the future.

It is of utmost importance that contracts are implemented correctly. The massive advantage of DLT is a precise, unforgeable, permanent history of what has happened. But while the computer may have a precise knowledge of what happened, unless humans can be convinced to agree that the ledger matches what people intended to happen, the applications are severely limited. The pairing of the radically new DLT pattern for executing workflows with languages designed for more traditional development patterns has, on public blockchains, led to multiple examples of lost and stolen funds due to bugs in smart contracts. It’s not too hard to understand why.

“General purpose modeling languages let you program any eventuality, but also let you experience any eventuality.” 

Blythe Masters, Digital Asset CEO

Consider the public Ethereum network, where two of the most widely-known attacks exploited shortcomings in Solidity, Ethereum’s primary smart contract language.

In 2016 an attack, now famously known as the DAO exploit, drained over $150M worth of Ethereum’s native currency, ether, from the DAO via execution of a contract written in Solidity. Analysis of the incident showed that a flaw in the contract enabled the attacker to trigger recursive calls to a function that withdrew ether from the DAO contract without ever having the debits register to the attacker’s account.

More recently, $30M of ether was stolen from several users of the Parity Multisig Wallet — again, written in Solidity. Analysis of the Parity hack revealed that an error in the contract code allowed the attacker to take exclusive control of, and then drain, the targeted wallets. Remarkably, several months later, $154M in ether on Parity wallets was locked — rendered unreachable — by accident. Again, due to poor programming practices when coding the Parity contract.

As of today, writing a robust contract in Solidity requires the programmer to be aware of reentrancy attacks, over- and underflows, short address attacks and many more besides. Every statement must be considered both from the point of view of successful execution, as well as where and how exceptions may be thrown, and what partial states the contract goes through. Every time the programmer writes “+” they need to be thinking of the Solidity plus operator, not the mathematical “+” they are used to reasoning about. While Solidity might be similar to JavaScript in terms of syntax, safe programming of Solidity is an entirely different skill!

“finance applications should not have to worry about overflow errors. Ethereum should provide base types that make sure these kinds of reimplementations are never necessary in application code.” 

Emin Gün Sirer, Professor at Cornell

Lack of confidence in contracts is unacceptable in financial markets, where the credits and debits surrounding the transfer of value must happen consistently, atomically, and with finality. There is, of course, always risk involved when adopting new technology; however, the use of DLT cannot be extended to financial markets if the contract language itself introduces significant new sources of risk.

There’s a common belief that the sort of language issues that caused the aforementioned attacks will be fixed with time. But many languages have features built into them by design — because they are useful for traditional application patterns — that make them a risky choice for financial contracts. Without changes to make them more suitable for DLT — which would make them less suitable for their original purpose — the burden of correctness is placed squarely on the shoulders of the developer, with the best support available being in the form of best practices and standards.

You can’t arbitrarily pick a language for writing contracts without taking the time to understand the potential ramifications of the choice.

As Shaul pointed out, the emergence of DLT today has parallels to the emergence of the Web in the 1990s. The radically new Web platform did not fully deliver on its capabilities until new architectural programming styles, like REST, were developed to match the properties of the Web. Trying to adopt known styles to an innovative platform hindered progress of the Web back then; there’s little reason to think that the evolution of DLT will play out much differently now.

There is a better way — and that is to use a language designed explicitly for the purpose of codifying financial contracts, with built-in safeguards designed to prevent the kinds of attacks described in this post. And so, as with all new technology, we have to take a step back and look at the business problem that needs to be solved — which is to deliver sound smart contracts that, when executed, are capable of automating the workflow of value transfer without introducing excessive additional risk into the financial process.

At Digital Asset, our engineering team has spent years studying contract execution, and defined a number of critical contract properties that a smart contract language must enable for it to be acceptable for automating financial workflows. We’re just going to briefly summarize them for now; over the next few months, other members of our engineering team will examine each of these properties in detail and explain how our contract modeling language, Daml, was built to meet these properties and more.

For the consequences of a contract to be compulsory, entrance must be voluntary. It is only when all parties enter into a valid contract voluntarily that they become obligated to perform to the terms of the agreement and can be compelled to do so by judgement in a court of law.

For a contract to be confidential, only the parties affected by the contract can have the right to view contract details by default. Maintaining contract privacy is a function of both the DLT architecture and the language, the role of the language being to determine which data can be shared, and with which parties.

For the processing of a contract to be automated, one must be able to reliably reason about all possible future outcomes of any given state of the contract. Contract workflows can only be automated if the parties to the contract are in a position to pre-authorize workflow steps with certainty that the results will meet their expectations.

For a contract to be enforceable, incontrovertible evidence of its authorization by all stakeholders must be preserved. Even using a DLT platform, dispute resolution paths through existing legal systems will remain necessary. This requires a tamper-proof trail of evidence showing that agreements were entered into voluntarily by all of the contract’s stakeholders.

For a contract to be guaranteed to perform as intended, it must be amenable to formal verification methods. When automating financial markets with smart contracts, the standards for quality assurance are very high. Formal methods are the most effective way to guarantee that contract code meets its intent, and the language plays a key role in facilitating contract verification.

At first glance, enabling these properties may seem intuitive — trivial, even — but this is in fact not the case. Stick with this series as our team unpacks each one in turn and show exactly why all smart contract languages are not created equal!

Read Part 3: A new language for a new paradigm: smart contracts

New to this series about Daml? Click here to read from the beginning!

Join the community and download the Daml SDK.

This story was originally published 7 May 2018 on Medium

About the authors

Simon Meier, Ph.D, Distinguished Engineer and Director of Engineering — Product Foundations, Digital Asset @meiersi

Simon Meier leads the team that developed Daml. He holds a PhD from ETH Zurich, where he co-authored the state-of-the-art security protocol verifier Tamarin. His work on proving the correctness of security protocols led to the discovery of crucial flaws in the ISO/IEC 9798 standard and informed the standard’s subsequent revision. Simon is a core member of the Zurich Haskell community, and helps organise ZuriHac, the largest Haskell Hackathon.

Neil Mitchell, Ph.D, Senior Product Architect, Digital Asset @ndm_haskell

Neil has a PhD in Computer Science from York University, where he worked on making functional programs shorter, faster and safer. Since 2008 he’s worked at Credit Suisse, Standard Chartered and Barclays, applying functional programming to obtain the same benefits he focused on during his PhD. Neil is the author of popular Haskell tools such as Hoogle, HLint and Ghcid — all designed to help developers write good code quickly. More recently Neil has been researching build systems with publications at ICFP and the Haskell Symposium, and a practical system based on those ideas named Shake. Neil’s home page.