Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Deconstructing the DAO Attack: A Brief Code Tour

vessenes.com

Post reply on HN
Print view View original

71–80 of 167 posts

Re: Deconstructing the DAO Attack: A Brief Code Tour

#71

Post by mbrock »

pron wrote: post #69
mbrock wrote: post #61

Earlier quoted context omitted.

I agree that functional vs imperative is a red herring in this case. The Ethereum model is "imperative" anyway, so a functional DSL would probably end up looking like some kind of monad. That said, it seems interesting to use a language like Agda for writing a DSL to EVM compiler, regardless of the exact nature of that DSL. Then you can have machine checked compiler correction proofs and also prove theorems about DSL…

That would be interesting and even necessary. But why not use something much easier than Agda, though not less powerful for this use case -- like TLA+ -- something that even "ordinary" engineers could use to verify their contracts (not to mention that it supports model-checking in addition to deductive proofs, which reduces the verification effort considerably)?

Maybe that would be better. I admit that I don't know the first thing about TLA+. Agda is what I learned about in school, and what my computer science friends are excited about, and I was already interested in using it to write verified compilers. Writing compilers with functional languages was also a part of my university education. But that's just my background.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#72

Post by beachstartup »

if you could 100% accurately and reliably model a contractual understanding in any kind of language, it would have been done eons ago. human language (i'm fond of english in particular), is extremely expressive.

but there's a reason we still have courts and judges. it's because language is the tool through which humans express their desires and fears (computer language included, because it is written by humans, so far), it's not a machine.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#73

Post by marvy »

powera wrote: post #68
whazor wrote: post #67

Earlier quoted context omitted.

To counter your attack on Buterin, he is aware that writing safe contract code requires proofs and type safety. That is why solidity is compiled to EVM code, so that improved languages could incorporate this. Solidity is built for rapid innovation and user friendliness. Buterin is now more busy with sharding and scaling issues.

People did lose $200 million dollars. Why is he focusing on scaling ? Edit: apparently the thefts so far are "only" 45 million.

So that they can lose $2 billion instead :)

Just kidding; bad joke; I just couldn't resist.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#74

Post by willtim »

pron wrote: post #50
willtim wrote: post #4

Modelling financial contracts in an imperative event-driven paradigm just seems like an accident waiting to happen. EDIT: To the downvoters, if you disagree, I would very much like to understand why, please reply with a comment. EDIT2: My position is that it is very difficult to reason about correctness and maintain invariants in a highly imperative setting. IMHO, it would be more desirable to use a declarative, or f…

I think you are placing far too much emphasis on language, especially as so far there's little evidence that some programming approaches yield less logical errors than others. I often see a similar sentiment expressed by people who are familiar with functional programming but unfamiliar with software verification, and may be unaware that nearly all verified software in the industry is written in imperative languages.…

Of course most of the money has been funding tools for imperative languages as that is the status quo. But this does not prove that there is little overlap with FP. Research FP languages like Coq have enabled INRIA to build a fully verified C compiler (Compcert), can your tools accomplish this? As far as Europe is concerned, FP does appear to be the future of formal verification.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#75

Post by jsprogrammer »

powera wrote: post #68
whazor wrote: post #67

Earlier quoted context omitted.

To counter your attack on Buterin, he is aware that writing safe contract code requires proofs and type safety. That is why solidity is compiled to EVM code, so that improved languages could incorporate this. Solidity is built for rapid innovation and user friendliness. Buterin is now more busy with sharding and scaling issues.

People did lose $200 million dollars. Why is he focusing on scaling ? Edit: apparently the thefts so far are "only" 45 million.

I thought only a fifth of ~$115 million has been sequestered (apparently the action will be rolled back)?

Re: Deconstructing the DAO Attack: A Brief Code Tour

#76

Post by devit »

willtim wrote: post #4

Modelling financial contracts in an imperative event-driven paradigm just seems like an accident waiting to happen. EDIT: To the downvoters, if you disagree, I would very much like to understand why, please reply with a comment. EDIT2: My position is that it is very difficult to reason about correctness and maintain invariants in a highly imperative setting. IMHO, it would be more desirable to use a declarative, or f…

