Mythrilとは
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というトークンでは兆以上の数量のトークンが一気に引き出されたようです。
以下は解説記事などです。
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上からコピーします。
適当なフォルダを作成して、その中にコピーしたコントラクトを「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を利用する事で脆弱性のチェックに利用できそうです。
