Designing expressive distributed protocols that can gracefully withstand attacks and manipulation is not a trivial task. Even solving a relatively simple use case, Bitcoin’s success in providing currency free of central control was certainly cause for celebration. When dealing with more complex problems, like financial contracts and governance, we have to step up our game.
Whether one believes the attack on the DAO was a problem in the contract or a flaw in Ethereum’s smart contracting language Solidity itself, it certainly highlights the need for better tools to help with the analysis of contracts deployed in mission-critical situations. To have such tools, a candidate for a smart contracting language needs to have a much greater level of precision in its specification. In fact, it needs a mathematically precise specification, usually called a formal semantics, to provide tools to analyze contracts that are to serve as dependable, production-quality services.
Without a formal semantics, it is impossible to reason about the code and specify what it does or to utilize any formal verification method to assure that it complies with any specification. For all intents and purposes, the only specification of Solidity’s semantics is its compiler to byte code for the Ethereum virtual machine (EVM). This compiler has not been formally verified. Likewise, the virtual machine running the code has not been verified, and so it is next to impossible to say anything meaningful about what contracts in Solidity are supposed to do.
Ethereum’s less rigorous approach has been cause for concern from day one , casually dismissed because most of us were ecstatic even just with the idea of a contracting system completely independent of any central entity or friction caused by middle-men. As has been predicted, we’re now at a point where a naive implementation free of a formal semantics can’t […]
