The second morning of Devcon2 provided a strong focus on security in the Ethereum ecosystem. Topics included formal verification of contracts, DApp-specific attack vectors, smart contract development best practices and the future of security in the ecosystem.
Presenters were selected from a broad range of backgrounds such as academics and system engineering providing a well-balanced and comprehensive consideration of security in the context of smart contract systems and distributed applications.
The simplicity of the EVM provides fertile ground for the advancement of formal verification techniques. Static analysis techniques which provide visualization and formal verification are becoming more widely available in the form of automated tools. The primary benefit of static analysis is complexity reduction, aiding the alignment of human mental models with high-level language and bytecode abstraction models.
Dynamic analysis techniques provide, among other benefits, runtime attack vector analysis. However, dynamic analysis coverage is generally incomplete. This incompleteness is due to the fact that at runtime it is easy to verify the presence of desired behavior, but difficult to prove the absence of undesired behaviors. An absence of standardized unit testing patterns was identified as a current secure development pain point.
Smart contract best practices were provided, and common agreement is that most secure programming practices include:
- check invariants and use escape hatches & emergency brakes
- isolation, separation and defense in depth
- use send() instead of call.value() and keep fallback functions simple
- favor 'pull' payment scenarios over 'push' payments
- identify untrusted contracts/actors and assume they are malicious
Smart contract deployment best practices include:
- prepare for failure
- rollout carefully (e.g., in phases associated with increasing risk)
- have an actionable plan to transfer data and funds in case of failure or breach
Smart contract ecosystem best practices include:
- have a small number of diverse and well-understood languages
- developers must demand a level of rigor appropriate for the funds at risk
- EVM improvements, such as replacing the call stack limit with gas-oriented limit
Panel: Smart Contract Security in Ethereum
Vitalik Buterin, Raine Revere, and Martin Swende
Ethereum launched with several smart contract languages, but the community has mostly converged on Solidity. Solidity’s dominance has been helpful in many ways. Spreading knowledge about insecure contract patterns is much easier when everyone’s speaking the same language.
Some EVM improvements could be made to make it easier to write secure contracts. For instance, if sending funds and sending messages between contracts used different opcodes, it’d be much easier to avoid unintentional reentrancy. However, there’s much more work to do at layers above the EVM than there is to do on the EVM itself. Work is being done on several smart contract languages that compile to EVM bytecode. As it has on the web, a diversity of languages can help progress. When developers learn through experience which language features minimize the cognitive load of writing secure contracts, those features will spread to more languages and developers will move to languages that have them. There will be multiple sources of experimentation and evolution that lead us to an ecosystem where it’s simpler to write secure contracts.
Smart Contract Security Best Practices
Joseph Chow
Joseph Chow delivered a great live version of the Smart Contract Best Practices document you can find at https://github.com/ConsenSys/smart-contract-best-practices. If you prefer video or audio to text, make sure to watch this video. The Smart Contract Best Practices document is a community collaboration, so if you have suggestions, pull requests are welcome!
Visualizing Security
Raine Revere
Developers are familiar with the concept of “code smells:” patterns in code that indicate likely problems. These patterns are great targets for static analysis. Raine built a tool called solgraph that when combined with solidity-parser, can output a visual graph of which parts of a contract need the most attention for security risks.
Beyond this kind of static analysis, it’d be useful to have dynamic analysis as well that depends on the state of the contract. To develop a dynanic analysis ecosystem, we need to start developing standardized unit testing patterns and standardized access control modifiers.
Ethereum Security Overview
Martin Swende
Take steps to reduce both the likelihood and impact of attacks, which can range from zero day exploits to game theoretical attacks. For instance, small hot wallets limit the impact of an attack on hot wallet assets. Maintaining a cold wallet limits the likelihood of a successful attack on those assets. Remember that dapps run in browsers, which have a huge attack surface, so take steps to minimize attacks, like not surfing the web with your dapp browser and hosting assets on trusted servers, not CDNs. The EVM environment adds new scenarios to worry about in application code, like chain reorganizations. Developers must truly understand the EVM, and the Python implementation is a very readable codebase to get started. There are several ongoing EIPs to address security issues in smart contracts, and these are open discussions for anyone to participate in.
Formal Verification for Solidity
Christian Reitwiessner and Yoichi Hirai
Writing code correctly is hard. It’s hard to even define what correct is. Correct is when the program does what the programmer expected, but it’s hard to test the infinite set of undesired behaviors. Formal verification allows us to proof correctness on all inputs—it can even let developers ask questions about the program’s execution. Why3 annotates Solidity with pre- and post-conditions. Future work will model the msg variable, multi-contract conditions and multi-transaction conditions for use in proofs.
Imandra Contracts: Formal Verification for Ethereum
Grant Passmore
Imandra formalizes the EVM inside an Ocaml-based formal verification language. This allows companies to prove which risks are present in their contracts so they can take steps to hedge that risk. These proofs help to translate systems between platforms, like Ethereum and Corda. Imandra can generate visual representations of the space of possible behaviors in a contract and drill down to which constraints apply in each category.