Home

A Next Generation Smart Contract and Decentralized Application Platform

A Next Generation Smart Contract and Decentralized Application Platform, Vitalik Buterin.

When Satoshi Nakamoto first set the Bitcoin blockchain into motion in January 2009, he was simultaneously introducing two radical and untested concepts. The first is the "bitcoin", a decentralized peer-to-peer online currency that maintains a value without any backing, intrinsic value or central issuer. So far, the "bitcoin" as a currency unit has taken up the bulk of the public attention, both in terms of the political aspects of a currency without a central bank and its extreme upward and downward volatility in price. However, there is also another, equally important, part to Satoshi's grand experiment: the concept of a proof of work-based blockchain to allow for public agreement on the order of transactions. Bitcoin as an application can be described as a first-to-file system: if one entity has 50 BTC, and simultaneously sends the same 50 BTC to A and to B, only the transaction that gets confirmed first will process. There is no intrinsic way of determining from two transactions which came earlier, and for decades this stymied the development of decentralized digital currency. Satoshi's blockchain was the first credible decentralized solution. And now, attention is rapidly starting to shift toward this second part of Bitcoin's technology, and how the blockchain concept can be used for more than just money.

Commonly cited applications include using on-blockchain digital assets to represent custom currencies and financial instruments ("colored coins"), the ownership of an underlying physical device ("smart property"), non-fungible assets such as domain names ("Namecoin") as well as more advanced applications such as decentralized exchange, financial derivatives, peer-to-peer gambling and on-blockchain identity and reputation systems. Another important area of inquiry is "smart contracts" - systems which automatically move digital assets according to arbitrary pre-specified rules. For example, one might have a treasury contract of the form "A can withdraw up to X currency units per day, B can withdraw up to Y per day, A and B together can withdraw anything, and A can shut off B's ability to withdraw". The logical extension of this is decentralized autonomous organizations (DAOs) - long-term smart contracts that contain the assets and encode the bylaws of an entire organization. What Ethereum intends to provide is a blockchain with a built-in fully fledged Turing-complete programming language that can be used to create "contracts" that can be used to encode arbitrary state transition functions, allowing users to create any of the systems described above, as well as many others that we have not yet imagined, simply by writing up the logic in a few lines of code.

Includes code samples.

By Manuel J. Simoni at 2014-07-23 17:12 | DSL | Paradigms | Parallel/Distributed | other blogs | 37143 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Concerning

The most worrying thing about this, to me, is that the language they use is not designed to be amenable to static analysis. Except by giving a script a limited supply of “gas” and running it to determine what it does, there’s no way to assert, say, “this script verifies this digital signature and succeeds iff the signature is valid” (to prevent invalid transactions), or “this script allocates a finite amount of memory” (to prevent denial-of-service attacks).

And politically speaking, implementing this outside of Bitcoin means skirting the existing distributed infrastructure and community for proprietary reasons, which I find suspect.

By Jon Purdy at Thu, 2014-07-24 01:27 | login or register to post comments

The most worrying thing

"The most worrying thing about this, to me, is that the language they use is not designed to be amenable to static analysis."

Agreed. Someone will figure out a way to do something hostile with those scripts. Since this language directly controls money, effort will be applied to that problem.

By John Nagle at Sun, 2014-08-03 20:49 | login or register to post comments

Implicitness and mutable state costing tens of millions of USD

Jon Purdy, John Nagle, and I'm sure many others, seem to be correct in their apprehensions of the Solidity smart contract language.

My initial feelings were that Solidity would probably be better served by a non-Turing-complete declarative language based on predicate logic, or at least a pure functional language.

The 31 million USD multi-sig wallet incident and the earlier 70 million USD DAO incident are both results of convenience features that overly rely on implicit behavior. (In one case, exploiting a catch-all method and inheritance and in the other case, exploiting accidental recursion via transparent replacement of fields with getter method calls (properties).)

I've just started browsing IC3, but am a bit disappointed at the lack of language research I've seen there, given that these two multi-million dollar incidents both boil down to language features that at least make hand analysis difficult. I'm glad to see some research on applying theorem provers, but I suspect that a cleaner contract language is also needed. If someone misunderstands the language semantics, they're more likely to start introducing axioms just to make the theorem prover happy, instead of trying to understand the flaws in their contracts.

Are any of you aware of any other research on smart contract languages, particularly the percentage of use cases that can be covered without needing Turing-completeness?

By kmag at Sun, 2017-07-23 10:00 | login or register to post comments

Typecoin

Are any of you aware of any other research on smart contract languages, particularly the percentage of use cases that can be covered without needing Turing-completeness?

The Typecoin paper (PLDI 2015) proposes affine LF as a foundation for smart contract languages. However, the authors didn't do a user study to see how widely applicable their idea is.

By adrieng at Sun, 2017-07-23 15:40 | login or register to post comments

Smart contracts have a long history

Smart contracts and related languages have a long discussion history on LtU, in approximate reverse chronological order:

* The SEC interested in formalizing contracts in Python (2010)
* Going functional on exotic trades (2009)
* Dana (2009) - a detailed post on contract languages, virtual economies in Second Life, and the PLT aspects.
* Stock exchanges: language design aspect (2008)
* Forex trading with functional programming (2008)
* Easylanguage: domain specific language for trading stocks (2007)
* Combinators for contracts (2006), which links to SPJ's Composing Contracts (2000), a great paper.
* And of course, nearly all of the above threads mention Nick Szabo's original smart contract language (2002), posted on LtU here but with no discussion, and his Secure Property Titles with Owner Authority (1998)

