Verification on Ethereum DApps

State-of-the-art (updating)

Publication

Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach (FC 18)

ZEUS: Analyzing Safety of Smart Contracts (NDSS 18)

• A good summary by Adrian Colyer

Finding The Greedy, Prodigal, and Suicidal Contracts at Scale (2018)

a new systematic characterization of a class of trace vulnerabilities, which result from analyzing multiple invocations of a contract over its lifetime

three example properties of such trace vulnerabilities:

1. Greedy: lock funds indefinitely,

2. Prodigal (very generous, recklessly wasteful): leak ether carelessly to arbitrary users, or

   1. For section 5.2, Figure 6 example doesn't hold: test contract

3. Suicidal: can be killed by anyone.

   1. based on Parity Multi-sig wallet contract, vulnerable one
   2. safe one ref: open zeppelin's multi-sig wallet implementation

• MAIAN
  • the first tool for precisely specifying and reasoning about trace properties, which employs inter-procedural symbolic analysis and concrete validator for exhibiting real exploits.
  • two major components: symbolic analysis and concrete validation
  • ​
  • depth-first
  • target at bytecode
• Posthumous contract: dead but can receive ether from any transaction. It is a special type of Greedy. (My test in Ropsten) (Contract code)
  • For SUICIDENONEMPTYSTACK test: even if id' is an indocile contract, selfdestruct(id') will send suicide's remaining ether to id'. In other words, any contract can't prevent Ether accepting. Or we say, we can use selfdestruct(id') to send Ether to any contract.

Quantitative Analysis of Smart Contracts (ESOP 18) (Apr 14-20)

• Define a new simplified PL to write smart contracts, which can be converted into stateful games. Then they provide an abstraction-refinement approach for quantitative concurrent games to automatically analyze.
• What is stateful/stateless games?
• mainly on section 4 and 5

Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts (POPL 18) (Jan 10-12) (video)

• Modular reasoning, module of reasoning
  • This paper recommends Modular Verification of Static Class Invariants, and, Ownership confinement ensures representation independence for OO programs
  • It says this topic has been studied extensively with the seminal works of Hoare (Proof of correctness of data representation) and Dijkstra (A discipline of programming)
  • http://www.cs.cmu.edu/~aldrich/oop/ It seems this is a good page to check.
• $ECF_{FS}$: Final-State Effective Callback Freedom
• $ECF_{C}$: Conflict Effective Callback Freedom❔
  • Conflict graph-based algorithm
    • Tracks read/write sets of invocations
    • Builds conflict graph
    • Checks for cycles
• Dynamic checking is decidable.
• Code: Go Ethereum enhanced with ECF Checker, a dynamic monitor of the ECF property, based on Geth.
• TR (Technical Report)

Scilla: a Smart Contract Intermediate-Level LAnguage (Automata for Smart Contract Implementation and Verification) (GitHub)

• Use Coq 8.7, State-Transition Systems for Smart Contracts: semantics and properties.
• Zilliqa is the world's first high-throughput public blockchain platform designed to scale to thousands of transactions per second. It brings the theory of sharding to practice with its novel protocol that increases transaction rates as its network expands. The platform is tailored towards enabling secure data-driven decentralized apps, designed to meet the scaling requirements of machine learning and financial algorithms. Zilliqa has been under research and development for two years. It has powered several ground-breaking deployments commercially to date.
  • Latest Testnet Trial Run: 2488 TX/S, 6 shards and 3600 nodes.
• Section 2: contracts as Communicating Automata
  • ​

Decentralization in Bitcoin and Ethereum Networks (WTSC@FC 18) (Mar 2, 2018)

• Key tool: Falcon relay network
• Key findings:
  • Bitcoin network can increase the bandwidth requirements for nodes by a factor of 1.7 and keep the same level of decentralization
  • Bitcoin network is geographically more clustered than Ethereum, with many nodes likely residing in datacenters
  • Ethereum has lower mining power utilization than Bitcoin and would benefit from a relay network
  • small miners experience more volatility in block rewards in Bitcoin and Ethereum

An Empirical Analysis of Smart Contracts: Platforms, Applications, and Design Patterns (WTSC 17@FC) (Apr 7, 2017)

• Several platforms for smart contracts have been proposed, and this paper have analyzed the usage of smart contracts from various perspectives. Mainly, by manually analyzing 834 smart contracts from Ethereum (811, verified) and Bitcoin (23), it concludes 5 categories describing smart contracts intended application domain, and 9 design patterns. Among these, they observe that token, authorization, time constraint, and termination are generally the most used patterns. Also, they give the quantitative results in details.