The actual issue is the fact that sending money to someone can result in untrusted code running in the middle of your code execution and even reentering it seems absurd.

Sending should always succeed immediately and if anything needs to be automatically triggered in response, the trigger should be executed asynchronously.

A great way to immediately see the problem is, for anyone with Rust experience, to think of this as a function taking an &mut self being somehow reentered without that &mut self being passed out by the function itself.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#77

Post by jacquesm »

whazor wrote: post #67
tinco wrote: post #37

In addition to this the language is not explicit enough. Even standard Haskell wouldn't be safe enough for a program that manages $250MM directly without safe guards. In addition to typesafety, it would have to be both explicitly typed at the lowest possible granularity and annotated with pre and post conditions. Not only did this code allow a bunch of tokens be transferred without compensation, it left the whole acc…

To counter your attack on Buterin, he is aware that writing safe contract code requires proofs and type safety. That is why solidity is compiled to EVM code, so that improved languages could incorporate this. Solidity is built for rapid innovation and user friendliness. Buterin is now more busy with sharding and scaling issues.

> Buterin is now more busy with sharding and scaling issues.

Those are currently not the issues that require attention.

You can make it as fast and as large as you want, if it is broken at the root that's all pointless. First walk, then run. I'd be more impressed with a much smaller system without sharding and massive scaling properties if it was bullet proof.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#78

Post by tdaltonc »

TruthAndDare wrote: post #25
fabled_giraffe wrote: post #6

I know I'll get napalmed for saying this, but why is this all over HN? Why are people obsessed with cryptocurrencies? It's bad enough that those with sufficient computing speed/power can already rip off the stock market; why does the world need another way for people to rip each other off? Since we've determined over history that some people will take advantage of weakness for their own gain, no matter what system yo…

> It's bad enough that those with sufficient computing speed/power can already rip off the stock market Who is getting ripped off?

Any one who agree with the narrative outlined in Flash Boys (which I do), thinks that HFT is basically a drain on the economy. It doesn't help allocate capital more efficiently or provide any liquidity when it's actually needed. It uses speed and deliberately rigged market rules to take returns fro people that are trying to put capital to work (either as investors or as businesses).

Re: Deconstructing the DAO Attack: A Brief Code Tour

#79

Post by tootie »

jacquesm wrote: post #31
DrJokepu wrote: post #28

Earlier quoted context omitted.

> That remains to be seen. Isn't this a somewhat meaningless statement? Is it possible to prove that "no matter what system you create to transfer goods, resources, services or value representing those, it will be exploited"? Is it possible to prove the contrary (that there is or could be such a system)? It will never be seen because we will never know for sure one way or the other. Best we can do is to make educated…

Let's take banking as an analogy: is it perfect? No, it definitely isn't. But it is 'good enough' to power worldwide commerce. So until these systems reach reliability parity with 'ordinary' banking we'll see reduced trust. But once a system gets launched that has staying power and that appears to have made the right decisions in the founding phase you can expect more and more commerce to ride on them. When more comm…

I don't understand how this is even comparable to "banking". It seems like more a replacement for wire transfers. I don't see how it changes the face of investment or the flow of capital.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#80

Post by tdaltonc »

jcfrei wrote: post #12

So, this review makes me wonder: Will the hard fork of the ethereum blockchain be of any use at all? The DAO appears to be fundamentally flawed, are all the coins there simply lost? What prevents an attacker from exploiting the DAO after the hard fork? Or will they simply invalidate all the transactions that went to the address of the DAO?

As I understand it: The goal of the fork is to freeze the DAO account starting just before the 'split' drain (at the blockchain level). And then figure out a long term solution (possibly using another fork to return all ETH to the original contributing accounts dissolving the DAO?).

The ability of a core of developers and miner to exercise their will over the system like this is alarming though.

https://blog.ethereum.org/2016/06/17/critical-update-re-dao-...

Post reply on HN