Deconstructing the DAO Attack: A Brief Code Tour • Hacker News Board

Re: Deconstructing the DAO Attack: A Brief Code Tour

#121

Post by mietek » Sat, Jun 18, 2016, 10:12 PM UTC

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…

Note that a type system, if done properly, is simply another name for a logic for proving properties of programs.

Examples:

* Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php)

* Coq (https://coq.inria.fr)

* Idris (http://www.idris-lang.org)

Re: Deconstructing the DAO Attack: A Brief Code Tour

#122

Post by lomnakkus » Sat, Jun 18, 2016, 10:16 PM UTC

jacquesm wrote: post #112

whazor wrote: post #108

Earlier quoted context omitted.

Ethereum is a turing machine that runs code, programming languages are more high level. Creating an ADA-like language is trivial compared to making a scalable blockchain that supports computation. Ethereum itself is more bullet proof, as there are multiple implementations and the description of the protocol better defined and has proofs inside.

> Ethereum is a turing machine that runs code That's the whole problem in a nutshell. I highly doubt that is the road to a viable solution but I'm patient enough to be proven wrong in the longer term. But anything that is Turing complete automatically implies that anything layered on top of it will incorporate such niceties as being impossible to formally verify due to the halting problem. In other words: the only wa…

Not sure why you're being downvoted. This is the problem.

Whenever you want any guarantees about anything you implement a very restricted[1] subset of what a TM can do... at least if you're allowing users to input arbirtrary programs[2]. If you don't restrict to a non-TC language... you're -- in so many words -- fucked. (Hence the "hack".)

[1] Preferably using a statically typed PL, for obvious reasons. There's actually a thing these days where non-TC languages can actually "do things". My favorite moniker for this is "pacman-complete" (coined by Edwin Brady, I believe.)

[2] Having looked at a few .sol files earlier, they at least look TC, having general recursion and all.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#123

Post by vatotemking » Sat, Jun 18, 2016, 11:29 PM UTC

winteriscoming wrote: post #39

The apparent typo is odd, IMO. I don't know the language in which that program is written, but looking at that snippet, "Transfer" takes 3 arguments whereas the "transfer" function takes 2 arguments. Isn't there any code review involved when this makes into the codebase. Assuming there was some code review and the reviewer just missed it (which is very much possible), a basic unit test case would have easily caught t…

One of the hardest things in computer science: naming things

Re: Deconstructing the DAO Attack: A Brief Code Tour

#124

Post by quonn » Sat, Jun 18, 2016, 11:55 PM UTC

jacquesm wrote: post #112

whazor wrote: post #108

Earlier quoted context omitted.

Ethereum is a turing machine that runs code, programming languages are more high level. Creating an ADA-like language is trivial compared to making a scalable blockchain that supports computation. Ethereum itself is more bullet proof, as there are multiple implementations and the description of the protocol better defined and has proofs inside.

> Ethereum is a turing machine that runs code That's the whole problem in a nutshell. I highly doubt that is the road to a viable solution but I'm patient enough to be proven wrong in the longer term. But anything that is Turing complete automatically implies that anything layered on top of it will incorporate such niceties as being impossible to formally verify due to the halting problem. In other words: the only wa…

> But anything that is Turing complete automatically implies that anything layered on top of it will incorporate such niceties as being impossible to formally verify due to the halting problem.

Not sure I follow here... You can certainly run a non-turing-complete language on top of a turing-complete one and anything in that language could potentially be verifiable.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#125

Post by willtim » Sun, Jun 19, 2016, 12:21 AM UTC

pron wrote: post #101

willtim wrote: post #99

Earlier quoted context omitted.

I mentioned Lexifi, a contract language, which is based on OCaml and is not imperative. I restricted my argument to Europe as we appear to be less commercially influenced (e.g. MIT teach freshmen Python, Oxford teach Haskell). Predicting the future is always subjective. I offered only my opinion.

> I mentioned Lexifi, ... which is based on OCaml and is not imperative. Oh, sorry. > we appear to be less commercially influenced I don't think this has anything to do with commercial influence -- just academic tradition and maybe even philosophical influences: I think you'll get different answers to the question, "does an algorithm or a computation exist outside its description in a language, and if so, in what way…

It's worth pointing out that most of the formal methods you have linked to involve contracts or specifications as separate stratified layers written in various logics. No Turing Machines involved. This is essentially functional programming as far as I'm concerned. The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same, but I was not necessarily advocating their use as you seem to have assumed. Even without dependent types, a total functional program can serve as both an executable specification and a logic with which one can derive proofs from (e.g. via an SMT solver). This is what I meant when I said functional programming is more amenable to formal methods. So any tool that uses dataflow analysis to convert imperative programs into functional ones, or requires me to write functional programs to describe what the imperative program should be doing, doesn't provide a counter argument in my mind. Finally, in my very first comment, I provided a link to a startup who are planning on using FP and SMT solvers for formal verification of blockchain contracts, so watch this space...

Re: Deconstructing the DAO Attack: A Brief Code Tour

#126

Post by [deleted] » Sun, Jun 19, 2016, 12:37 AM UTC

vessenes wrote: post #93

winteriscoming wrote: post #39

The apparent typo is odd, IMO. I don't know the language in which that program is written, but looking at that snippet, "Transfer" takes 3 arguments whereas the "transfer" function takes 2 arguments. Isn't there any code review involved when this makes into the codebase. Assuming there was some code review and the reviewer just missed it (which is very much possible), a basic unit test case would have easily caught t…

I think after sleeping on it that I agree with you, this is more likely the outcome of bad refactoring. You can read the code commits on github if you like; I don't have them handy, unfortunately. transfer is a very poorly named function, of that there is no doubt. And Transfer is badly named as well. transferAndLockTokens vs LogTransfer would be much, much better.

[deleted]

Re: Deconstructing the DAO Attack: A Brief Code Tour

#127

Post by csarva » Sun, Jun 19, 2016, 2:03 AM UTC

Natanael_L wrote: post #105

jstolfi wrote: post #94

Earlier quoted context omitted.

> this typo apparently hasn't yet been fixed in the repos IIUC, once an Ethereum program is started, it cannot be killed or fixed. If so, updating the gitbub repo would be pointless at this time.

If it has a provision for forwarding all assets (with the necessary internal state detailed) to another address/DAO, then you can basically perform a migration to a fixed version.

There is no such provision. You can transfer the "balance" of a contract to another, but not any of it's internal state. This is left up to the programmer and AFAICT, they didn't implement this feature in the DAO contract(s).

Re: Deconstructing the DAO Attack: A Brief Code Tour

#128

Post by kartickv » Sun, Jun 19, 2016, 2:59 AM UTC

rbobby wrote: post #117

jacquesm wrote: post #2

Whoever thought it was a good idea to have case sensitive function names where the names are allowed to be identical but not identical in function? Major fuck-up there. That should have never passed the concept stage, nor the review stage. Function names should describe what a function does.

Case sensitivity in any programming language is crazy. I can't for the life of me see a valid engineering principal that accepts IsTheOne() and istheone() being different bits of code. Oh sure at a technical level the computer has no problem with... the problem is restricted to those oh so error prone humans. Can anyone here honestly say that if they were doing a code review they'd agree that solely a difference in c…

I don't know why you've been downvoted, but anyone who disagrees with you needs to explain in what situation it would make sense to have two different functions or files with names differing only in case.

I upvoted you.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#129

Post by winteriscoming » Sun, Jun 19, 2016, 3:05 AM UTC

This function will reduce user balances, before the vulnerable withdraw function is called. So, instead of the logging function, we should have:
if (!transfer(0 , balances[msg.sender])) { throw; }

This would .... also reduce the tokens available to the user later on

The more I think of the typo and the explanation about it in that article, the more unclear I am about that whole code.

Keeping aside this hack, for a moment, if that is indeed a typo and instead it should have called the lower case transfer method to really reduce the user tokens, then does this mean that all these DAO contracts (or whatever the right term is) that have been executed till date have been affected by this and as such the entire eco-system state was already messed up before this hack?

Nothing in that article suggests that this code flow, where this apparent typo is present, is applicable only for this specific hack.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#130

Post by kartickv » Sun, Jun 19, 2016, 3:15 AM UTC

jsprogrammer wrote: post #119

rbobby wrote: post #117

Earlier quoted context omitted.

Case sensitivity in any programming language is crazy. I can't for the life of me see a valid engineering principal that accepts IsTheOne() and istheone() being different bits of code. Oh sure at a technical level the computer has no problem with... the problem is restricted to those oh so error prone humans. Can anyone here honestly say that if they were doing a code review they'd agree that solely a difference in c…

IsTheOne() and istheone() are different bits of code.

That's a circular argument. They are different only because the language says they are different, while the post you've responded to says (correctly) that that's bad language design.