There's been some work in this area, but I haven't seen many lessons learned from this research, or even PLT research, adopted in the Solidity language. I don't know enough about the Ethereum VM itself to comment on that, but I believe they evolved together, so no doubt they share some of the same problems.

If we start from what we want, namely a human-readable and understandable contract language, where every party can read and understand the implications of a contract, and these can be cheaply verified by each party with total confidence, then it seems like Ethereum is taking entirely the wrong approach. They see smart contracts as just another type of programming, rather than what it probably should be: a domain-specific language for non-programmers declaratively specify contracts that are then compiled to code that verifiably enforces the contract. This DSL is exactly what Szabo describes in his 2002 paper.

Edit: just came across this very comprehensive list of financial DSLs, some of which are no doubt related, like Ivy (slides).

By naasking at Mon, 2017-07-24 16:06 | login or register to post comments

The minefield

You are quite right in how you characterise the two kinds of approach to smart contracts. The difficulty with the "domain-specific language for non-programmers declaratively specify contracts that are then compiled to code that verifiably enforces the contract" is that any DSL you come up with is almost certainly going to be incomplete, in that many potential applications of interest will be ruled out. Ethereum seems to have taken the choice of giving a very flexible but dangerous basis, leaving the problem of coming up with sane contract languages as something to be layered upon it.

I note that Yoichi Hirai has specified the Ethereum VM in Isabelle and Coq, which enriches the Ethereum ecology in an interesting way, one which might suggest that Solidity is not the future of Ethereum. He has been hired by Ethereum.

Christopher Allen says of the minefield approach to smart contracts that they should not be called smart contracts at all, but chain code.

By Charles Stewart at Tue, 2017-07-25 14:10 | login or register to post comments

The difficulty with the

The difficulty with the "domain-specific language for non-programmers declaratively specify contracts that are then compiled to code that verifiably enforces the contract" is that any DSL you come up with is almost certainly going to be incomplete, in that many potential applications of interest will be ruled out.

Agreed 100%. Such a DSL would seem to be a better starting point for your first attempt though. Fail-safe, as they say, and they set the tone of the platform with this first release.

As it stands, the first language, Solidity, is mostly just a quirky procedural language, with all the usual failures, but with some extra dynamism that makes static analysis even more hopeless. There are promising starts at more formal backends, like this EVM backend for Idris.

The efforts at formalizing EVM are great, but the EVM isn't the main source of the problems yet, the low-hanging fruit seems to all be in Solidity at the moment. And that's just a cursory list assembled at a glance.

Assuming some safer high-level smart contract language becomes dominant, then there are vulnerabilities due to failures of full abstraction, and then vulnerabilities in EVM itself, at which point the formalizations will be very useful.

Many of these problems might have been avoidable if they incrementally extended the EVM to Turing completeness as the inherent limitations became understood, instead of going Turing-complete right from the get go.

By naasking at Tue, 2017-07-25 16:31 | login or register to post comments

Process calculi for chain code

There are promising starts at more formal backends, like this EVM backend for Idris.

It's interesting that the authors of that thesis say they think FP is not an ideal fit for the job, and that process calculi might be a better fit.

By Charles Stewart at Wed, 2017-07-26 08:27 | login or register to post comments

Indeed, EVM features

Indeed, EVM features pervasive mutation and messaging, so I can see why process calculi would fit more naturally.

By naasking at Wed, 2017-07-26 12:09 | login or register to post comments

The E language for smart contracts

I neglected to mention the smart contracts work done in the E programming language, though that work was mentioned in some of the threads I linked to.

Something like the E language provides a pretty sound basis for smart contracts (see the Donut-Lab work at the above link). So there's a Turing complete basis that has a better security story and a proper solution for resolving "plan interference", unlike Solidity or Vitalik's follow-up "safer" EVM language, Viper.

By naasking at Tue, 2017-07-25 16:58 | login or register to post comments

Further to this, the number

Further to this, the number of safety caveats listed on the official Ethereum wiki is simply depressing, given how many of these issues have been solved for decades.

I also haven't seen it discussed much elsewhere, but I mentioned on reddit the very fact that message-not-understood can be caught dynamically and forwarded blindly is itself a cesspit of future vulnerabilities. This ability makes security non-compositional.

For instance, an earlier version of the multi-sig wallet may not have exposed the authority to re-initialize, but a later one could add it, and all of a sudden every program performing delegation using the new version is vulnerable, even though that code didn't change one bit, and the wallet reference is perfectly encapsulated. You need whole program analysis to ensure contract safety.

The vulnerable programs actually passed multiple audits, so combined with the above, it's clear that ensuring the safety of contracts in written in Solidity is currently infeasible.

By naasking at Wed, 2017-07-26 02:25 | login or register to post comments

Smart contracts for the Stellar payment network

There is WIP developing a smart contract framework for the Stellar payment network. The system seems to be usable, but the design is not yet finalised and is not supposed to be used yet for long-term contracts.

Cf. Stellar Smart Contracts (deprecated guide), ZkVM announcement (2019) and Turrets Network (document repository).

If you found the idea of smart contract automation interesting but did not like the fact that most of the work is being done in the context of volatile cryptocoins, this might be worth a look.

By Charles Stewart at Wed, 2021-05-12 10:13 | login or register to post comments