はじめに

先日開催された The IEEE Blockchain-2020にて、Ethereum Smart Contractの脆弱性であるRe-entrancy の解析手法についての論文が採択されたので、ざっくり概要を書いてみようと思います。

これはRA(Re-entrancy Analyzer)というツールとして公開されています。
またarXivでも論文が公開されています。

超概要

解析手法を3行でまとめてしまうと

コードをシミュレートして
ただの関数呼び出しの実行経路とRe-entrancy攻撃による関数呼び出しの実行経路を抽出して
両者を比較
です。
両者に差異がなければRe-entrancyなし、差異があればRe-entrancyありです。

Re-entrancyとは

Ethereum Smart Contractの最も代表的な脆弱性で、不正な関数の再帰呼び出しを引き起こします。Ethereum史上最大の事件"The DAO"では、この脆弱性を突くことでコントラクトの送金処理が繰り返し実行され、莫大な被害が発生しました。
Ethereum Smart Contract Best Practicesに掲載されているコード例が以下です。これは銀行の役割を持つコントラクトの通貨の引き出し処理を行う関数を想定しています。

// INSECURE
mapping (address => uint) private userBalances;

function withdrawBalance() public {
    uint amountToWithdraw = userBalances[msg.sender];
    (bool success, ) = msg.sender.call.value(amountToWithdraw)(""); // At this point, the caller's code is executed, and can call withdrawBalance again
    require(success);
    userBalances[msg.sender] = 0;
}

攻撃のポイントをまとめるとこんな感じ。

ユーザーの残高をリセットする(最終行)前に送金処理を行なっている(下から3行目)。
Ethereumにおいて、コントラクトによる他のコントラクトへの送金と関数呼び出しはどちらもコントラクト呼び出しであり、同一である。
関数呼び出しの際に指定した関数が存在しない場合、fallback関数という名無しの関数が実行される。
普通の送金処理では呼び出す関数を指定しないため、fallback関数が実行される。
攻撃者は、自分が用意したコントラクトのfallback関数の中で被害者コントラクトの関数withdrawBalanceを呼び出す。

以上より、ユーザーの残高がリセットされる前に送金処理が再帰的に実行され、被害者コントラクトがもつ暗号通貨が吸い尽くされてしまいます。

シンボリック実行(コードのシミュレート)

コードのシミュレートには、シンボリック実行(symbolic execution)という手法が用いられます。
これは、引数のようなコード上では不定な値を"シンボル変数"という任意の値を表す変数として表現することで擬似的な実行を行うものです。シンボリック実行によって、プログラムが取りうるあらゆる状態を網羅的に探索することができます。

RAでは、SolidityではなくEVM(Ethereum Virtual Machine)の命令をシンボル変数を処理できる形で実装することでコントラクトのシンボリック実行を可能にしています。

経路条件式(実行経路)

経路条件式(path condition)とは、プログラムがある状態に至るまでに満たされる必要のある条件式です。
例えば以下のようなpythonコードがあるとします。


if 0 <= a:
    return 1
else:
    return 0

このコードの経路のイメージ図は以下です。

プログラムの先頭は必ず実行されるので、初めの経路条件式は恒真です。
return 0 の行に到達するにはa < 0 である必要があるのでこれがこのブロックの経路条件式です。またreturn 1してるブロックに到達するには0 <= aである必要があり、これがこのブロックの経路条件式となります。

このように、条件分岐が増えるにつれ経路条件式が複雑になっていきます。

経路条件式の比較

Re-entrancyの検出には、通常の実行の際の経路条件式とRe-entrancy攻撃が発生した際の経路条件式を比較します。両者のイメージは以下です。

左が通常、右がRe-entrancy攻撃です。右の攻撃コントラクトでは単純な関数呼び出しのみを行います。そのためRe-entrancyを持たない関数の場合、左と右の結果は一致します。Re-entrancyを持つ場合、関数呼び出しが成功する際に満たされるべき条件が通常の関数呼び出しと異なるため、最終的な経路条件式が左右で異なります。厳密にはプログラムの終端状態は当然複数あり、それぞれが経路条件式を持つので、左と右で経路条件式が恒等式となるようマッチングできるかで一致判定を行います。

余談1

これは実は私の学生時代の研究です、えへへ

余談2

久々にコードをリファクタリングしてgithubにプッシュしたら完全に赤の他人のアカウントでコミットされてしまいました。こんなことあるんでしょうか。気持ち悪すぎます。過去のコミットを消しても消えません。助けてください。