Ethereum Heist

[Ron Pressler]

Ethereum is a blockchain cryptocurrency of the kind that normally attracts people with a certain political ideology. Ethereum's novelty is the inclusion of a virtual machine that allows running programs on the blockchain (I'm not familiar enough with the concept to understand precisely what that means), that are intended to encode machine contracts. The (first? and) most famous of those contracts is an organization called The DAO, which is a virtual VC of sorts, where people have invested their money and can vote on investments.

It turns out that the DAO contract contains a bug, or an "unintended feature", which has allowed someone to steal $50M worth of funds from the DAO in the last 24 hours.

The Ethereum team (which, I believe, is also the team behind the DAO), has issued a call (reproduced below) to formal method experts to help prevent such events from happening again; they are offering grants:

> Developers, cryptographers and computer scientists should note that any high-level tools (including IDEs, formal verification, debuggers, symbolic execution) that make it easy to write safe smart contracts on Ethereum are prime candidates for DevGrants, Blockchain Labs grants and String’s autonomous finance grants.

The Ethereum VM specification is found here, and I believe that a TLA+ model, which would allow modeling and verifying Ethereum contracts, is a very reasonable effort, which may also be a great marketing opportunity for TLA+ in light of the media attention given to the heist. 

Ron

[Alan Moore]

When I heard of the hack the first thing I thought of was TLA+. Shouldn't they be using a declarative language, not an imperative one, to specify contracts?

I'm new to it and I've never written a spec in TLA+ so this is probably an ignorant question: Couldn't something like TLA+ be used instead of their javascript-inspired language? I know it couldn't actually implement the contract terms but at least the before/after of the terms of the contract can be unambiguously specified... or not? Clue for the newbie?

Alan

[Ron Pressler]

TLA+ can specify unambiguously the full contract terms, their pre- and post-conditions, the bytecode VM and anything else you may want to know about Ethereum code. What it cannot do is implement any of it, because it's not a programming language... To a total newbie, I'd say think about TLA+ as a software simulation system, where you can simulate both your code and anything about the environment at any level of detail as you care to know. But instead of only running specific simulations, you can ask questions like "is this property always preserved?", "can this ever happen?" 

But you can't compile the simulation nor have the simulation interact with the outside world. It is a design and investigation tool that helps you build and understand software. This is why it can be especially suitable for Ethereum -- not as a replacement to anything, but precisely because everything is already built. TLA+ helps you write and understand programs regardless of the implementation language you choose.

Ron

[Alan Moore]

Thanks for the clarification.

That is pretty much what I figured. My thinking was that the contract language could be something like TLA+ and then when the contract is executed (by some external implementation language) the terms specified by the TLA+ spec could be used to "validate" the contract's execution by said external implementation. Or maybe a contract could include a TLA+ spec in *addition* to the contract's Ethereum code to be used as a sanity check on the code and the before/after state. This probably doesn't make any sense and is applying TLA+ where it doesn't belong... just an incomplete train of thought... nevermind :-\

Alan

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/uCcycpSzbZ4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--

-- 
"Whatever you can do, or dream you can do, begin it. Boldness has genius, power, and magic in it. Begin it now." - Goethe

[Ron Pressler]

There is nothing magical about TLA+ as a language. Leslie Lamport is a well-known opponent of the trend of "thinking in languages" ("Thinking is not the ability to manipulate language; it’s the ability to manipulate concepts. Computer science should be about concepts, not languages."). TLA+ just has clear, well-understood and relatively standard mathematical semantics, and is a tool for rigorously reasoning about what programs do. Putting something like TLA+ into the Ethereum language for execution at runtime wouldn't currently make much sense for complexity reasons. Writing Ethereum specs in a language with built-in verification tools is a whole other matter, but as what is executed is bytecode anyway, you have no assurance that the code you're executing is the code you verified.

But yes, use TLA+ in addition to Ethereum code. A TLA+ spec is a verifiable blueprint; the code itself is the building. It is much more than a sanity-check, though. It is a verification of your design. 

In addition to verifying contract design in general, TLA+ can model the Ethereum VM itself, and could be used to verify compiled Ethereum contracts. The Ethereum VM seems to be pretty thoroughly specified and is not too big, so a formal TLA+ spec seems like a very feasible and worthwhile goal. But that's a somewhat different use of the tool, although some combination of the two may be interesting as well.

The real challenge is figuring out what safety properties you'd want to verify for a contract. That is a job for the Ethereum domain experts, economists, lawyers etc..

Ron

[Christopher Meiklejohn]

What's unclear to me is that if TLA+ is the right tool?

It appears that what smart contracts need is not TLA, but an operational semantics for the language that smart contract provide?  Is TLA+ sufficient but not necessary?  That's my concern.  It seems that an operational semantics based on the language that the smart contracts provide would be necessary to ensure safety without restoring to something that TLA, that while may ensure correctness, might not be the proper fit for what needs to be proved.

- Christopher

[Ron Pressler]

Every language has operational semantics; they just may not be well specified, but from what I can tell, the Ethereum VM bytecode has a pretty good spec. However, well-defined semantics are just necessary for formalization. They cannot ensure correctness just as the clear operational semantics of Turing machines don't help ensuring the correctness of every Turing machine program. You still need a tool that will help you reason about a program, given its language's semantics. 

Ron