Live data from Hacker News

Deconstructing the DAO Attack: A Brief Code Tour

vessenes.com

101–110 of 167 posts

Re: Deconstructing the DAO Attack: A Brief Code Tour

#101
post #99
post #82

Earlier quoted context omitted.

> Research FP languages like Coq have enabled INRIA to build a fully verified C compiler (Compcert), can your tools accomplish this? First of all, end-to-end verification is something very unique. CompCert is a great accomplishment, but it is only a medium-sized program, it required a world-expert to write, and even then it tool a lot of effort and still he skimped on the termination proofs. Imperative tools, OTOH, a…

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?" This may be tied to actual philosophies, Derrida in France vs. Kripke in the US[1] (to prove the connection, a "Kripke structure" is a very common mathematical structure denoting an "abstract" computation, which is used commonly in non-language-based verification). I've been told that the study of program semantics tries to reconcile the two.

As to Haskell vs. Python, first, MIT used to teach Scheme; they have explained their reasons for switching to Python. Second, this difference is more indicative of the competition between "theory A" and "theory B". Theory A studies algorithms and complexity (and Haskell is not the best first pedagogical choice for that), while theory B studies logic and semantics (and language). Theory B is relatively small, but it does have a stronger presence in Europe. Although, even within theory B there seem to be those who prefer linguistic approaches (semantics) and those who prefer conceptual approaches (Kripke structures, abstract machines).

[1]: Not that Britain is too fond of French philosophy, but the Brits had Robin Milner, who is as close to a CS deconstructionist as you could find.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#102
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.

Are we sure that case sensitivity is the culprit? As others have noted, the function being called takes (and is given) 3 arguments but the function that is supposed to be called takes only 2.

IDE and autocompletion could be the direct cause, but in the end if the function had been properly named it wouldn't have happened (root cause).

Re: Deconstructing the DAO Attack: A Brief Code Tour

#103
post #87
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…

> It's nice that Vitalik Buterin is a genius, but it shows that this guy is only 22 and dropped out of university because anyone with a degree in computer science knows about this stuff Personal attacks, which this crosses into, are not ok on Hacker News. Please edit such stuff out of your comments here. We detached this subthread from https://news.ycombinator.com/item?id=11928562 and marked it off-topic.

[deleted]

Re: Deconstructing the DAO Attack: A Brief Code Tour

#104
post #22

Earlier quoted context omitted.

Because it is an insanely interesting problem to try and solve technically. That is, a medium of exchange is essential to a modern economy and yet how to objectively regulate the supply of that medium of exchange without exploitation can be considered somewhat of a paradox. The quest is to solve the paradox via ever evolving technological solutions.

objectively regulate There's your problem. Such grandiose visions might have passed for a 1930s-era technocrat, but are laughable today.

> objectively regulate

I think you misunderstood...regulate as in increase or decrease the creation of the medium of exchange through technology, not government entity.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#105
post #94

Earlier quoted context omitted.

If I understood the explanation on that article correctly, what's even more interesting is that this typo apparently hasn't yet been fixed in the repos (assuming I'm looking at the right ones). There are 2 repos which I looked at: https://github.com/slockit/DAO https://github.com/TheDAO/DAO-1.0 I don't know which one is the authoritative one. But the interesting bit is both these repos still have that same typo in th…

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

Re: Deconstructing the DAO Attack: A Brief Code Tour

#106

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…

This is what I wanted to ask about. I don't even know what language this is. Is Transfer even a legit function, and if not, does this language just keep on chugging for non-existant function calls?

The language is Solidity (https://solidity.readthedocs.io/en/latest/) which runs on the Ethereum VM.

Certainly one of the challenges for the project is implementation and security issues in the Turing-complete language they decided to create for the purpose of smart contracts. Postscript and ActionScript have probably averaged a security flaw a month for the last decade; I can't imagine getting Solidity correct from the start.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#107
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.

Or a malicious one. The move has to be voluntary.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#108
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.

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

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.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#109
It reads like the debugging that you've done a million times if you are working with ordinary, mutable, C-family code.

To start off with, you think you're developing a valuable skill in being able to follow a call stack along with a bunch of variables. It certainly has its uses, but after a while you come to wonder why it always ends up this way. Sure, you can understand every bug eventually, but surely there's some reason why you're constantly reasoning about the state of the variables and the order of the function calls. You can write unit tests, but of course you can't think of all the undesired behaviours beforehand.

The author does mention that something functional with strong types is necessary. Probably a good idea.

As for the split function, there's a question of whether it is really necessary. I wouldn't have thought an investment fund would need a split function. An ordinary fund doesn't; if you're in, you're in for whatever proportion that you've put in. Why not just make a second fund with the same (reduced) code if you have some other group of investors? More functions = bigger attack surface.

Re: Deconstructing the DAO Attack: A Brief Code Tour

#110
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.

I couldn't agree more with this sentiment. I haven't spent too much time on Ethereum contracts but this is such a ridiculous language/platform design issue.

Funny thing is, it reminds me of implicit typing of int/float based on the first letter of the variable name that ye olde FORTRAN77 had as a major footgun.
Post reply on HN