3 ms·
Please correct me if I'm wrong, but isn't it the nature of a turing machine (decentralized or not) to produce an endless series of "unforeseen" exploits?
by asynchrony 8y ago
Please correct me if I'm wrong, but isn't it the nature of a turing machine (decentralized or not) to produce an endless series of "unforeseen" exploits?
- piracy1 8y agoI find that an interesting thesis but I don't quite understand how it's true. Could you expand on that?
- asynchrony 8y agoBased on the halting problem, a provably complete analysis of the behavior of some (most?) programs in a turing-complete language is impossible. To put it another way, it is impossible to be sure that there isn't another vulnerability after you've patched the last one. 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.
- cortesoft 8y agoThe halting problem doesn't say that you can't do a complete analysis of a PARTICULAR program to see if it halts, it just says you can't have a general algorithm that would do this for ALL programs. Since we are trying to analyze particular programs, you aren't going to be limited by the halting problem.
- asynchrony 8y agoIf it's possible to do a complete analysis of any particular program, shouldn't it follow that it's possible to do a complete analysis of all programs? If only a subset of all programs can be completely analyzed as particular programs, what are the boundaries of that set?
- cortesoft 8y agoSo the halting problem isn't stating that there exists a program that you can't analyze to see if it stops, the problem states you can't create a single PROGRAM that will be able to analyze all other programs. 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-annotated https://genius.com/Douglas-hofstadter-contracrostipunctus-an...
- asynchrony 8y agoI'm familiar with the proof and the story. My point is that the claim that any particular program can be fully analyzed is equivalent to saying that all programs can be analyzed. Perhaps you're saying that it's possible to analyze any particular program for known exploits once they've been discovered?
- cortesoft 8y agoMy point is that the halting problem doesn’t prevent you from analyzing any particular program for exploits.
- asynchrony 8y agoI wasn't claiming that it is not possible to analyze a program to detect known exploits. Rather that it is extremely probable that another exploit will be found after the last one has been patched, and it is impossible to prove otherwise. 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.
- UncleMeat 8y agoThis is not true. There are sound static analyses. The problem is that they have oodles of false positives.
- tree_of_item 8y agoYes, but even if your language is total you have an analogue of the halting problem, where instead of analysis being undecidable it just takes an unrealistic amount of effort.
- asynchrony 8y agoMy understanding is more hand-wavy than formal, but would the combination of a total language and some limitation on the total number of instructions produce a provably predictable language?
- lmkg 8y agoLikely not. It takes only a very small number of instructions to implement an interpreter for a Turning-complete language, and then you can create arbitrary behavior by passing different input. The number of necessary instructions is shockingly small, if using something like Binary Lambda Calculus or Subtract-And-Branch-If-Negative.