List of the top smart contract vulnerabilities
dasp.co
dasp.co
https://github.com/paritytech/parity/pull/6102/files#diff-8e...
A lot of people think "smart contracts" are inherently insecure. I personally believe that most of the "hacks" were very preventable, if those who had written the code slowed down to think about what they were doing.
This doesn’t help us prevent the mistake in the future, though. You can’t prevent bugs and vulnerabilities in code by just mandating that everyone think more before acting.
This is why we have a rule during our learning reviews at work following an incident that the action item can’t be, “be more careful next time.” That is not an action item, that is magical thinking.
We have a saying at my work - “plan for a world where we are just as stupid tomorrow as we are today”
This is only true for a very narrow view of what a "mistake" is. Classical tragedy is more inclined to the view that in some situations, there will be at least one mistake somewhere no matter what choices people make.
In a more contemporary source, there's an episode of Friends in which the backstory is that, years ago, Phoebe married a gay ice dancer so that he could get a green card, and also because she was secretly in love with him. He comes back to ask for a divorce because he's learned that he isn't gay after all and he's fallen in love with another girl.
This is painful for Phoebe, and she asks "Do you think, if you'd realized you weren't gay earlier, that we could have..." "Never mind, I don't think there's any answer you could give that would make me feel better."
A lot of "hacks" are preventable in hindsight though. I think the real issue is that we are just beginning to secure smart contracts and its more about the process than the person who made a mistake.
The tooling for Solidity is alright but most of the EVM and the languages associated with it are in their infancy. Formal Verification might be a solution here but we also have to consider the developer ergonomics of writing secure smart contract code.
When applied to programming, a first step towards that could be as simple as using a safer language, where it's more difficult to shoot oneself in the foot, and where all sorts of errors are prevented by default.
Should also require visibility to be declared (right now just compiler warnings happen).
I am one of the tool's authors. We went on to found ChainSecurity (https://chainsecurity.com) in order to deepen our research and understanding of smart contract security. Feel free to ask any questions about securify or ChainSecurity.
My experience with formal verification is that the further a language is away from being a pure functional language with easy to check termination, the more difficult you make life for yourself. You really want a smart contract language that was specifically created to be easy to formally verify rather than trying to tack on formal verification later.
it's a bit opaque what lines of code you are warning of
I don't own any crypto assets myself, but I think that using a non-turing-complete scripting language for the bitcoin blockchain was a wise decision rather than a lack of vision.
Since we are trying to analyze particular programs, you aren't going to be limited by the halting problem.
If only a subset of all programs can be completely analyzed as particular programs, what are the boundaries of that set?
A very crude explanation for the proof is something like this:
Imagine you design a program that takes another program as input and tells you if it halts.
Now, imagine you create another program, and all it does is call your first program, passing itself as the argument. Then, it does the opposite of whatever the first program predicts that it will do; if your 'halting detection program' says this new program will halt, the program instead loops forever. If your 'halting detection program' says this new program will loop forever, instead it halts.
So, in short, the idea is that you can't create a program IN ADVANCE that can't be tricked by a future program that knows about the halting detection program you are using.
So yes, you CAN analyze any program, but not by using a single algorithm.
A fun story using this idea is in Godel, Escher, Bach: https://genius.com/Douglas-hofstadter-contracrostipunctus-an...
Perhaps you're saying that it's possible to analyze any particular program for known exploits once they've been discovered?
Or: the set of all finite Brainfuck programs that don't contain a `[` or `]` instruction. Those also halt.
Also, see Idris: https://www.idris-lang.org/. It's a language that has dependent types and a totality checker.
A dependent type is a value which depends on another value. For example, the length of an array depends on how many elements there are in the array.
A totality checker means that you must prove that a program that you write halts; otherwise, it fails to compile.
In Idris, if you ever write the equivalent of reduce recursively, you must prove that the recursion will terminate. This is done by noting that the length of an array is dependent on how many elements are in the array, noting that if an array has zero length then reduce will terminate, and noting that every time reduce is called with a non-zero array length it returns reduce called with that array length decremented by one. Then, since repeatedly subtracting one from a positive number eventually reaches zero (at which point the recursion halts) you're guaranteed that your reduce function halts.
EDIT: I guess you are right in the strict sense that languages like Idris aren't Turing complete. But they still can do a huge number of computable and useful things (and most of the things you'd want other languages to do), so I feel like "Turing complete" is mostly a semantic argument here.
Perhaps there remains some unexplored region in the limited yet flexible yet verifiable space of languages that was until now uninteresting.
The halting problem doesn't prevent playing whack-a-mole against previous exploits, but it ensures that proving more exploits do not exist is impossible. That's why I think a turing-complete language for smart contracts is a poor choice.
exit
while 1: pass
- It's not such a large amount that it's a systemic risk.
- The hack was arguably enabled by negligence; the contract was changed after its last security audit, hacked, changed again and still didn't get a new security audit, and only after that the funds were frozen. Strong incentives to be more careful are probably good. Forking every time somebody's negligent could get messy.
- The DAO hack involve an attack that was new to most people in the community, and even the tutorial code on ethereum.org was vulnerable to similar hacks. These hacks were more in the nature of simple oversights, enabled by overly complicated code. Good auditors would probably have found them.
- The largest loss of funds was to the entity that made the contract (or a related entity anyway). That entity also said they had plenty of other money for their project.
- Most of the remaining losses were to ICOs, who should have gotten competent advice to avoid this contract (given the first hack and lack of audit), and who've demonstrated fundraising ability so could conceivably get bailed out by their own investors.
- Despite heavy criticism from certain quarters about Ethereum's supposed lack of immutability (after the DAO hack), immutability actually is a strong community value. Some people supported the DAO fix on the grounds that it was early days, but feel that the network is more mature now.
2. #9 has nothing to do with "off-chain issues". Off chain has very clear context and refers to layer 2 solutions for scaling. No need to call a website bug "off chain issue".