• Another contribution is the analysis of platforms. At first, they drew up a candidate list, 12 platforms, by examining all 175 articles of coindesk.com in "smart contracts" category by Sept 15, 2016. Then ruled out half of them by 3 criteria:

  • have already been launched,
  • are running and supported from a community of developers, and
  • are publicly accessible.

  They get the sample of 6 platforms (Bitcoin, Ethereum, Counterparty, Stellar, Monax and Lisk), and give the results, mainly considering blockchain types, contract languages, transaction amount and market shares.

• 5 categories:

  • Financial
  • Notary
  • Game
  • Wallet
  • Library

• 9 design patterns:

  • Token
  • Authorization: relating to critical operations
  • Oracle: the interface between contracts and the outside
  • Randomness
  • Poll: allows users to vote on some question
  • Time constrain
  • Termination
  • Math: e.g., SafeMath.sol
  • Fork check

• Good survey, helpful to beginners. However, it didn't analyze DSL or VM used for smart contracts. For example, high-level languages like Solidity or Viper, and low-level virtual machines like EVM or IELE. Also, some platforms claim they support

A Concurrent Perspective on Smart Contracts (WTSC 17)

• A good summary by Adrian Colyer

Defining the Ethereum Virtual Machine for Interactive Theorem Provers (FC 17)

"To our knowledge, ours is the first formal EVM definition for smart contract verification that implements all instructions. Our definition can serve as a basis for further analysis and generation of Ethereum smart contracts."

Formal verification of Smart Contracts (Short paper, workshop) (PLAS 16)

• attempt to use F* framework to do formal verification on smart contracts
• Solidity or EVM

A Survey of Attacks on Ethereum Smart Contracts (SoK) (Systematization of knowledge paper) (POST 17)

In this paper we provide the first systematic exposition of the security vulnerabilities of Ethereum and of its high-level programming language, Solidity.

• online examples
  • only provides 5 attacks: SimpleDAO (reentry), KotET (mishandled exception and indocile receiver), OddsAndEvens (public secret), Governmental (time constraints and unpredictable states) and dynamic libraries (function visibility), and 1 miscellanea: gasless send.
  • two Solidity versions: 0.3.1 and 0.4.2
• some notes for function calling process:
• Each function is uniquely identified by a signature, based on its name and type parameters.
• If the signature matches one function, the execution will jump to that, else jump to fallback function.
• Modifier checking happens in function's inter logic.
• Sometimes, invocation to fallback function will have 0x3af39c21 in data field.
• My Test Contract in Ropsten

Make Smart Contracts Smarter (CCS 16)

• Oyente, a verification tool using symbolic execution. It declares that Oyente can detect four main vulnerabilities: timestamp dependency, front running (money concurrency), mishandled exceptions and reentry bugs.

Hawk: The Blockchain Model of Cryptography and Privacy-Preserving Smart Contracts (SP 2016)

• ​

Town Crier: An Authenticated Data Feed for Smart Contracts (IACR 16)

• TBR

Scripting smart contracts for distributed ledger technology (IACR 16)

• TBR

The Ring of Gyges: Investigating the Future of Criminal Smart Contracts (IACR 16)

• TBR

Step by Step towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab (IACR 15)

• (TBR)

True Attacks in Real World

The DAO in Jun 2016

The Parity Bug in Jul 2017

The Parity Bug in Nov 2017

Some thoughts for vulnerabilities

Currently, types of vulnerabilities can be divided as 3 main categories: external calling, internal execution and blockchain limitation.

Several tools to detect bugs

• Transaction-based: (External)

inter-procedural, trigger + modules

• EVM based: (Internal) (Single)

Intra-procedural

• Chain property: relay network

Tools

MAIAN

• source code

Manticore

• Manticore is a symbolic execution tool for analysis of binaries and smart contracts.
  • Linux ELF binaries (x86, x86_64 and ARMv7)
  • EVM bytecode (video 1) (video 2)
    • Folder example provides coverage, minimal and so on. Mainly simple usages of API.
• Manticore: Symbolic execution for humans
• Dynamic binary analysis tool with EVM support (described in Ethereum Smart Contract Best Practices)
• CLI (Command-line Interface)

