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 forwards a small amount of gas. The recipient can write to the log but that's about it. TheDAO used .value() which forwards all the available gas.
If you do use .value(), then you can do it safely by doing it only once per method, as the very last step, and only using it in top-level methods. Then any sort of reentrant callback will find any required state changes already done. E.g. subtract from the user's balance, send the funds, and if the send fails then throw. The recipient can call back but the balance is already decremented. Using a mutex is another option. I've tested all this and it works.
There are a lot of reasons Ethereum is designed this way. The most common reason for a contract to run code when receiving funds is to prevent users from accidentally losing their money. E.g. in any contract that holds ether and maintains a ledger with balances for multiple users, if anyone sends ether to the contract address, they'll lose it, unless the contract either throws an exception or automatically adds to the user's balance on its ledger.
User addresses and contract addresses are interchangeable, because it lets you do things like use a multisig timelocked vault to receive funds and anything can send to it just as if it were a regular user account.
All that said, the devs are working on improvements too.
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 institution will risk creating smart contracts on this platform.
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.
Nope, Serpent is a different language that compiles to the EVM, and Krug just noticed that by default, a send in Serpent includes more gas than Solidity does, opening a door to unexpected attacks.
Solidity is the official supported language, Serpent is an earlier and slightly lower-level language that some people still use. I expect they'll fix the gas default.
> All computations on Ethereum have to be funded with "gas" (transaction fees)
But that's what was wrong with the exploited DAO code - it didn't use gas. The point of the article is that it's very hard or impossible to verify the correctness of the smart contracts.
The programming classic "Mythical Man Month" had a chapter for the "second system effect". Its where developers put lots of complicated features in to the second system in a series. Its a pattern for failure.
In this case, Ethereum developers built a much more complicated cryptocurrency by making it Turing complete - to the extent of writing their own new computer language and virtual machine to run it.
They skipped over the halfway step of declaring parameters in the payment transactions, that open source enterprise library code, e.g. Java, could execute for for required behavior. No. They made the new code itself a user-contributed and immutable! part of the system.
That's actually a pretty good decision in my opinion. At least in this case. Think what would happen if they went for alternative solutions:
1. If it wasn't immutable, you'd never be sure when a contract changes. That's the basic assumption about contract - once you sign it, whether in real world, or by doing some action in Ethereum, you don't expect it to change how it works. That's why immutable is good.
2. User-contributed is just how it's supposed to work. It's decentralised. Everyone's a user. The content has to be user-contributed. Having some central publisher/gatekeeper is contrary to the whole idea.
3. Own VM is debatable. Sure, they could go with JVM, but the scope would have to include much more complexity (classes, namespaces, etc.) than just function/instruction execution. Maybe the limits of javacard would be enough, maybe not.
I really don't think the second system effect applies here. It's not a rewrite of something that existed and had issues.
Solidity contracts are already modules which contain functions. They're equivalent to Java classes with static methods or Scala objects. As for namespacing, I don't know how in this day and age programmers can say that's not worth it.
Solidity contracts do contain functions and some state. But that's at a fairly different level than Java's classes. Internals are not exported. The contract's structs belong to contracts. There's no need for namespaces within code because addresses provides namespacing already - all your code is normally visible to you already and you'll not get unexpected names shadowing anything in your code.
I'm not saying namespacing is bad, just that namespacing as defined in Java is likely not necessary in ethereum world, as I understand it. It would likely just confuse what's immutable vs what's referenced by name.
Turing-completeness was the entire conceit of Ethereum, as I understand it- without that you would have Bitcoin with a few bells and whistles, and no one would bother. And once you're committed to that, a new language and environment are essential- something this entire fiasco shows is that a language for contract programming has very different requirements than what software engineers are currently used to, in order to be safe in ways that don't apply to ordinary software.
In all likelihood, a working and reliable Ethereum simply requires computer science theories we don't have yet. A working Solidity would probably look something like Ada, but with types and invariants the likes of which we've never seen. Its potentially a very interesting research subject! But for now, yes, investing in Ethereum is like climbing aboard in a rocket aimed at Mars- exciting and futuristic, but unlikely to get you where you hope to go.
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].
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.
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 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.
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 but also against inspection :)
I'd love to see an example of such a restricted contract language. My speculation is that we'll see a few different languages pop up with different approaches to safety, along with coding methodologies and tools for static analysis.
Maybe we'll also discover a handful of primitive contract building blocks, to be implemented with care and stringency, with methods for combining them.
> The problem of understanding properties of the contract may be NP-hard [1] i.e. practicallly uncomputable.
The difficulty makes good contract design a valuable service (like hiring lawyers). Otherwise everyone would just write their own contracts. A more declarative, less powerful language would have opened this up at the expense of contract succinctness.
Is it a case of Second System Effect, or Build One to Throw Away? I don't have an opinion either way, but just pointing out that the very same pattern is also known as a successful one in some cases.
Build one to throw away means you're building the same "system" again, but with more specific requirements based on what you learned. Second system effect is building a bigger system will broader and vaguer requirements.
(Also, Brooks later said: "This I now perceived to be wrong, not because it is too radical, but because it is too simplistic. The biggest mistake in the 'Build one to throw away' concept is that it implicitly assumes the classical sequential or waterfall model of software construction." He wrote a later book, The Design of Design, encouraging iterative development.)
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.
Thanks for the clarification. So, Solidity is a compile-only, strongly typed language? While Javascript is usually interpreted (or JIT compiled) and dynamically typed.
Having a little bit of trouble parsing how the attack worked -- so when a transfer happens, the destination account gets to run a command; they then ran a command that called the source's send-ether command, which ran because it was still in 'we owe destination account money' mode because the full initial contract had not concluded?
Then at some point it terminates itself before emptying the source account (and thereby causing a rollback that would cascade back?)
You've nailed it. In this case, the call stack depth would halt you before TheDAO runs out of funds, though. So you end up with some multiple, say 30x, where you can put in 1 ether and drain 30 ether. There is about a month lockup period during which your seed cash and your multiplied cash is frozen.
What made this particularly devastating is that there was a second bug which allowed the attacker to transfer their token that represented that first ether back to the DAO. So instead of 30x return, they could eventually drain the whole DAO (although they stopped after the discussion of a fork began).
If you overflow the stack it throws and rolls back (which is another attack in certain circumstances). What killed TheDAO is basically that childDao called back the sender method, which sends again without having deducted yet.
Do the deduct before the send, and the whole problem goes away.
It's not really concurrent, the VM runs one transaction at a time.
The send returns false if it fails. So if you check for that, you can throw an exception, which rolls back the whole transaction just like in SQL.
The reason the send doesn't automatically throw is that if you were doing lots of sends in a loop, you'd actually want to ignore the exception, so if one send fails it doesn't block everybody.
>if you were doing lots of sends in a loop, you'd actually want to ignore the exception, so if one send fails it doesn't block everybody.
This sounds like the wrong default behaviour. If we're talking about sending money, and there's a list of people to send money to, I would say that the default behaviour should be to throw an exception, because if not you could end up having money not be properly redistributed.
For example, a simple smart contract to share costs. If one member not longer participates then shouldn't their cut be given to the remaining participants?
The fact that it doesn't roll back everything by default concerns me quite a bit...
You can accomplish that by checking the return value. But Solidity doesn't have try/catch, it just rolls back everything upon throw. If send() were to actually throw upon failure, then it would roll back the entire method call and nobody gets paid. A troublemaker could use an account that always throws when it receives funds, and permanently block all payouts for everybody (unless a contract admin has a way to kill accounts).
The best pattern is not to put sends in a loop at all. Just update a ledger inside the contract, and have each user call a withdraw() function to get their money. That way if you're careful you can even use call.value, so users can include as much gas as required, and can withdraw the money directly into any sort of contract they like.
Sending before deducting the money seems like an obvious design flaw that should have raised red flags. Is there any explanation for why it was implemented this way, and why it wasn't spotted by the developers?
Ethereum isn't doomed. I don't think it will ever have as much backing as Bitcoin because of institutional buy-in; but the world needs programmable smart contracts. Some rich soon-to-be-dead billionaire tech nerds want to be able to do something every year without worrying about a judge taking that away from them. Individual will is what cryptocurrencies are about. Bitcoin in terms of international payments and store-of-value; and Ethereum in terms of contracts and computing.
Ethereum is doomed, and not just because it's based on a poor design. It's doomed because it just shot its credibility to shreds by protecting a single, uniquely privileged contract. Forking proves that the ethereum network cannot be trusted as the neutral contract arbitrator it was designed to be.
The idea of smart contracts is an interesting one, and perhaps another project will come along and do it better. But Ethereum won't be that project.
Based on a poor design? according to who? It's the most advanced blockchain out there by far and wide! This was a single contract with a flaw, it's like saying the whole internet is doomed because some website got a SQL injection.
I don't think "most advanced blockchain out there" is actual praise. Systems, especially systems that are meant to serve as a substrate for more advanced systems must be simple to understand and reason about. Making the foundation turing complete is indeed poor design.
Turing completeness is not an implication of poor anything. All it does is remove certain kinds of generality from your proofs. You can still prove things, you just have to be careful stating what the assumptions are.
So you mean to tell me that taking away the ability to write generic programs to validate contracts is good design? See Rice's Theorem (https://en.wikipedia.org/wiki/Rice%27s_theorem). Once you have turing completeness verifying any non-trivial program property starts requiring grad school experience and real proficiency with writing and verifying proofs. Most people, including programmers, do not have the training nor the discipline to actually do what you suggested.
In practice the assumptions you mention turn out to be assumptions about totality and termination of certain building blocks and so you are back to a restricted subset of the language which should have been the original language to begin with but instead of automatic verification you have turned the problem into manual labor. Thinking about this more I agree with the naysayers. Etherium was a good experiment to show people what they should not put into a smart contract system.
.and that PhD computer scientist will have a contract that he/she cannot be held responsible for anything bad that happens with the code he/she writes. Written by a juris doctor lawyer. :)
I think this is the core flaw in the mindset of Ethereum adherents: the very idea that it is even possible to have "Laws" which are completely objective to the point of mathematical logic and that these could/should be enforced, literally, by a computer running a program.
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!
So, just write your contract in a non-turing complete subset of it. Just because the power is there doesn't mean you have to use it if you don't want to.
According to the article, you need to write interfaces that accept a function and call it somewhere down the line. At this point you already cannot guarantee the lack of recursion, simply because the supplied function can call your function again. It is simply not possible to write a code that always halts, unless you never even call the supplied function.
There's a difference between general recursion and bounded recursion, and you can very easily constrain recursive functions to terminate, especially if you're in control of the data they must pass around.
You just made my point. The Ethereum designers have offloaded all the hard work onto others. What value do I get out of this platform if I'm doing all the hard work?
Solidity language makes very hard to write safe code:
Is Ethereum/Solidity Suitable for Secure Smart Contracts?
It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power reactor, than to writing loose web code.
Yet the current Solidity language and underlying EVM seems designed more for the latter. Some misfeatures are:
A good language for writing state machines would ensure that there are no states from which it is impossible to recover.
A good language for writing state machines would make it painfully clear when state transitions can and cannot happen.
A good language for maintaining state machines would provide features for upgrading the security of a live contract.
A good language for writing secure code would make it clear that there are no implicit actions, that code executes plainly, as read.
The current language does not fulfill any of these commandments, and in fact, the last one, involving implicit recursive calls, is what did The Dao in.
The SlockIt team even had the designer and implementor of Solidity perform a review of their code. If he cannot get something like The DAO to be secure, no one can.
I think you're thinking of use cases that would definitely be stopped outside of ethereum world:
> Some rich soon-to-be-dead billionaire tech nerds want to be able to do something every year without worrying about a judge taking that away from them.
You can do things like this, but the law either already covers this, or will adjust. If you gain money, you're expected to pay the usual tax on that gain. First few may get away with it, but once it becomes popular, audits will start.
> Individual will is what cryptocurrencies are about.
Same as above - inheritance tax.
Essentially it's this xkcd situation: https://xkcd.com/1494/ Just with wealth gain and tax office instead.
The point of Ethereum is to provide something that is different from the real world. If not, it is simply fiat, except that it is 1000 times more inefficient and burns up loads of electricity.
You cannot rely on the law to treat your wishes long after you are dead. The largest park in Toronto (High Park), for example, should technically not be owned by the city because the person that bequeathed it to the city said that it would revert to some other organization if a catholic was ever elected mayor, but that never happened.
As for XKCD - where something happens is no longer clear cut. If someone creates a etherium contract during a year in Argentina while SSH'd into a computer in Hong Kong it starts to become very difficult to enforce the law.
I'm not even talking strictly about tax evasion I'm talking about subversion of the states restriction on individual action - and I agree that this isn't a good thing across the board. I don't like the idea of billionaires hiding their influence and wealth, I just think it is inevitable.
Some people are willing to trade goods and services for Bitcoin, just like they would dollars.
I don't think it's relevant what the person receiving the Bitcoin does with it after (converting directly to dollars, holding, or buying other goods/services), since those are the same things people do with regular dollars anyway.
> Some rich soon-to-be-dead billionaire tech nerds want to be able to do something every year without worrying about a judge taking that away from them.
Billionaires still have nexuses with the physical world. The machines which execute their code, for example, can absolutely be affected by court orders. So too can their homes, their cars, their planes, their drones and of course their person.
There's a brand of techno-utopianism that assumes that if it's virtual, it's magically immune from the whole mechanism of law. This has never been true. The law asserts itself to be omnipresent in all human affairs and -- unlike a computer program -- the law's power is accepted at face value by billions of people and underlined by men with guns and dogs.
>the law's power is accepted at face value by billions of people and underlined by men with guns and dogs.
emphasis mine. I find that last bit, though, to be super interesting; "enforced by men with guns" has always been a big part of the rhetoric of any discussion of law, anarchist, or libertarian thought.
But... I'm not sure I've ever seen dogs mentioned in that context.
A contract-based blockchain seems very likely to me. But there's no reason that has to be Ethereum. Having had the chance to sort of ponder this over the last couple of days, I can't help but come to the conclusion that Ethereum is indeed fundamentally flawed and probably entirely unsalvageable, for all the reasons given in that blog post and more. The eventual contract-based blockchain that succeeds is going to look a lot more, well, engineered, for lack of a better word. Probably a lot more proofs of various things. Fewer features that are all individually much stronger.
In fact, there's little reason to believe that something this complicated would be done correctly the first time. Remember... Bitcoin is not the first digital currency either!
> Some rich soon-to-be-dead billionaire tech nerds want to be able to do something every year without worrying about a judge taking that away from them.
But apparently it only takes a fork to freeze/reverse their contracts. I would take my chances with a traditional foundation, Alfred Nobel's is still running smoothly since +110 years ago, yearly executing its "code".
> want to be able to do something every year without worrying about a judge taking that away from them
Except we're just about to prove that an institution can decide to nullify a Ethereum contract with the soft/hard forks. In the very best case that will a cabal of miners with unknown intentions (and clearly they're not too invested in the Libertarian "code is contract" angle of the network) instead of a democratically constructed judicial system.
"without worrying about a judge taking that away from them"
Unfortunately the ultimate arbiter of the courts' authority is not a piece of code or a piece of paper, but the courts themselves. If someone disputes the authority of a contract (smart or otherwise) that dispute will ultimately be settled in court. Even if the contract contains language claiming that it is not open to interpretation by a certain court or set of courts, the validity of THAT language will ultimately be interpreted by... a court.
There is no degree of technical cleverness that can supersede the authority of a sovereign entity. You can hide things from a sovereign, move things out of the reach of a sovereign, but you can never overrule a sovereign's authority within its own borders.
RTFA. The idea of smart contracts isn't dead, but Ethereum looks like a terrible platform for it, given that it's very hard to audit the smart contracts on it.
I agree with your sentiment but downvoting because the guidelines specifically ask that you not say things that imply a commenter hasn't read the article.
The problem with Turing completeness is that if it's not there from the start, people inevitably end up needing features that aren't present in the restricted language, and then a Turing complete language is added to either the original system or a successor, and being an afterthought it usually ends up being a hack job.
Examples: SQL was supplemented with procedural languages for stored procedures, Excel was supplemented with VBA, HTML was supplemented with JavaScript and, well, Bitcoin was supplemented with Ethereum.
So providing a Turing complete language was the right decision as far as it goes, but it's not enough by itself. If you need reliability - which this does - it needs to be the case that typical code does not involves arbitrarily complex computation. Typical code needs to fit stereotyped patterns whose behavior is predictable.
If Ethereum is to continue, it's clear that exhorting people to try even harder not to make mistakes in the current version of Solidity, won't cut it. The language needs to be supplemented or replaced with something that makes it easy to write correct code for the kind of things people typically want to do.
There are languages which are both expressive and Turing incomplete, for example Coq. In the Coq language, Turing incompleteness is actually needed to be able to make complete proofs. Maybe Solidity would have been better implemented within Coq, but it's too late now.
Is it too late now? It seems to me that it should be possible to implement a better language on top of the existing system, there are plenty of languages that compile to JavaScript after all, so it's still worth discussing what a better language might look like.
You say Coq is expressive; okay, but in what sense, for what purposes? A language which isn't Turing complete - or even one which is - isn't going to be expressive for all purposes. As I understand it, Coq is designed to be expressive for the kind of things people doing research in type theory want to write, in the same way SQL is designed to be expressive for database queries.
What sort of things do smart contracts typically want to say? Are they more similar to type theory research, database queries or something else?
One possible answer is that it's too early to say yet, in which case perhaps extensibility is an important attribute. For example, suppose Racket were used as a language for writing smart contracts, with a backend to generate Ethereum byte code. Being a dialect of Lisp, Racket is highly extensible. It also has an optional type system. Do smart contracts tend to be prone to the kind of errors that are caught by a type system? If so, it would be worth using one.
Note that Solidity is not JavaScript, it's just superficially similar in some ways. The comparison with JavaScript is for marketing pretty much.
In particular, Solidity is statically typed.
I would say that smart contracts are a lot like event processors that update bits of contract-local state and enforce preconditions. They are run in a single "thread" in blockchain order, but they can also invoke each other reentrantly (and that's the major source of confusion so far, so it should be limited and made very explicit).
Some contracts perform more complex calculations, e.g. I know of one that calculates compound interest using fixed point math.
There might be room for several different simpler languages for different purposes... It would make sense to use the most restricted language that can express the contract you want.
From what I've seen of the discussion on this, you're right about uncontrolled reentrancy being a big source of problems.
One thing that occurs to me: would the command-query distinction be a useful notion here? I have no truck with it in the general context in which it was coined, but in this context maybe it would be useful to draw a hard line distinction between 'I call you to ask for information' and 'I call you to ask for money'.
Solidity contracts can define "const" functions which aren't allowed to change state.
For some uses you can also look at the events that a contract emits, which are indexed and searchable off-chain... so client apps can read them, but not contracts themselves.
Okay, so const was available as a feature - but not used because it wasn't the default? Some of the discussion on this seems to be saying Solidity supports exceptions and transactions, which should provide a lot of safety here (on error, an exception should be thrown and everything the script just did should be rewound) but the documentation was still exhorting programmers to check return values all over the place. Is this at least in part a matter of bad defaults? I'd be quite prepared to believe so; bad defaults are a much bigger problem than they are sometimes thought to be.
Interestingly, Coq is expressive enough to write arbitrary computations; for example, you can write a Universal Turing Machine emulator; or, more realistically, many people write programming language implementations in Coq, in order to prove results about them.
However, Coq can only run those computations for a given number of steps; in other words, you can't say "run this until it halts, and give me the result", but you can say "give me the result after 3^^^3 steps, or 'Nothing' if it hasn't halted by then".
The reason this is interesting in this discussion is that Ethereum uses "gas" in a similar way.
That particular thesis actually ends up recommending against using a dependent functional language for Ethereum contracts...
I think we might need to think of contracts as very important algorithms and prove them like we prove quick sort. That doesn't require dependent typing and functional programming; you can prove theorems about imperative code if you just have formal semantics.
I'd be interested to see a verified dependently typed compiler to EVM for some simple language... but it kind of seems like a PhD project.
Coq is pretty specific in what it does like css (also Turing incomplete. There is a pretty low bar for features needed to make something Turing, it doesn't take much more then mutable variables and a while loop or recursive functions to impliment rule 110
you are thinking of this[1], it relies on a human following directions due to css not having any ability to calculate rules based on the results of other rules so if that was turning complete then by the same logic a piece of paper with instructions for how to do rule 110 would also be turing complete because a human could use that to calculate rule 110.
Yep, yep, and if contracts were written in Coq or a similar language, it would be easier to formally prove that they are "safe" from smarty pants hackers..
That would be a really nice application for formal methods, it seems.
People (rightly) make the same critique of Bitcoin: it is very easy for regular people to lose their money. To keep it safe you need to be a security expert, and even then there are no guarantees, and mistakes are forever.
My response is the same for both Bitcoin and Ethereum:
Even if these technologies are only used by trained professionals, they can still be revolutionary. Almost no one can safely operate a printing press, and yet that invention has toppled empires.
At worst, these are back office technologies. At best in a decade or two someone will figure out how to design a good enough GUI that a novice can safely explore a powerful subset the technology, trusting that bumpers are in place around the sharp edges.
People at large are not supposed to put money in printing presses they can't use properly, they are supposed to put money in books made by those printing presses.
Ethereum is definitively unsafe, it's basically impossible to create code without any bugs, and it's impossible to prove a piece of code doesn't have any bug. That defeats the all purpose of Euthereum.
Bitcoin is just unsafe by nature for the user, although the protocol itself is most probably safe.
It is doomed, who would trust a contract now with real "money"? Unless you have a mathematically rigorous proof that the contract is trustworthy I sure wouldn't.
Sorry, but this is bullshit. You sound like Ethereum or SlockIt employee. No one in their sane mind would trust their money a company which can't guarantee security of your funds, let alone good coding practice (the DAO code is shit, sorry -- there are no tests, no comments, no spec, no clear upgrade story etc.). Good attempt, and I can feel for Ethereum folks, but something this important should be rock solid, not "experiment" when you're fucking with people's money. This is not a hacker's playground.
"I thought again about my early plan of a new language or writing-system of reason, which could serve as a communication tool for all different nations... If we had such an universal tool, we could discuss the problems of the metaphysical or the questions of ethics in the same way as the problems and questions of mathematics or geometry. That was my aim: Every misunderstanding should be nothing more than a miscalculation (...), easily corrected by the grammatical laws of that new language. Thus, in the case of a controversial discussion, two philosophers could sit down at a table and just calculating, like two mathematicians, they could say, 'Let us check it up ...'" --Gottfried Wilhelm Leibniz
I didn't know the language was turing complete. Isn't this computing 101? If you want a secure thing then you must be able to reason about it statically. Making things turing complete means any non-trivial property of program correctness can not have a generic solution and so you've just opened yourself up to a world of hurt.
Another VC funded outfit I chatted with also boast of TC. This is, I agree with you, software engineering 101. But that's probably it: don't know about you, but I could not stomach making a pitch for funding for the latest hype [1] knowing that the fundamentals are unsound.
I am hoping that the recent events -- Theranos, out-smarted contracts, etc. -- will permit a return to maturity in this field. Money has poisoned this field.
[1]: wrote about (genetically) evolving cellular corporation back in '96 so this is not a case of I don't get it.
You could always run the program on a fake, mock state then test postconditions for sanity. So, if those postconditions pass and we haven't run out of gas, run the program for real, otherwise return an error.
Eg transferring 30 eth from contractA to contractB you would have one of the postconditions asserting that ContractA balance is the old balance minus 30.
The notion of gas implies a stack or effort limit, so it's guaranteed that any operation will eventually fail once it runs out of resources. Thus you can specify a theoretical upper limit on resources used in pre-verification, which (AFAIK)is paid by the client contract that requests to withdraw money from the other contract.
I guess one could avoid this by using a DSL that is formally verifiable, but it's still an interesting option
Yes, I'd assumed since Ethereum was so highly touted and hyped that the foundations of the entire thing were sane. Well I mean sane in the sense that the actual contract language was as restrictive as possible and custom made for expressing contract law but it turns out you can do arbitrary computation and although in theory you're limited by this gas thing because the language is not formally specified and verified it is not clear at all if there are no other bugs lurking around with respect to bypassing the gas bounds.
What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece.
> What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece.
Actually, termination checkers often compare the size of the term being reduced before and after an evaluation step, and if it can prove that it's always smaller, then termination is assured. With the notion of finite amounts of gas, termination seems assured, so this termination analysis can (and should) be added to EVM.
Based on this termination property, all sorts of static analyses now become possible.
You can reason statically about turing-complete languages. They just have to be syntactically restricted to forms amenable to mathematical analysis. Ethereum's scripting language is poorly designed for this.
Many high-tech fintech digital contracts are written in languages like Haskell or Ocaml. Fintech people value strong types, declarative programs, immutability, etc.
Correct. That is what I mean but you still don't just want a restricted subset. You want something that guarantees termination and also lets you reason about any weird runtime behavior and resource usage in a very rigorous way. Some of these things are still research problems and some of them are barely becoming practical in languages like Rust.
You usually get that through a restricted subset of an otherwise turing-complete language. The standard approach is to impose a finite metric on the arguments of a function and demonstrate that, as the function recurses, that metric monotonically approaches zero.
>barely becoming practical in languages like Rust.
As far as I know, this cannot be done in Rust. Agda, Coq, and Idris are the primary languages supporting termination checking (because they are syntactically suited for it). Haskell supports it as well through Liquid Haskell.
I meant reasoning about resource usage. Rust provides lifetimes which I think is based on linear logic (see https://news.ycombinator.com/item?id=7061876). In theory, this gas thing should act as the metric you mentioned but it doesn't seem like it is implemented properly when it comes to how the fundamental building blocks of Solidity act with respect to the gas metric. The termination stuff in total languages I think has a ways to go in terms of general accessibility. Dependent types aren't the easiest thing to pick up.
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?
There are also a class of total languages (Coq, Agda, Idris) that are guaranteed to terminate but admit (polymorphic) recursion. This is stronger than FOL but weaker than turing-completeness, and certainly sufficient to implement any feasible contract.
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.
But : https://en.wikipedia.org/wiki/Solidity "As specified by Wood it is designed around the ECMAScript syntax to make it familiar for existing web developers;"
I don't think accessibility is a bad thing. I think computing, its practice and theory, should be taught the same way we teach literacy. I didn't mean "average" as in "incompetent". If writing contracts was as simple as writing a few lines of code in some formal language that didn't require a law or finance degree then I would consider that to be a good thing. It would be even better if the system was designed from first principles with solid theory backing it.
I totally agree, but the reality is that in order to write contracts that are sure to be correct, you need a level of expertise that involves much more work than just learning how to write programs. Knowing the syntax and usage of a rigorously-typed language like Agda is the easy part.
Then the platform is flawed. Average programmers should be able to understand it easily.
It's not that hard, some wants X and some wants Y in exchange.
I'm not a lawyer but I write contracts with my clients. If you keep things simple it should fit most people. making g smart contracts complicated you keep it in the area of a small elite who are knowledgeable of playing safe with it.
There is a thing that advertises itself as being like Ethereum but without the Turing completeness.
It is meant to be able to do more computation based stuff than Bitcoin, but without being Turing complete.
However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.)
>However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.)
> [...] has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses. Adam has also constructed a 4,888-state Turing machine that halts iff there’s a counterexample to Goldbach’s Conjecture, and a 5,372-state machine that halts iff there’s a counterexample to the Riemann Hypothesis.
I didn't mean that the two aren't related, just that they aren't as strongly related as the group seemed to be implying. They were saying that Ethereum being turing complete made it inconsistent in some way.
But yes, the two definitely are connected.
For example:
A program which could solve the halting problem would be able to determine whether a given system is consistent.
So, as a result, if a system could prove that a program solved the halting problem, and it could simulate programs running, then it could simulate the program that solves the halting problem being applied to a program that searches for inconsistencies in the system. This would allow it to prove whether it is itself consistent.
Therefore, by Godel's second incompleteness theorem, a system which can simulate programs for any number of steps, and which is consistent, and which can do arithmetic and such, cannot prove that any particular program solves the halting problem.
Admittedly, this is a lot weaker than "no program solves the halting problem", but I think it is a fairly clear connection.
So, yes, I agree that they are related.
But Ethereum's Turing completeness (or, Turing completeness except being limited by gas costs), does not mean that Ethereum is "inconsistent", because that is, uh, pretty much a nonsense claim. And that is the claim that I think the other group was making (Though they may have stopped making it since.)
Also, btw, wrt that blogpost, they got the number of states for a machine which ZFC cannot prove does not halt, but which does not halt, down to, iirc, like 2030 ? But you probably knew that already because it is the next blogpost on there.
You heard wrong. Regex is specifically not turing complete. It corresponds to the class of machines called DFAs. Above regexes are CFGs, which correspond to pushdown automata. Above CFGs are CSGs, which correspond to linear bounded automata. Above CSGs are unrestricted grammars, which correspond to turing machines.
You may be thinking of PCREs, which aren't actually regular expressions, but are sometimes erroneously referred to as such. I don't know if those are turing complete or not.
By definition regular expressions are not Turing complete... There is an ordering relationship between turing machines and regular expressions which explicitly states regular expressions are strictly a subset of turning machines. This is automata theory 101. Ask for a refund from your school.
As expected, "Ethereum is turing-complete" turned out to be just a marketing meme (or a horrible idea at best), just like "Litecoin is silver", "Doge is community", and all the others.
I love how law and court systems are basically bug bounties on legal systems, community knowledge, and social constructs. Society will inevitably improve dramatically.
Oh wait, no. We just turned programmers into politicians and lawyers. I think more people will be pissed when they find out that "trust in the system" ultimately means "trust the writer of the smart contract".
Unlike law, which has admitted that insane things happen and provides "emergency stops" (ie: Supreme Court can say whatever the heck they want and provide a check against any of Congress's laws)... there isn't really a way to add human "emergency stops" to the equation of Ethereum.
I hear your sentiment. But not your argument as much. Politicians and Lawyers are inherently > smart contract writers?
'I think more people will be pissed when they find out that "trust in the system" ultimately means "trust the writer of the smart contract".'
How is this different than not trusting Lawyers?
'Unlike law, which has admitted that insane things happen and provides "emergency stops" (ie: Supreme Court can say whatever the heck they want and provide a check against any of Congress's laws)... there isn't really a way to add human "emergency stops" to the equation of Ethereum.'
Agreed on using Ethereum contracts anytime in the near future (or ever) for anything life or death or over exposing your self financially is insane. There are plenty of cases that are a better fit for a smart contract system. People should invest affordable proportions of their money.
Except that once theere's a lot of money in smart contracts, people will hack the contracts without letting people know. Somebody's going to complain about "losing all their money in a contract and they don't know why" but they'll be ignored as technically ignorant and in the meantime, the thief will walk with lots of money.
Probably quite difficult in practice, unless he/she could somehow convince a mining pool or something.
Another option would be to set up mining hardware in a place like China with low cost electricity. However, this would take time, money and serious effort - if you cash out ether to fund it, you likely crash the price, and if you succeed in fighting the hard fork, the split in the community would likely destroy the trust in Ethereum and your funds go poof.
Assuming contracts can identify the coinbase address of past blocks, then that would be relatively straightforward.
But this may not be up to the miners alone. Perhaps even more important is what for the major exchanges choose to run, since they're needed to convert Ether back into BTC/fiat currency. If a major exchange makes a public announcement committing to either the soft or hardfork, then that will sway a great many miners.
What if they had used a language without the possibility of recursion and without loops? I'm being serious. Languages that disallow certain types of recursion, and disallow loops exist. You'd think they would've used something that actually allows for total functions that are guaranteed to terminate in a certain way, instead of a JavaScript clone...
How did this madness start? I don't want law to be turing complete. Especially programatic law. Why are people so nonchalant about this? This is not sane design. You want totality and termination proofs. At least that's what I would look for in any programatic system of law.
This debacle seems like the most obvious possible outcome for any system combining the concepts "Turing-completeness" and "cryptocurrency blockchain". What baffles me most about the whole mess is that any of it caught anyone by surprise. I guess I had vaguely (naively?) assumed that the people building Ethereum and TheDAO must have come up with some clever solution for this sort of problem, but so far I haven't heard of one.
Its too bad, I really thought Vitalik was the Chosen One, but I think he reacted incorrectly here by panicking and showing concern.
If I had been him I would have let DAO fail without even discussing any fork. Be as emotionless about it as the code itself. Admit mistakes were made, somebody (DAO investors) will lose some money in the short term but stay true to the principles of Ethereum.
PLUS even after all this drama, $ETH has a market cap of ~$1B as well as independence (fingers crossed) from government intervention making it an alternative to Fiat currency, as well as a much better block rate than BTC lending itself to mining on consumer-grade GPU's for the moment at least. I'm looking at litecoin LTC as my next crypto-bubble investment as well.
There's still lots of good to be said about Ethereum. DAO is toast, long live DAO2! Ethereum will come out stronger long term.
Surely an issue here irrespective of technology flaws or not is the economic impact on the time taken to write smart contracts.
If it now takes substantially more dev time to write a smart contract that is "secure" (ie by spending lots and lots of time testing for vulnerabilities) this will invariably come at a cost.
So while the theory of smart contracts is brilliant this recent hack might go down in history as a case study as to why writing contracts is too expensive to do in all but the top 1% of situations.
I wonder if a language like Haskell with a strong type system and strict typing could help. If you were able to express exchange of currency with the type system.
It's now clear that Ethereum's contract system has major security vulnerabilities. This is a killer flaw for something which exists only to secure transactions between mutually mistrustful parties. Maybe someone else will do this again, better. Etherium itself probably is doomed.
There are also hard questions to ask the people involved. The same people seem to be behind Etherium, the DAO, and the programmable door-lock startup which the DAO was supposed to fund. This is suspicious. This might be an inside job. At least three times in the Bitcoin world, some Bitcoin exchange claimed they lost money due to a "hack", but in the end it turned out to be an inside job.
I wrote this originally in response to a post by cyphar (https://news.ycombinator.com/reply?id=11942889), but I'd really love a response from anyone with more knowledge or thoughts on how the law might interpret this situation in relation to already existing "virtual legal systems". cyphar wrote:
"It was definitely fraud. Either it was a contract, in which case "taking $50 million without anyone's consent" doesn't pass the officious bystander test. Otherwise it wasn't a contract, so the default is still fraud (though in that case, the DAO would be the thing being defrauded rather than the investors)."
I'd like significantly more details on your legal theory for how this was "definitely fraud" or how "the default is fraud" if there was no legal contract, the split executor was a direct party to the agreement, and the terms of the agreement were followed. "$50 million" was not taken, 3.6 million or so "ether" was split out from the original smart contract/account, which may or may not end up having some dollar value.
In at least two previous threads [1, 2], comparisons were made to the MMOG EVE Online (developed by CCP Games), and I think the analogy raises some interesting questions. EVE is a self-contained artificial system that, so long the system framework itself is not exploited, is ruled entirely by code. It has a digital currency (ISK) that has an official conversion rate from real world fiat currency to ISK, and an unofficial ToS breaking (but non-criminal AFAIK) conversion rate from ISK back to fiat. CCP has nothing to do with this exchange, but exchanges for ether to other currencies are also 3rd party. Virtual items as well as ISK itself thus have calculable value, both within the system, in terms of time/rarity, and in terms of nation-state issued money. There are person-actor driven "contracts" of various sorts, and people driven markets. There is fraud, piracy, and pure chaotic destruction as well, and that's considered entirely within the system framework so long as the overall code rules of the world are not violated.
Given that, what exactly is the legal difference between the DAO and EVE Online? In EVE, if Alice attacks Bob, or infiltrates his organization, and steals/destroys a few hundred billion in ISK (equivalent to a few thousand dollars at current exchange rate), or sets up a fraudulent bank/scheme that makes off with hundreds of billions or trillions (this has actually happened), do you think Bob should be able to sue in a real world court of law? The essence of the situation looks similar/identical to me: that the parties are operating under a non-contract non-legal agreement to be governed within the a specific set of world rules, and that therefore any interactions within those world rules, however angry they might get about it on a personal level and whatever colloquial English they might use to describe it, creates no legal standing of any sort outside. If EVE client/server were hacked (the world rules distorted) it'd be an issue (though still not necessarily a legal one), just as if the Ethereum VM was hacked it'd be an issue, but if those were operating entirely as they should be then what's the basis of legal complaint? What's the generalized objective basis for court involvement in people agreeing to mess around with made up numbers on computers, even if other people decide to try to exchange those numbers for money?
Legally speaking, CCP goes out of its way to emphasize that isk are play tokens money with no cash value, and losing it all is part of the game. TheDAO/Ethereum supports exchanging ether for money. And anyone who lies about contract (beyond smiling and saying "here the contract code, sign it if you want" is commiting a fraud
>Legally speaking, CCP goes out of its way to emphasize that isk are play tokens money with no cash value
CCP officially supports converting money to ISK, and there are 3rd party exchanges for ISK to money. My understanding was that TheDAO ran purely on ether, and that any exchanges for money (be it fiat or another digital currency) were also happening purely 3rd party. Does an official line on "don't go the other way" make a material difference? If CCP merely took no stance on it at all, involved in no way but not working to ban anyone doing it, would that change anything? How "seriously" do they have to police it? Is there any case law on this?
>And anyone who lies about contract (beyond smiling and saying "here the contract code, sign it if you want" is commiting a fraud
Can you clarify your point here, and what you were referring to?
1. (and again): How is there any legal contract here, and if there isn't what's the 'fraud' legally (not a colloquial "fraud" with no legal impact)? Are you arguing that people should not be allowed to have non-legally binding (and thus non-contractual) agreements on shifting around "value" based on coded rules?
2. In the case of TheDAO, there were no lies, TheDAO stated clearly and repeatedly that the definitive governing authority was the smart contract itself, and TheDAO organization itself was not (or at least, publicly claims it was not) involved in the controversial smart contract execution. Instead it was at least one of the independent parties to the agreement. So if you were referring to TheDAO I'm confused.
3. In the case of EVE, are you arguing that ISK is different and therefore fraud is legally ok? Or are you arguing that it's still legally fraud?
Fiy, i recently came upon this company http://m.imgur.com/Hv9n7fk,55JgdgK that wants to sell ETH to Chinese. I checked the company registry, and found out that the guy has registered a proprietorship back in 2013.
Jeremy Clarkson published his bank account details in his column to back up his assertion that you can send money to a bank account but not withdraw any. However apparently anybody can set up an automatic payment from any account to any other account...
This exploit wasn't legal either. It was blatantly fraud. I've asked a lawyer for their opinion and it was a very simple question to answer. Contracts are never entirely literal and usually there are implied clauses in contracts. There is a very simple test called the "officious bystander": if there had been a neutral bystander who had asked "should we allow anyone to take $50 million dollars without our consent" then unless both parties would've said "of course!" then it isn't considered to be a clause of the contract and it is just simply fraud. The developers of theDAO wouldn't have said "of course" so it's fraud.
So, you are trying to be a great libertarian by doing without the courts of law and the state but then, when everything goes wrong with your money, you call for the opinion of the courts of law and for the state to enforce that opinion.
Right I would tend to agree. They really went out of their way though to say that the "code is the contract nothing else matters" I think that is where some of the doubt comes in.
Right before the theft they would have said "off course", so sure their code was perfect... They made it abundantly clear the truth was in the code, and that men justice was an obsolete concept.
It's effectively legal because a lot of financial fraud is not pursued.
For example, people from different countries scamming old people out of $1000 for Prince Abu to free his millions.
That being said, I can understand why you think something being legally exploitable is something new. Just like a loophole in a contract is a loophole in a contract.
In the case of smart contracts, there is no recourse unless built in to the contract. This is by design.
All that's going to happen is people will start writing smaller, more testable, less damaging contracts. This regime is different from legal contracts because many lawyers specifically write contracts to create problems later. In this new world, good contract writers will be gods.
So if you're a good software engineer, there is potentially a huge market about to open up for you.
> It's effectively legal because a lot of financial fraud is not pursued.
That's not what "legal" means. Just like killing people without leaving traces to find you is not "effectively legal". It may simply be not worth pursuing because of gain/effort trade off.
Was the hack legal? A system letting you in if you poke it just right doesn't mean you are legally allowed in. I fail to see how a bug in banking software would be any different to the bug in the DAO.
The terms of The DAO Creation are set forth in the smart contract code existing on the Ethereum blockchain at 0xbb9bc244d798123fde783fcc1c72d3bb8c189413. Nothing in this explanation of terms or in any other document or communication may modify or add any additional obligations or guarantees beyond those set forth in The DAO’s code. Any and all explanatory terms or descriptions are merely offered for educational purposes and do not supercede or modify the express terms of The DAO’s code set forth on the blockchain; to the extent you believe there to be any conflict or discrepancy between the descriptions offered here and the functionality of The DAO’s code at 0xbb9bc244d798123fde783fcc1c72d3bb8c189413, The DAO’s code controls and sets forth all terms of The DAO Creation.
Basically, the code is the only authentic version of the contract. The attacker entered this contract and used its functionality as was programmed in the blockchain, he didn't modify a bit of the code. So it seems pretty legal.
Yes, this would be considered fraud in the US legal system, but that's not the point.
* If you have to involve the legal system then the project has failed because the whole point was to have a contract enforcement mechanism which doesn't need a court system.
* If a legal system can override the smart contract then there's no point to even having one since the ultimate authority still resides with the state.
> Yes, this would be considered fraud in the US legal system, but that's not the point.
It is the point though. It is the only point that will matter. Since the writers of the software are US citizens, it's most likely that they will get sued if the transaction is not aborted. Any scenario where the money is not returned to investors will result in the investors suing people -- no matter how much conviction people have that the DAO should be outside of the courts.
> * If you have to involve the legal system then the project has failed because the whole point was to have a contract enforcement mechanism which doesn't need a court system.
$50 million is missing, and people feel wronged as a result. I wouldn't call it a "failure of the project" that it is accountable to the law. Nobody is above the law, not even programmers that write software which governs itself.
> * If a legal system can override the smart contract then there's no point to even having one since the ultimate authority still resides with the state.
Again, nothing and nobody is above the law. You'd have to overrule the Magna Carta if you wanted to change that. And that's just not going to happen.
>$50 million is missing, and people feel wronged as a result.
So what is the plan going forward - if either party in a "smart contract" feels disadvantaged by the outcome - they go running to the law and outside jurisdictions for remedy? Isn't avoiding all that overhead the point of have a "smart contract" in the first place?
It's an interesting concept and I'd like to see the project survive (from a technology standpoint; I not risking any cash with it)... maybe it is good they did a faceplant 6 weeks in and can start answering some very hard questions that have come up.
The banks pretty much state that their software is an approximate implementation of the contract not the real contract itself. They specify that the real contract is what their lawyers drew up as interpreted by a human judge considering hundreds of years of legal case law.
The DAO basically said screw the lawyers and case law and precedent bullshit, the contract is nothing more or less than the results of running this program on the Ethereum VM.
As the program executed a way to transfer 10s of millions of dollars and they specifically stated that the program was the contract, by The DAO no contract violation occurred, hence no hack.
Because the point (as I understand it) of this whole experiment is that they were trying to create an altcoin that used strict contracts as the basis for transactions (with no human intervention). Essentially the code is the contract, so code behavior is necessarily abiding by its contract and anything done with that code is legitimate.
No, it was fraud. I asked a lawyer, and the stealing of $50 million would not be considered a clause of the contract (it doesn't pass the officious bystander test). As much as programmers might try to remove lawyers and courts from our lives, they are vital to actually doing things with other people where you might have a difference of opinion on what a particular agreement means.
How is not being above the law a failure of a project? If the goal of the project was to be above the law and be accountable to no-one, then the project was doomed from day one. Then again, I never bought the concept of the DAO (lawyers are incredibly important people who are undervalued in our society).
That was the goal of the project. Quote www.ethereum.org: "One of the many advantages of having a robot run your organization is that it is immune to any outside influence as it’s guaranteed to execute only what it was programmed to."
"Ethereum is a decentralized platform that runs smart contracts: applications that run exactly as programmed without any possibility of downtime, censorship, fraud or third party interference."
First of all, the "officious bystander" test is from English law, not US law.
Second, while there are similar tests in other countries' legal systems, it's not that clear cut whether this would be considered such a case or not -- a single lawyer's opinion aside.
> First of all, the "officious bystander" test is from English law, not US law.
Yeah, sorry. But as you say there are similar tests in other countries.
> it's not that clear cut whether this would be considered such a case or not
Whether it would be considered a contract, or what are you referring to? Either way, Etherium and/or the authors of the DAO will get sued, and the investors will win the suit. If you think there's a scenario where someone walks away with $50 million and nobody goes to jail as a result, I'm sorry to say that you're delusional.
And if Etherium hard forks the blockchain, then people have lost faith in the system. So IMO this won't end well for Etherium in either case.
>If you think there's a scenario where someone walks away with $50 million and nobody goes to jail as a result, I'm sorry to say that you're delusional.
Maybe you should read up on financial fraud, white collar crime and Wall Street?
As other comments say, legality and hard failure are big differentiators here, and in fact the specific language you used invokes a really key point. Emphasis added:
>You think banks aren't hacked?
There has been a lot of general description of the individual or group that performed the splitting as an "attacker" or "hacker", but the very nature of the system in question subverts the conceptual foundation of "attacking". To be an "attack" rather then a legitimate execution of an agreement, the action would have to be "illegitimate", but when legitimacy is explicitly defined by the code itself, then how can any action allowed by the code be illegitimate? It'd be a different issue entirely if the underlying VM or a system had been exploited, but merely doing as the code allowed when the code is made the agreement's authority?
Also, I've been using "agreement" here too rather then "contract" because, despite the label of "smart contract" Etherium has adopted I think there's a basic legal question about whether legally they're "contracts" at all. A contract is a subset of the space of agreements; all contracts are agreements, but not all agreements are necessarily contracts. There are many factors in determining validity of contracts and a huge body of contract law that has already been discussed a great deal, but all that depends on there being a contract at all, and for that there needs to be an agreement where the parties intend to be bound by the law (of whatever jurisdiction whose enforcement power they wish to invoke). There are many agreements where there is no intention to have legal enforceability, and in that case the courts have nothing whatsoever to say on the matter. Contract law never even enters the picture.
The DAO, and Etherium in general, have made a big deal specifically about not invoking the courts. That was supposed to be part of the entire point of smart "contracts", that they'd have nothing at all to do with any common legal system and be self-contained in and of themselves. In turn though that could mean that any smart contract that declares itself fully self-definitional is in turn not a contract period, so there cannot be an "attacker" in the legal sense.
Bank hacks in contrast aren't much different in concept from bank heists of any other kind. They are able to invoke real world power in response, and have multiple levels of fallbacks and insurance for their customers. It's by design a much softer fail, multiple level system with an expectation of occasional failure built-in and a strong human element. This adds expense and inefficiency, but provides benefits to imperfect human societies too. It came out of ages of real world experience and testing after all.
It was definitely fraud. Either it was a contract, in which case "taking $50 million without anyone's consent" doesn't pass the officious bystander test. Otherwise it wasn't a contract, so the default is still fraud (though in that case, the DAO would be the thing being defrauded rather than the investors).
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 forwards a small amount of gas. The recipient can write to the log but that's about it. TheDAO used .value() which forwards all the available gas.
If you do use .value(), then you can do it safely by doing it only once per method, as the very last step, and only using it in top-level methods. Then any sort of reentrant callback will find any required state changes already done. E.g. subtract from the user's balance, send the funds, and if the send fails then throw. The recipient can call back but the balance is already decremented. Using a mutex is another option. I've tested all this and it works.
There are a lot of reasons Ethereum is designed this way. The most common reason for a contract to run code when receiving funds is to prevent users from accidentally losing their money. E.g. in any contract that holds ether and maintains a ledger with balances for multiple users, if anyone sends ether to the contract address, they'll lose it, unless the contract either throws an exception or automatically adds to the user's balance on its ledger.
User addresses and contract addresses are interchangeable, because it lets you do things like use a multisig timelocked vault to receive funds and anything can send to it just as if it were a regular user account.
All that said, the devs are working on improvements too.