5 ms·

Is formal verification of contracts feasible? Is anyone working on it? Also, here's a possibly crazy idea: could one create bug bounties for algorithms (or eve

Is formal verification of contracts feasible? Is anyone working on it? Also, here's a possibly crazy idea: could one create bug bounties for algorithms (or even arbitrary software) on the Ethereum blockchain by writing the algorithm into a contract such that if you somehow break it you receive the bounty? An example of this would be the massive implicit bounty currently placed on the crypto algorithms (SHA256, ECDSA/Secp256k1, etc) underpinning cryptocurrencies (of course, if those were broken the value of the cryptocurrency would plummet instantly)

HaseebQ 9y ago
See: https://www.youtube.com/watch?v=voyespPGQZI https://www.youtube.com/watch?v=voyespPGQZI (Directions in Smart Contract Research A Selection - Philip Daian)
- Emilie656 9y ago
  Google is <-paying 97$ per hour! Work for few hours and have longer with friends & family! On tuesday I got a great new Land Rover Range Rover from having earned $872 this last four weeks. Its the most-financialy rewarding I've had. It sounds unbelievable but you wont forgive yourself if you don’t check it... ------------>http://ow.ly/iBXm30dNtIZ http://ow.ly/iBXm30dNtIZ
mbrock 9y ago
Yoichi Hirai and others are working on completing proof assistant support for EVM, meaning you will be able to prove program properties using logical pre/post-conditions with machine checked proofs. There are already useful tools for symbolic execution, and I have a hunch that this kind of verification will be important along with model checking.
- chalst 9y ago
  The specification of EVM in HOL exists already [1] and can be used to prove correctness of EVM code already. EVM is pretty low-level, though; the same can't be done for Solidity code. Yoichi has a page that outlines his thinking about what Ethereum's formal verification needs are [2]. What I would like to see is a verified high-level smart contract language layered on top of the Ethereum stack, allowing non-logicians to put together contracts that mean what they think they mean. See [3]. [1]: https://github.com/pirapira/eth-isabelle https://github.com/pirapira/eth-isabelle [2]: https://github.com/pirapira/ethereum-formal-verification-overview https://github.com/pirapira/ethereum-formal-verification-ove... [3]: http://lambda-the-ultimate.org/node/5003#comment-94645 http://lambda-the-ultimate.org/node/5003#comment-94645
deleted 9y ago
[deleted]
JetSpiegel 9y ago
There's already an implicit bug bounty. Whoever found this bug got a bounty of millions. Much better than the presence that tech companies pay.
- tlrobinson 9y ago
  Yes, but I'm suggesting designing explicit bug bounties. The point of a bug bounty is to offer a smaller sum of money than would be lost if the vulnerability were exploited maliciously. Cryptocurrencies are serving as bug bounties for their crypto primitives, but that only benefits other users of those primitives.

HaseebQ 9y ago

See: https://www.youtube.com/watch?v=voyespPGQZI https://www.youtube.com/watch?v=voyespPGQZI (Directions in Smart Contract Research A Selection - Philip Daian)

Emilie656 9y ago
Google is <-paying 97$ per hour! Work for few hours and have longer with friends & family! On tuesday I got a great new Land Rover Range Rover from having earned $872 this last four weeks. Its the most-financialy rewarding I've had. It sounds unbelievable but you wont forgive yourself if you don’t check it... ------------>http://ow.ly/iBXm30dNtIZ http://ow.ly/iBXm30dNtIZ

mbrock 9y ago

Yoichi Hirai and others are working on completing proof assistant support for EVM, meaning you will be able to prove program properties using logical pre/post-conditions with machine checked proofs. There are already useful tools for symbolic execution, and I have a hunch that this kind of verification will be important along with model checking.

chalst 9y ago
The specification of EVM in HOL exists already [1] and can be used to prove correctness of EVM code already. EVM is pretty low-level, though; the same can't be done for Solidity code. Yoichi has a page that outlines his thinking about what Ethereum's formal verification needs are [2]. What I would like to see is a verified high-level smart contract language layered on top of the Ethereum stack, allowing non-logicians to put together contracts that mean what they think they mean. See [3]. [1]: https://github.com/pirapira/eth-isabelle https://github.com/pirapira/eth-isabelle [2]: https://github.com/pirapira/ethereum-formal-verification-overview https://github.com/pirapira/ethereum-formal-verification-ove... [3]: http://lambda-the-ultimate.org/node/5003#comment-94645 http://lambda-the-ultimate.org/node/5003#comment-94645

deleted 9y ago

[deleted]

JetSpiegel 9y ago

There's already an implicit bug bounty. Whoever found this bug got a bounty of millions. Much better than the presence that tech companies pay.

tlrobinson 9y ago
Yes, but I'm suggesting designing explicit bug bounties. The point of a bug bounty is to offer a smaller sum of money than would be lost if the vulnerability were exploited maliciously. Cryptocurrencies are serving as bug bounties for their crypto primitives, but that only benefits other users of those primitives.