3 ms·

The author mentions that turing complete contracts will have bugs in them eventually. While currently that happens, we do have formal verification methods in co

by TeeWEE 9y ago

The author mentions that turing complete contracts will have bugs in them eventually. While currently that happens, we do have formal verification methods in computer science. And thats exactly what people are trying to apply on Ethereum: Formally verified smart contracts. https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/ https://blog.ethereum.org/2016/06/19/thinking-smart-contract...

rrobukef 9y ago
It is just moving the goalposts. The formally verified contract is only as good as the assertions proven. Look at WPA2, it was formally verified against 'most' attacks.
- mannykannot 9y ago
  Just to be clear, this is an argument that even formal methods might not be sufficient to secure Ethereum (and certainly not if applied piecemeal), not an argument that it can be secured by other means.
  - rrobukef 9y ago
    Yes, i think a lot of the stupid bugs would be avoided. I don't think this was a stupid enough bug that formal methods would always catch.
mannykannot 9y ago
Formal methods have been under development for decades, yet their penetration into software development is miniscule. Hardly any professional developers know how to use them. Turning Ethereum and its contracts into a formally verified system would be the largest adoption of formal methods by several orders of magnitude. Ironically, the article you link to does not support your post: it also stresses the difficulties of applying formal methods, and claims instead that various interventions of the sort that have not been particularly successful in securing software generally will be sufficient to satisfy the particularly stringent requirements of a crypto-currency (of course, to say that Ethereum needs formal methods in order to be usable would be to admit that it is not close to being so, so that view will always be contested by the Ethereum foundation. At Cardano [1], however, they do seem to think formal methods will be part of their solution, though I am not sure to what extent.) This is all mostly moot, however, as the Ethereum we have now is demonstrably insecure by any measure. [1] https://www.cardanohub.org/en/home/ https://www.cardanohub.org/en/home/
- TeeWEE 9y ago
  Yeah true, it is used in some industries such as the space and flight industries, where you want to be sure your code is correct. However it comes with a range of problems, and often its not worth going into the effort of formally verifying a contract. But with ether, the costs quickly outweigh the ptential losses. I don't know if it will work, in theory it can, i just wanted to be possitive: I see a light at the end of the tunnel.

by TeeWEE 9y ago

rrobukef 9y ago

It is just moving the goalposts. The formally verified contract is only as good as the assertions proven. Look at WPA2, it was formally verified against 'most' attacks.

mannykannot 9y ago
Just to be clear, this is an argument that even formal methods might not be sufficient to secure Ethereum (and certainly not if applied piecemeal), not an argument that it can be secured by other means.
- rrobukef 9y ago
  Yes, i think a lot of the stupid bugs would be avoided. I don't think this was a stupid enough bug that formal methods would always catch.

mannykannot 9y ago

Formal methods have been under development for decades, yet their penetration into software development is miniscule. Hardly any professional developers know how to use them. Turning Ethereum and its contracts into a formally verified system would be the largest adoption of formal methods by several orders of magnitude. Ironically, the article you link to does not support your post: it also stresses the difficulties of applying formal methods, and claims instead that various interventions of the sort that have not been particularly successful in securing software generally will be sufficient to satisfy the particularly stringent requirements of a crypto-currency (of course, to say that Ethereum needs formal methods in order to be usable would be to admit that it is not close to being so, so that view will always be contested by the Ethereum foundation. At Cardano [1], however, they do seem to think formal methods will be part of their solution, though I am not sure to what extent.) This is all mostly moot, however, as the Ethereum we have now is demonstrably insecure by any measure. [1] https://www.cardanohub.org/en/home/ https://www.cardanohub.org/en/home/

TeeWEE 9y ago
Yeah true, it is used in some industries such as the space and flight industries, where you want to be sure your code is correct. However it comes with a range of problems, and often its not worth going into the effort of formally verifying a contract. But with ether, the costs quickly outweigh the ptential losses. I don't know if it will work, in theory it can, i just wanted to be possitive: I see a light at the end of the tunnel.