I have actually tested this attack technique (using my own contracts on a local test chain), and I've been in discussions with some Solidity developers and the guy who first published the attack. The situation is not as bad as this article claims. For starters, you can use address.send(x) instead of address.call.value(x)(). All computations on Ethereum have to be funded with "gas" (transaction fees), and send() only…
The situation is not as bad as this article claims. Well it kind of is actually. The people that wrote the DAO script had the script checked by lots of Ethereum experts and the bug slipped through. So if the Ethereum experts can't stop things like this happening then what chance do individual developers have. Basically creating a turing complete scripting language on the blockchain is not secure. No financial institu…
Ethereum is Doomed
181–190 of 217 posts
Re: Ethereum is Doomed
#182Earlier quoted context omitted.
I think we have a lot of theory about turing-complete computation. I really wonder why somebody would be willing to sign a turing-complete contract? The problem of understanding properties of the contract may be NP-hard [1] i.e. practicallly uncomputable. It may even be undecidable by involving instances of the halting problem [2]. [1] https://en.wikipedia.org/wiki/NP-hardness [2] https://en.wikipedia.org/wiki/Haltin…
It is undecidable in the general case as shown by Rice's theorem [1]. [...] Rice's Theorem may essentially be generalized from Turing machines to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs. [1] https://en.wikipedia.org/wiki/Rice%27s_theorem
The parent comment asks why someone would agree to a "Turing complete contract". But it's not necessary for an Ethereum contract to be "Turing complete" any more than Quicksort is "Turing complete". If the contract's code does something simple, we can verify and prove that it behaves as expected. It wouldn't be impossible to create a "safe" DAO-like contract.
Re: Ethereum is Doomed
#183Earlier quoted context omitted.
The whole point of Ethereum is turing completeness. Ethereum without Turing completeness already exists and its called Bitcoin. While this implementation of The Dao has failed, Ethereum is the only blockchain where implementing The Dao is possible.
This doesn't sound right to me. Contract law should not require turing completeness. First order logic should be more than sufficient. How does having a loop in contract law make any sense?
Re: Ethereum is Doomed
#184Earlier quoted context omitted.
I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.
> in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.
Re: Ethereum is Doomed
#185Earlier quoted context omitted.
The situation is not as bad as this article claims. Well it kind of is actually. The people that wrote the DAO script had the script checked by lots of Ethereum experts and the bug slipped through. So if the Ethereum experts can't stop things like this happening then what chance do individual developers have. Basically creating a turing complete scripting language on the blockchain is not secure. No financial institu…
Not a knock on your post, but "checked by experts" is like saying "QA looked at it". If the tools aren't in place to warn/prevent, re:"stop things like this", unintended executions are only going to continue. It is the brave new old world.
Re: Ethereum is Doomed
#186Earlier quoted context omitted.
It is undecidable in the general case as shown by Rice's theorem [1]. [...] Rice's Theorem may essentially be generalized from Turing machines to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs. [1] https://en.wikipedia.org/wiki/Rice%27s_theorem
Of course, that doesn't mean you can't prove anything. It just means you can't prove things generally and automatically. For example, you can't solve the halting problem in general, but you can most definitely prove that a specific program terminates, or that large classes of programs all terminate. The proof of Rice's theorem boils down to the impossibility of the halting problem. The parent comment asks why someone…
With the current system I imagine one could even utilize homomorphic encryption to implement another Ethereum inside Ethereum that is cryptographically protected not only against modification but also against inspection :)
Re: Ethereum is Doomed
#187I love that Smart Contracts act basically as bug bounties to make the Ethereum systems, community knowledge, and open contracts improve dramatically.
Re: Ethereum is Doomed
#188Earlier quoted context omitted.
Correct. Programmatic contracts should have democratized the entire business but instead this new scheme creates a new class of "lawyer".
I strongly prefer "laws" that are based on mathematics/computability theory than on social conventions.
We are thankfully very very far from a system of Laws which are anything like that. Such a system might be great in certain "sandbox" environments for manipulating resources that have carefully controlled interactions with the outside. But to have arbitrarily complex "smart contracts" running in the affairs of the real world? no thanks!
Re: Ethereum is Doomed
#189Earlier quoted context omitted.
Of course, that doesn't mean you can't prove anything. It just means you can't prove things generally and automatically. For example, you can't solve the halting problem in general, but you can most definitely prove that a specific program terminates, or that large classes of programs all terminate. The proof of Rice's theorem boils down to the impossibility of the halting problem. The parent comment asks why someone…
But wouldn't Ethereum be a lot safer to use if its contract system would only have so many degrees of freedom, that all side effects and properties of contracts were computable for all contracts in a practical amount of time? With the current system I imagine one could even utilize homomorphic encryption to implement another Ethereum inside Ethereum that is cryptographically protected not only against modification bu…
Maybe we'll also discover a handful of primitive contract building blocks, to be implemented with care and stringency, with methods for combining them.
Re: Ethereum is Doomed
#190> Solidity is like programming in JavaScript, except with your bank account accessible through the Document Object Model. Such a beautiful, terrifying sentence.
This is a very snarky hyperbole. Solidity has as much to do with Javascript as Java does. For starters, Solidity is a compiled, typed language. It is still new and has to be improved.
The same language can be both compiled and interpreted, this doesn't affect the semantics of the language. For example, OCaml ships with both a compiler and an interpreter. There exist AOT compilers for JavaScript too.
Also, JavaSript is a typed language. It is just dynamically typed and does too much type coercion.