Devcon3 Security Round Up

Maurelian
Maurelian
Nov 3, 2017 · 5 min read

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

  1. Tools
  2. Formal verification
  3. New languages

Tools

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:

EVM-LAB

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 opviewer (aka Retromix), which is an in terminal version of the Remix debugger, and is part of his EVM-Lab tools.

Martin Swende’s ‘Retromix’

He also discussed the Ethereum Foundations work using fuzz testing to scale consensus testing between different EVM implementations.

More information:

evmlab repository
TestEth (fuzzing in evmlab)
evmFuzz repository
Talk recording

Zeppelin OS

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.

More information:
Site
Whitepaper
Talk Recording: Not yet available

Static Analysis

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.

More information:
Oyente IDE
Oyente paper
Talk Recording: Not yet available

Securify site
Talk Recording: Not yet available

Hydra Framework

Hydra is an interesting project from the prolific Phil Daian (and his talented colleagues), taking a 3-pronged approach to security:

  1. Formal verification and specification
  2. escape hatches
  3. 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).

Hydra Repo Paper: https://thehydra.io/paper.pdf
Slides
Talk Recording: Not yet available

New languages

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.

Viper

I was fortunate to get a tutorial from David Knott, a primary contributor to the Viper compiler. Viper’s design is more constrained 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).

Viper repository
Viper Docs

Bamboo

Bamboo is a functional programming language being designed by Dr. Yoichi, (formal verification engineer at the Ethereum foundation). Bamboo uses makes state transitions explicit, while having the “sugarly syntax to trap solidity developers”. Incidentally, Yoichi’s dry humor is hilarious.

Although very early, I think Bamboo is promising, and I’m excited to watch this project evolve.

Talk slides
Bamboo repository
Talk Recording: Not yet available

Babbage

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

Solidity improvements

Though solidity lacks the shiny newness of the more experimental languages, Solidity continues to mature, becoming more battle hardened with each release (and each vuln).

Julia IR
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.

SMTChecker
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.

Slides: https://chriseth.github.io/notes/talks/solidity_update_devcon3/

Formal verification

K-EVM

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

Formally verifying Casper

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

Good old secure programming

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

Bringing it all together

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.

Do you love this stuff?

I’m part of the team at ConsenSys Diligence. If you have a knack for diving deeply into Solidity and the EVM, and an interest in smart contract security, we’re looking for people to join our smart contract audit practice (apply here).

Maurelian

Written by

Maurelian

More From Medium

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade