Neutrinoで働くブロックチェーンエンジニアのブログ

渋谷の専門特化コワークNeutrinoに入居してブロックチェーンエンジニアとして働いています。元丸の内。(Neutrino運営企業とは直接関係ありません)

セキュリティ分析ツールMythrilで、一部のERC20トークンで問題の関数を解析する

Mythrilとは

f:id:naomasabit:20180514010330p:plain:w300

Consensys社が開発している「Security analysis tool for Ethereum smart contracts」です。

Mythril公式 consensys.net

mythrilのgithubのREADMEより。

Mythril is a security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. The analysis is based on laser-ethereum, a symbolic execution library for EVM bytecode.

スマートコントラクト処理の解析を行なって脆弱性の分析を行います。 EVM上での動作に基づいており、deploy済みのコントラクトも解析できます。 以下の分析手法を利用していると書いてあります。

  • concolic analysis

concolic testingという、コードからカバレッジを最大化する変数を生み出す手法。concolicはconcreteとsymbolicからの造語

元論文は"CUTE: a concolic unittesting engine for C"(Sen, Koushik; Darko Marinov, Gul Agha 2005)

  • テイント解析

注目したいデータに設定したタグを伝搬させて追跡することで,プログラムやデータ間の依存関係を分析する手法

Mythrilでチェックできるコントラクトの問題について

Mythril-Detection-Capabilitiesを基に以下表に書いてみましたが、一部情報がまとめきれていないものもあるため、後々追記します。

問題 概要
Unprotected functions 重要でかつ、誰でも呼び出し可能な関数の存在
Missing check on CALL return value 呼び出しで戻ってくる値に対して検証がない処理
Re-entrancy 危険なコントラクトの外部呼び出しに基づいて、呼び出し元コントラクトの状態を決定する危険性(DAO事件などは、外部呼び出しを繰り返し行って発生した)
Multiple sends in a single transaction 一度のトランザクションで複数回の送金を行う事
External call to untrusted contract 危険なコントラクトの外部呼び出し
Delegatecall or callcode to untrusted contract
Integer overflow/underflow オーバーフロー、アンダーフローの危険性
Timestamp dependence タイムスタンプ依存の処理(マイナーによってタイムスタンプは記録されるため、必ずしも正しいとは言えない)
Payable transaction does not revert in case of failure
Use of tx.origin
Type confusion
Predictable RNG
Transaction order dependence
Information exposure
Complex fallback function (uses more than 2,300 gas) 多量のgasを利用する複雑なfallback関数
Use require()instead of assert() assert関数は、不変条件をチェックする時のみに利用するのが推奨されている。require関数の方が適切な場合
Use of depreciated functions throw関数よりrevert関数が適切な場合
suicide関数よりselfdestruct関数が適切な場合
sha3関数よりkeccak256が適切な場合
Detect tautologies 常にTRUEと評価される比較条件を検出する
Call depth attack EIP150によって改善された「Deprecated/historical attacks」の検出

batchTransferのオーバーフロー問題について

2018年4月下旬、一部のERC20トークンについて、独自実装がされていたトークンについてOverFlowの脆弱性があり、不正送金が発生するという問題が起きました。

batchTransferという独自の関数にオーバーフローを起こす余地を残していたため、BatchOverflow問題と呼ばれています。

BeautyChainというトークンでは兆以上の数量のトークンが一気に引き出されたようです。

以下は解説記事などです。

medium.com

blockchain.gunosy.io

batchTransferを解析してみる

MythrilのDockerイメージ作成

Mythrilのソースコードを取得します。

git clone https://github.com/ConsenSys/mythril/

cd mythril

楽に動かすために、Dockerfileが提供されているので、dockerイメージを作成します。(Dockerがなければインストールします)

docker build . -t mythril

問題のあったコントラクトを取得

BeautyChainというトークン($BEC)で問題のbatchTransferが実装されていました。

本来はノードから取得するべきなんでしょうが、今回は手軽にEtherscanからコントラクトを取得します。

Etherscan上のBeautyChainのトークンコントラクト

Etherscan上からコピーします。

f:id:naomasabit:20180514005144p:plain

適当なフォルダを作成して、その中にコピーしたコントラクトを「BECToken.sol」として保存します。

mkdir $HOME/tmp #この中に「BECToken.sol」を保存する。

コンテナを起動してMythrilを実行

作成したmythrilタグのイメージからコンテナを作成し、bashでコンテナの中に入リます。

docker run -it -d --name mythril-container -v $HOME/tmp:/var/tmp mythril bash #コンテナ作成
docker exec -it mythril-container bash #コンテナの中に入る

mythrilを実行します。「BECToken.sol:PausableToken」はBECToken.sol内のPausableTokenコントラクトを分析するという意味合いです。

PausableTokenコントラクト内にはbatchTransfer関数が含まれています。

cd /var/tmp
myth -x BECToken.sol:PausableToken > sec_analysis.txt #mythrilでセキュリティ分析を実行

分析結果を確認する

ホスト側のマウントしている「$HOME/tmp」フォルダに行き、出力された分析結果「sec_analysis.txt」を確認します。transferについてassertを利用して起きる可能性のある問題、オーバーフローの可能性がある問題との警告してtransfer, batchTransferが検出されました。

オーバーフローの確認としては、OPCODEとして"ADD", "MUL"があるかどうかなどを判断して検出しているようです。

==== Exception state ====
Type: Informational
Contract: PausableToken
Function name: transfer(address,uint256)
PC address: 4229
A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. 
--------------------
In file: BECToken.sol:29

c;
  }
}

/**


--------------------

==== Integer Overflow  ====
Type: Warning
Contract: PausableToken
Function name: transfer(address,uint256)
PC address: 4216
A possible integer overflow exists in the function `transfer(address,uint256)`.
The addition or multiplication may result in a value higher than the maximum representable integer.
--------------------
In file: BECToken.sol:28


    

--------------------

==== Integer Overflow  ====
Type: Warning
Contract: PausableToken
Function name: batchTransfer(address[],uint256)
PC address: 1587
A possible integer overflow exists in the function `batchTransfer(address[],uint256)`.
The addition or multiplication may result in a value higher than the maximum representable integer.
--------------------
In file: BECToken.sol:263

es[_receivers[i]].add

--------------------

警告が少ないに越したことはないですが、やや広範に出す可能性があるため、実務において出てきた警告を基に個別に精査していく必要がありそうだと思いました。

今回のような事件があるとコントラクトのデプロイ時に緊張しますが、mythrilを利用する事で脆弱性のチェックに利用できそうです。