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

61–70 of 167 posts

Re: Deconstructing the DAO Attack: A Brief Code Tour

#61

Post by mbrock »

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.…

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 programs.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#62

Post by jacquesm »

tmalsburg2 wrote: post #47
krapp wrote: post #45

Earlier quoted context omitted.

Wouldn't it be better to just rewrite everything in that safe language and abandon whatever Ethereum is written in?

Sure, but many people are so deeply invested in Etherum that I doubt that it's going to happen. But perhaps there will be a competing system.

The only person who is currently really deeply invested is the hacker. The rest, not so much.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#63

Post by chii »

rahimnathwani wrote: post #18
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 didn't downvote you, but your comment left me scratching my head. You made a statement without any explanation. Care to elaborate why imperative programming is so bad here? Real-world contracts also use imperative style.

real world contracts are interpreted by a court of law, which have leeways that aren't afforded by a machanical interpreter.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#64

Post by htns »

I don't get how the transfer vs Transfer typo is supposed to have enabled a larger attack. The token balance is zeroed in the splitDAO function anyway, and presumably the sanity checks in transfer are also redundant, or else there would have been no need for recursion.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#65

Post by willtim »

johnbender wrote: post #52
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 would go further. Given the sums of money involved I think it might also be worthwhile to have a formal semantics and a logic for proving safety properties of these blockchain programs (beyond type safety). Not every application would require that kind of rigour but if the participation and value of a given currency/contract/program is determined largely by trust then it seems natural to want more serious guarantee…

I agree. I covered this only briefly under 'formal methods'. My point was that such formal semantics and proofs are far more easily obtained starting from a functional language.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#66

Post by RobertoG »

I'm going to be a little polemic here.

It's this an attack?

It's not the problem that those technologies try to solve, to get rid of subjectivity?. In a way, this could be interpreted as trying to be free of politics.

If my understanding of what they are trying to accomplish here is correct, if the system allow it, then, by definition, it's legal.

If you require a framework where something allowed by the code but with unexpected consequences is illegal, you are again where you started.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#67

Post by whazor »

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.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#68

Post by powera »

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.

People did lose $200 million dollars. Why is he focusing on scaling?

Edit: apparently the thefts so far are "only" 45 million.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#69

Post by pron »

mbrock wrote: post #61
pron wrote: post #50

Earlier quoted context omitted.

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.…

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)?

Re: Deconstructing the DAO Attack: A Brief Code Tour

#70

Post by wildlogic »

jacquesm wrote: post #62
tmalsburg2 wrote: post #47

Earlier quoted context omitted.

Sure, but many people are so deeply invested in Etherum that I doubt that it's going to happen. But perhaps there will be a competing system.

The only person who is currently really deeply invested is the hacker. The rest, not so much.

Hah.
Post reply on HN