Ask HN: Will smart contract security bring attention to formal verification?
3 comments
Formal verification is almost always too costly for most projects but it seems like a good match here given the financial risks are so high. From what I've seen though, cryptocurrencies seem to take off based on marketing + emotions first followed by technical merit.
The Ethereum project is really interesting for example and there are talks of applying formal verification to it, but it doesn't look like the language used for smart contracts there was designed to be easily applicable to formal verification. I'd like to see a cryptocoin developed from the ground up with formal verification in mind instead of it being an afterthought. Most coins have clients written in unsafe languages like C or C++ so I don't see this happening any time soon.
The Ethereum project is really interesting for example and there are talks of applying formal verification to it, but it doesn't look like the language used for smart contracts there was designed to be easily applicable to formal verification. I'd like to see a cryptocoin developed from the ground up with formal verification in mind instead of it being an afterthought. Most coins have clients written in unsafe languages like C or C++ so I don't see this happening any time soon.
Cardano could be a cryptocoin to look into due to their research first approach. TBH I didn't have a closer look into their whitepapers.
If researchers fuzz Ethereum smart contracts they will discover critical bugs in the Ethereum Virtual Machine, then decide formally verifying Solidity written contracts was a waste of their time. Of course these bugs will be patched but there will be a never ending river of bugs for researchers to find later just like there is in every other VM. Rewriting the VM, and using a language amenable to formal verification for the contract DSL, then releasing their own implementation would probably be a better use of their skills and resources instead of dressing up Solidity.
Imagine pwn2own had a $100k bounty on the EVM except you also have the added incentive of keeping all the ETH you can grab as well https://arstechnica.com/information-technology/2017/03/hack-...
Imagine pwn2own had a $100k bounty on the EVM except you also have the added incentive of keeping all the ETH you can grab as well https://arstechnica.com/information-technology/2017/03/hack-...
To the degree formal verification adds economic value to smart contracts, it will get attention. The attention is a side effect of the primary uses. To put it another way, many contracts are agreed without having been reviewed by both parties' lawyers and negotiated back and forth. Largely this is because the economics including calculated risks, the amounts exchanged, previously established trust, etc. don't meet a party's threshold for paying for legal services because the purpose of the contract is not "to hire a lawyer."
Perhaps analogously, the business uses of encrypted communications over the web has not led banks to invest in cryptographic testing. Banks tend to buy and rely on off the shelf products and when smart contracts are adopted, they are likely to behave similarly.
[Edit: where the opportunity may lie is at the nexus of the computer science and the legal profession: Paying legal council to formally verify a smart contract.]
Perhaps analogously, the business uses of encrypted communications over the web has not led banks to invest in cryptographic testing. Banks tend to buy and rely on off the shelf products and when smart contracts are adopted, they are likely to behave similarly.
[Edit: where the opportunity may lie is at the nexus of the computer science and the legal profession: Paying legal council to formally verify a smart contract.]
Acknowledged, that it really depends on how many people are willing to pay for verification services. Product developers may be encouraged economically or legally though. For example cryptocurrency exchanges may decide to list only Quantstamp-verified tokens. Quantstamp's CEO Richard Ma likes to compare his project to Verisign - being kind of a certificate authority for the blockchain.
caveat: My basis of experience is in the US.
I think it is possible that the primary forces which will shape the general use/non-use of formal verification methods for smart contracts will be legal not technical. The distance from widespread adoption of formal use of smart contracts and the current state of the world is approximated by the distance between the widespread availability of legal council and the scarcity of people skilled in formal verification. It is easy for an ordinary individual to enter into an ordinary contractual agreement because lawyers are ubiquitous. It is difficult/impossible for an ordinary individual to enter into a smart contract because qualified practitioners are rare. The growth of qualified smart contract practitioners may be rapid until the point where is is deemed legal practice and becomes regulated as such. And if I were to bet, I would bet that it will be deemed legal practice once it comes on the radar of the legal system.
I think it is possible that the primary forces which will shape the general use/non-use of formal verification methods for smart contracts will be legal not technical. The distance from widespread adoption of formal use of smart contracts and the current state of the world is approximated by the distance between the widespread availability of legal council and the scarcity of people skilled in formal verification. It is easy for an ordinary individual to enter into an ordinary contractual agreement because lawyers are ubiquitous. It is difficult/impossible for an ordinary individual to enter into a smart contract because qualified practitioners are rare. The growth of qualified smart contract practitioners may be rapid until the point where is is deemed legal practice and becomes regulated as such. And if I were to bet, I would bet that it will be deemed legal practice once it comes on the radar of the legal system.
Isn't this a beautiful opportunity to highlight the strengths of formal verification methods as a means to prevent such disasters from the outset?
The area is actively being researched for example at ETH Zürich [2]. The SF-based startup Quantstamp [3] are designing a system based on an Ethereum ERC20 token with the goal to automate and effectively decentralize smart contract verification and auditing. Think fuzzers as well as SAT+SMT solvers running on nodes in a decentralized network competing for rewards akin to proof of work based systems [4].
In the near future I can see the Quantstamp network develop into a leading platform for software verification services. Starting with Ethereum smart contracts, they plan to expand to other platforms like NEO, WAVES or ADA. Maybe the computational power of the verification network can be leveraged to verify more general purpose software as well? I'm excited to see what will come.
Is that a realistic outlook in your opinion?
[1] https://en.wikipedia.org/wiki/The_DAO_(organization)
[2] Securify, Formal Verification of Ethereum Smart Contracts, http://www.securify.ch/
[3] https://quantstamp.com/
[4] Quantstamp whitepaper, https://docsend.com/view/shcsmhe