czc@vultr:~/manticore/examples/linux$ manticore basic
2018-01-30 16:48:42,626: [7231] m.manticore:INFO: Loading program basic  
2018-01-30 16:48:52,257: [7231] m.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0   
2018-01-30 16:48:53,831: [7231] m.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0   
2018-01-30 16:48:53,834: [7231] m.manticore:INFO: Results in /home/czc/manticore/examples/linux/mcore_t9BiJE      
2018-01-30 16:48:53,834: [7231] m.manticore:INFO: Total time: 9.56235694885  
czc@vultr:~/manticore/examples/linux$ cat mcore_t9BiJE/test_00000000.stdin | ./basic   
Message: It is greater than 0x41   
czc@vultr:~/manticore/examples/linux$ cat mcore_t9BiJE/test_00000001.stdin | ./basic   
Message: It is less than or equal to 0x41 

• API
  • API Reference
  • Manticore Documentation 0.1.0 (released on Mar 22, 2018)

czc@vultr:~/manticore/examples/script$ python count_instructions.py ../linux/helloworld   
Executed  6266  instructions. 

Mythril

• Reversing and bug hunting framework for the Ethereum blockchain (described in Ethereum Smart Contract Best Practices)

• Documentation mythril 0.14.9

• Install

  • require libssl-dev
  • Currently, I use python3 -m venv ./ in a test directory, then cd bin and source activate.

• Note

  • Mythril requires Python 3.5 to work.
  • It is built on laser-ethereum, a Z3-based symbolic Ethereum VM.

• Introducing Mythril: A framework for bug hunting on the Ethereum blockchain by Bernhard Mueller, a security engineer at ConsenSys.

full node needs or use infura

• Analyzing Ethereum smart contracts for vulnerabilities

In this article, I’ll show how to run different types of security scans with Mythril using smart contracts from the Ethernaut wargame as examples (thanks to the guys from Zeppelin solutions for giving me permission). If you haven’t tried the wargame yourself, be aware that there are spoilers ahead! I recommend giving it a shot yourself first if you haven’t already.

• news: Mythril: The New Ethereum Blockchain Error Detector
• Upcoming Talk, April 12, 2018, Smashing Ethereum Smart Contracts for Fun and ACTUAL Profit, by Bernhard Mueller

Solidity Parser

A Solidity parser in Javascript. So we can evaluate and alter Solidity code without resorting to cruddy preprocessing.

• In: Solidity code
• Out: AST
• Warning: not deal with constructor

Solgraph

• In: AST (thus dependent on Solidity Parser)
• Out: DOT graph
• Generates a DOT graph that visualizes function control flow of a Solidity contract and highlights potential security vulnerabilities.
• Visualize Solidity control flow
• not support for EVM bytecode
• a Node.js package

Dr.Y's Ethereum Contract Analyzer

• Online Version
  • Input: bytecodes
• Programming language: OCaml
• Notes:
  • use and rename the pre-compiled one to opam, modify the PATH and wait opam init for a long time (about an hour).
  • It starts a web server at localhost:xxxx, xxxx is specified by yourself.
• Code structure:❔
  • TODO
• Issues:
  • 20 open now in Github

Securify

• Automatically Detecting the Bug that Froze Parity Wallets
• team page

SmartCheck

• provided by SmartDec

SmartCheck: Static Code Analyzer
We have built our own static code analyzer for Solidity. Our full analysis includes complete manual analysis and verification of all the issues reported by SmartCheck.

Oyente

EthFiddle Solidity IDE in the Browser

• Powered By Loom Network

####Vyper online

• Documentation
• Github repo
• Install: pip install vyper, Python 3 required.
• vyper-run: support some features as hevm.

Remix - Solidity IDE

• should pay attention to input format:
  • address: "0xcafecafecafe..."
  • address []: ["0x...", "0x..."]
  • uint256: 0xcafecafecafe...
• Security
  • Transaction origin: Warn if tx.origin is used
  • Check effects: Avoid potential reentrancy bugs
  • Inline assembly: Use of Inline Assembly
  • Block timestamp: Semantics maybe unclear
  • Low level calls: Semantics maybe unclear
  • Block.blockhash usage: Semantics maybe unclear
  • Selfdestruct: Be aware of caller contracts.
• Gas & Economy
  • Gas costs: Warn if the gas requirements of functions are too high.
  • This on local calls: Invocation of local functions via this
  • Delete on dynamic Array: Use require and appropriately
• Miscellaneous
  • Constant functions: Check for potentially constant functions
  • Similar variable names: Check if variable names are too similar
  • no return: Function with return type is not returning
  • Guard Conditions: Use require and appropriately
  • Result not used: The result of an operation was not used.

Other Useful Development Tools or Testing Framework

Formal verification framework

