From what I've read about Ethereum's contract language, it doesn't make itself easy to statically verify properties you want to check so I don't see how problems like this are going to go away until another language is used.
The parity wallet uses a "shared library" in which the actual logic is implemented. All individual wallets have their own data storages and coin balances, but contain just a little bit of logic code that redirects calls to this shared codebase.
This shared library itself is also just a contract, except that it's intended to be called internally by other contracts (the different wallets). Though it typically doesn't happen, it can be called directly by humans. This is what the makers of this "shared library" apparently forgot to consider, until somebody called the "initialization function" of the shared library directly. By doing this, the shared library initialized itself as if it was one of the individual wallets that normally call the library. It therefore used its own (previously unused) data store, in which it correctly entered the caller of the init function as owner.
This wasn't of use for anything, as there are no ethers at all on the shared library, so the owner could not steal any funds. But being the owner, he was able to trigger the kill switch! Since this particular "multisig wallet" was actually not a wallet, but the shared library, killing it not only killed the (empty) wallet, but also the core functionality of all the real wallets that contain real money out there! And of course that functionality is mandatory to work with the funds of these wallets. Without it, the money cannot be moved anywhere.
Now comes the fun part: suiciding a contract normally transfers all ethers on that contract to the caller of the suicide function. Knowing this, you could expect that the individual wallet owners could just as easily suicide their now "brain-dead" multisig wallets as well, thereby recovering their funds...but that doesn't work, as performing the suicide requires a call to the shared library to check whether the callers' signatures qualify the caller to perform that suicide ;-)
This sounds really similar to the big Ethereum wallet hack from earlier this year.
I would say there are many ways to look at this with regard of "what went wrong":
- You could say that it's a very, very bad idea to share ANY code between individual wallets which - from a functional standpoint - should not have any intersections between them whatsoever (except of using the same blockchain of course). Individual wallets are DESIGNED to fully isolate the contained tokens and state from each other, so why not also fully isolate their code by duplicating it? Is saving a bit of gas on wallet creation actually worth the additional complexity that comes with code sharing? Seems like someone took the "DRY" principle to a very unhealthy extreme here.
- Apparently the explicit construct of libraries described here (http://solidity.readthedocs.io/en/develop/contracts.html#lib...) is not very well-known in the Ethereum community. I did not know about it (someone here on HN pointed me to it), and while this is understandable considering that I have just a tiny stake in ETH and don't write Ethereum contracts for a living, the fact that Gavin Wood - co-creator of Ethereum - did apparently also not know about it (or for some reason decided not to use it for this library, which would be equally concerning, because if it's not usable for a textbook example like this, it must be seriously flawed) should cause a bit of head-shrugging. Because according to the docs, this construct delivers a crucial limitation with which this entire drama would have been impossible: libraries don't need their own state! So it's just consequential to not allow them to have any state (like an owner, or ETH funds), which apparently is exactly what the library construct does.
- Maybe this incident is just another bit of proof to the theory that the combination of immutability, handling of huge monetary values without any human oversight at all, and the idea of a Turing-complete language just don't mingle together very well. If you're not able to manually interfere in case stuff goes wrong in a way you didn't anticipate, you need to be able to basically anticipate absolutely all ways in which stuff can go wrong beforehand. A Turing-complete language seriously complicates doing this, possibly to an extent that kicks the entire concept beyond the realm of practicability. If this turns out to be true, the entire value proposition of Ethereum would be void right from the beginning.
My wife once left the car running and went to buy gum in a drug store, the car wasn't their when she got back. Shit happens I guess.
https://www.reddit.com/r/ethereum/comments/7bem7v/solidity_l...
What problems specific to Ethereum do you see? Formal verification has been applied to complex domains and large projects before.
Work on this has indeed been going on for decades, and its very limited adoption so far is a testament to its difficulty. Only a tiny fraction of the code in the domains you mention is formally verified, and I notice that banking and finance are not on your list. The answer to "why would how useful Ethereum is or could be make a difference?" is that if Ethereum becomes as useful and important as intended, the size and scope of the problem will be well beyond anything that has been achieved so far. Arguably, given the value at risk, it has already crossed that threshold by a wide margin.
There are, however, people working on it, such as at Cardano [1], which is an exciting development. Ultimately, I think it will be more successful than trying to fix Ethereum.
If you don't have experience writing formally-verified code, I suggest the F* tutorial [2].
Rather, formal verification is just one piece in the puzzle. The software responsible for contracts in Ethereum needs to be equally well and thoroughly developed as if it was sending people to the Moon in the 60s or to Mars in the current Decade.
It'll probably take blood, sweat, money and mistakes just like in many other disciplines but we'll get there.