The second day of Devcon3 was packed with security topics. It's going to take me some time to synthesize all that information, this post is a first attempt at trying to do that.
Many links to resources are missing, and I'm sure there are ideas that I'm not conveying clearly. Please comment if you have a useful link, or a correction I should make.
I've grouped the ideas into 3 themes, along with a few miscellaneous observations
- Tools
- Formal verification
- New languages
Although our tools have improved tremendously in the past year (ie. Truffle's debugger, and huge usability improvements to Remix), we still have a long, long way to go.
There were a couple very cool new tools relevant to security introduced this week:
In his talk, Martin Swende made the interesting observation that even when different EVM implementations agree on the state root hash, it's possible for there to be 'ephemeral disagreements' in the stack and memory, which could be manipulated to cause a consensus failure.
In order to address this, Geth and Parity have introduced a standard trace object, which can be outputted after after every EMV operation during the execution of a transaction.
This enabled him to create Retromix, which is an in terminal version of the Remix debugger, and is part of his EVM-Lab tools.
He also discussed the Ethereum Foundations work on fuzz testing using testeth, and LibFuzzer.
evmlab repo: https://github.com/holiman/evmlab Testeth repo: TBD LibFuzzer on ethereum repo: TBD Talk Recording: TBD
Manuel Araoz discussed Zeppelin OS, which promises a robust approach to upgrading contract logic on chain. It also comes with a new zeppelin_os command line tool, which I'm sure will be full of goodies.
Site: https://blog.zeppelinos.org/ Paper: https://zeppelinos.org/data/zeppelinOS_Whitepaper_Draft.pdf Talk Recording: TBD
We heard an update from Loi Luu about Oyente, as well as a newer entry from Securify. Both tools perform their analysis at the bytecode level, and are able to identify common classes of vulnerabilites such as re-entry.
Oyente IDE: https://oyente.melon.fund/ Oyente paper: https://eprint.iacr.org/2016/633.pdf Talk Recording: TBD
Security site: https://securify.ch/ Talk Recording: TBD
Hydra is an interesting project from the prolific Phil Daian (and his talented colleagues). , taking a 3 pronged approach to security:
- Formal verification and specification
- escape hatches
- bug bounties
Hydra introduces a concept called an exploit gap, a way for developers to turn crippling exploits into safe, decentralized bounty payments using a new form of fault tolerance called N-of-N Version Programming (NNVP) (not to be confused with N-Version Programming).
Repo: https://github.com/IC3Hydra/Hydra Website: https://thehydra.io/ Paper: https://thehydra.io/paper.pdf Slides: https://docs.google.com/presentation/d/1jqqBeQx2B7hoqM5_al4UvYerIYx5Se1AFGTuahQMu6M/edit Talk Recording: TBD
A lot of work and research effort is going into building new EVM languages which incorporate lessons learned from solidity. I especially love learning about these projects, because they give a new lens through which to view the EVM, and contract architecture in general. Even if you never deploy a contract written in anything but solidity, learning a new EVM language will make you a better smart contract developer.
I was fortunate to get a tutorial from David Knott, a primary contributor to the Viper compiler. The design of Viper places more constraints on developers than solidity. For instance, Viper doesn't support contract inheritance, and doesn't have modifiers, both of which are essential features in solidity. There are also plans for a rich typing mechanism which could ensure for example that a value is always derived from the same units (ie. price = wei/currency).
Repo: https://github.com/ethereum/viper Docs: http://viper.readthedocs.io/en/latest/
Bamboo is a functional programming language being designed by Dr. Yoichi, (formal verification engineer at the Ethereum foundation). It provides a rigorous method for applying state changes, while having the "sugarly syntax to trap solidity developers". Incidentally, Yoichi's dry humor is hilarious.
I'm excited to watch this project evolve.
Slides: https://yoichihirai.com/yoichi-bamboo.pdf Repo: https://github.com/pirapira/bamboo Talk Recording: TBD
Christian Reitwiessner's Babbage is a visual programming language which models smart contracts as machinery. Keeping with the trend of other languages, it's less expressive, and more constrained than solidity.
Medium post: https://medium.com/@chriseth/babbage-a-mechanical-smart-contract-language-5c8329ec5a0e Paper: https://chriseth.github.io/notes/articles/babbage/babbage.pdf Slides: https://chriseth.github.io/notes/talks/babbage_devcon3/#/7 Talk Recording: TBD
Although it may like the "shiny new" factor of the experimental languages above, Solidity continues to mature, becoming more battle hardened with each release.
Alex Beregszaszi introduced Julia, a new intermediate language to be used in the Solidity compiler. Julia promises to make the compiler more less complex and more maintainable. It could also help with auditing contract systems, and even adapting solidity to new VMs.
Christian Reitwiessner demonstrated the new SMTChecker, which can formally verify that certain error conditions (such as under/overflow, or invalid states) are unreachable.
He demonstrated with this code, though I haven't yet figured out how to access the SMTChecker feature.
https://gist.github.com/4e3658b0f59baa65e9dced2537eaf5c1
Slides: https://chriseth.github.io/notes/talks/solidity_update_devcon3/
Everett Hildenbrandt presented K-EVM, an implementation of the EVM, in the "K" language. K provides a formally defined set of semantics, enabling formal reasoning, and theorem proofs about programs. It also comes with a rich toolset for analysis, and has been used for formal verification in other languages including C.
This project will eventually give us new tools to ease the process of writing and proving specifications about programs written in high-level languages. Another team is extending K-EVM provide a formal verification of the Viper compiler!
Paper: https://github.com/kframework/evm-semantics
Yoichi has been hard at work on verifying Casper (the friendly finally gadget), his talk provided a great update on the evolution of the protocol, as well as outlining the assumptions which he is working on proving.
Slides: https://yoichihirai.com/yoichi-verifying-casper.pdf
Perhaps my favorite session of all was a panel reflecting on the Underhanded Solidity contest. Rather than big promises from early stage projects, the panelists focused on the basics:
- Just knowing how to write solidity isn't enough. Developers, and especially auditors, need to know the EVM, and the ethereum protocol.
- Write more tests! A great comment was on the need to do more testing of large scale interactions. Typically systems are tested interacting with 10 or so accounts, when it would be more realistic to test with 1000s of users.
- Reading carefully: an interesting bit of wisdom I gleaned from Martin Swende. When auditing he reads contracts from bottom to top, which helps him to avoid internalizing the developer's assumptions about the contract system.
I appreciated Raine Revere's comment that there are times when ignoring certain security best practices is justified in order to provide a better user experience, and enable interoperability with other systems.
Underhanded solidity contest repo: https://github.com/Arachnid/uscc
There's much to learn on day 3 and 4 of Devcon, and I'll likely still be trying to assemble a coherent view of the current trends and gaps in smart contract security in the weeks following the conference.