• AxLang: Formally Verifiable Smart Contracts for the Ethereum Ecosystem
• Bamboo
• Certik

Disassembler

• evmdis: human readable
  • echo -n $(cat your.bin-runtime) > true.bin-runtime
  • cat true.bin-runtime | evmdis > your.disasm
• hevm: can specify some opcode behaviors
• opcode-tool: Etherscan online
• evm disasm:
• Solidity online toolbox

Function Signature

• Keccak-256
• Ethereum Function Signature Database

The Truffle Framework

• Truffle is the most popular development framework for Ethereum with a mission to make your life a whole lot easier.
• Truffle: smart contract compilation, library linking, creation of contract artifacts, interacting with smart contracts on the front-end
• Ganache (TestRPC): Personal blockchain and explorer for development
  • Quickly fire up a personal Ethereum blockchain which you can use to run tests, execute commands, and inspect state while controlling how the chain operates.
• Drizzle: Reactive web3 and smart contracts for easier integration with JS frameworks (coming soon)
• Truffle Box:

Explorer for Blockchain

• MyEtherWallet:
• getStorageAt: how to read smart contract storage

Decompiler

• porosity (report) (July 7, 2017) (talk at DEFCON25)
  • Decompiler and Security Analysis tool for Blockchain-based Ethereum Smart-Contracts
  • Three main usages:
    1. Disassemble
    2. Decompilation
    3. Some bugs detection: (TODO: figure out the logic for each supported type)

    • Notes:

      1. --code is mandatory. --abi is optional but recommended.
      2. --cfg can generate dot code for contract's CFG. Save the output as file.dot then dot file.dot -Tpdf -o image.pdf to get the image (Install graphviz: sudo apt-get install graphviz). Among -Tps, -Tpng and -Tpdf, -Tpdf is the best.

    • Install

      1. Download from Github and follow this page
      2. Set environments by command abi=$(cat ./output/SendBalance.abi)
      3. -- code can be followed by $bin or $binRuntime.

    • Problems/issues:

      1. executeInstruction: NOT_IMPLEMENTED: REVERT | NUMBER | MSIZE

    • Some try:

      1. To decompile CryptoKitties geneScience contract, it crashed for massive memory usage.
      2. To decompile provided vulnerable.sol but failed, too.

parse: Please at least provide some byte code (--code) or run it in debug mode (--debug) with pre-configured inputs.
Porosity v0.1 (https://www.comae.io)
Matt Suiche, Comae Technologies <support@comae.io>
The Ethereum bytecode commandline decompiler.
Decompiles the given Ethereum input bytecode and outputs the Solidity code.


Usage: porosity [options]
Debug:
    --debug                             - Enable debug mode. (testing only - no input parameter needed.)

Input parameters:
    --code <bytecode>                   - Ethereum bytecode. (mandatory)
    --code-file <filename>              - Read ethereum bytecode from file
    --arguments <arguments>             - Ethereum arguments to pass to the function. (optional, default data set provided if not provided.)
    --abi <arguments>                   - Ethereum Application Binary Interface (ABI) in JSON format. (optional but recommended)
    --hash <hashmethod>                 - Work on a specific function, can be retrieved wit --list. (optional)

Features:
    --list                              - List identified methods/functions.
    --disassm                           - Disassemble the bytecode.
    --single-step                       - Execute the byte code through our VM.
    --cfg                               - Generate a the control flow graph in Graphviz format.
    --cfg-full                          - Generate a the control flow graph in Graphviz format (including instructions)
    --decompile                         - Decompile a given function or all the bytecode.

Test Coverage

Solidity-coverage

• https://github.com/sc-forks/solidity-coverage

Library

OpenZeppelin

• OpenZeppelin, a framework to build secure smart contracts on Ethereum
• e.g., SafeMath.sol and Ownable.sol

Semantics

KEVM

• K
  • ERC20-K: Formal Executable Specification of ERC20

LEM

• Formal Verification of Deed Contract in Ethereum Name Service (pdf)
  • It verifies a specific contract. The target is the EVM bytecode for "Deed", a contract part of the Ethereum Name Service. The theorem proved through Isabelle/HOL states that, upon an invocation of the contract, only its owner can decrease the balance.

Virtual Machine

IELE

Framework

embark

Framework for serverless Decentralized Applications using Ethereum, IPFS and other platforms

Useful Resources

• https://github.com/pirapira/ethereum-formal-verification-overview
• https://github.com/pirapira/awesome-ethereum-virtual-machine
• Week in Ethereum News
• Solidity Bug Info
• Awesome Ethereum
• awesome-solidity