Re: Ethereum Heist

[Alan Moore <kahun...@xxxxxxxxxxxxxx>]

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

On Friday, June 17, 2016 at 11:37:33 PM UTC-7, Ron Pressler wrote:
> 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