EthIRダウンロード - EthIRソースコードのダウンロード

ethir

Ethereum Bytecodeの高レベル分析のためのフレームワーク。 Ethirは、Ethereum Bytecodeの完全かつ健全なCFGを構築し、プログラムのルールベースの表現（RBR）を生成します。この高レベルの表現により、既存の高レベル分析を適用してEVMコードの特性を推測できます。

インストール（ubuntu）

1. Solidityコンパイラをインストールする（最後のバージョンテスト0.4.25）

Solidityコンパイラの静的な実行可能ファイルを含むフォルダーソースをダウンロードします。

パスに追加し、インストールされていることをテストします。

 sudo cp source/solc* /usr/bin/
 sudo chmod 755 /usr/bin/solc*
 solc --version
 solcv5 --version
 solcv6 --version

最新バージョンをインストールする場合に備えて：

 sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc

2.イーサリアムをインストールする（最後のバージョンがテストされた1.8.18）

フォルダーソースに静的実行可能ファイルが提供されます。

OTをパスに追加し、インストールされていることをテストします。

 sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version

最新バージョンをインストールする場合に備えて：

 sudo apt-get install software-properties-common
 sudo add-apt-repository -y ppa:ethereum/ethereum
 sudo apt-get update
 sudo apt-get install ethereum

3. Z3をインストールします（最後のバージョンテスト4.5.0）

ソースコードフォルダーをダウンロードします。

フォルダーを解凍してインストールします。

 unzip z3-z3-4.5.0.zip
 cd z3-z3-4.5.0
 python scripts/mk_make.py --python
 cd build
 make
 sudo make install

4.依存関係をインストールする（最後のPIPバージョンテスト8.1.1）

pip installコマンドを使用して6つのインストール、Pythonライブラリをリクエストします。

 pip install six
pip install requests

上記のコマンドは、PIPバージョンに応じて失敗する場合があります。その場合は、以前のコマンドではなく、次のコマンドを実行します。

 python -m pip install six
python -m pip install requests

バージョンを確認するには、コマンドpip -Vを実行します。

Ethirを実行します

Ethirを実行するには、フォルダーEthir内で次のコマンドのいずれかを実行します。

SolidityファイルからEthirを実行します。

 ./oyente-ethir -s file_name.sol

EVMファイルからETHIRを実行します：

 ./oyente-ethir -s file_name.evm -b

分解EVMファイルからETHIRを実行します：

 ./oyente-ethir -s file_name.disasm -disasm

オプション

コマンド./oyente-ethir -h ETHIRのすべての利用可能なオプションを含むリストを表示します。最も関連性の高いもののいくつかは次のとおりです。

コントロールフローグラフをテキストモードで保存し、ドットファイルにグラフィカルに保存します。

 ./oyente-ethir -s filename -cfg

saco rbrを生成します

 ./oyente-ethir -s filename -saco

デバッグ情報の表示：

 ./oyente-ethir -s filename -d

Ethirによって生成されたすべてのファイルは、その実行中にdirecrtory/tmp/costabs/に保存されます。

実行例

ETHIRがインストールされたら、分解ファイルブロックのRBRを生成する必要があるとします。フォルダーの例で使用可能なEVM.DISASM 。まず、 Ethir Directoryにアクセスして、コマンドを実行する必要があります./oyente-ethir -s ../examples/blockking.evm.disasm -disasm 。

実行中、Ethirはディレクトリ/TMP/Costabsを作成しました。そこでは、ブロックに関連付けられたRBRを保存します。このディレクトリを検査すると、RBRを含むRBR.RBRという名前のファイルがあります。一般的なエディター（GEDIT、EMACS）を使用してファイルを開くと、RBRが生成されます。以下は、ブロック用に生成されたRBRのスケクトです。

 block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
	s(0) = 96
	s(1) = 64
	l(0) = s(0)
	s(0) = calldatasize
	call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
 
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
	eq(s(0), 0)
	call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))

jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
	neq(s(0), 0)
	call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
 
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
	s(0) = 224
	s(1) = 2
	s(0) = s(1)^s(0)
	s(1) = 0
	s(1) = calldataload
	s(0) = s(1)/s(0)
	s(1) = 607252836
	s(2) = s(0)
	call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))

コマンドを実行する場合./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -eop上記の代わりに、Ethirが生成するRBRには、EVMバイトコードがテキストにインターリーブされます。以下は、ブロックするために生成されたノップアノテーションを備えたRBRのスケッチです。EVM.DISASM：

 block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
	s(0) = 96
	nop(PUSH1)
	s(1) = 64
	nop(PUSH1)
	l(0) = s(0)
	nop(MSTORE)
	s(0) = calldatasize
	nop(CALLDATASIZE)
	call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
	nop(ISZERO)
	nop(PUSH2)
	nop(JUMPI)
 
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
	eq(s(0), 0)
	call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))

jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
	neq(s(0), 0)
	call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
 
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
	s(0) = 224
	nop(PUSH1)
	s(1) = 2
	nop(PUSH1)
	s(0) = s(1)^s(0)
	nop(EXP)
	s(1) = 0
	nop(PUSH1)
	s(1) = calldataload
	nop(CALLDATALOAD)
	s(0) = s(1)/s(0)
	nop(DIV)
	s(1) = 607252836
	nop(PUSH4)
	s(2) = s(0)
	nop(DUP2)
	call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
	nop(EQ)
	nop(PUSH2)
	nop(JUMPI)

Ethirでは、分析されたファイルのCFGを保存することもできます。その場合、コマンドを実行する必要があります./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -cfg 。 Ethirは、Directory /TMP/Costabs/に.cfg拡張子を備えたファイルにCFGを保存します。

ファイルには複数のスマートコントラクトが含まれている場合があることに注意してください。その場合、Ethirは各契約RBR0.RBR、RBR1.RBR、... RBRN.RBRごとに1つのファイルを生成します。

スマートコントラクトの例

フォルダーの例には、ツールをテストするための実行の例が含まれています。 Solidity、EVM、Resasemblyファイルの両方があります。

ブロッキング、evm.disasm、advertisement.sol、validtoken.sol、cryptophoenixなどの例のほとんどは、ブロックチェーンから取得された現実世界の契約であり、loop1.solやsum.solなどの他の例は、抑制プロセスを理解しやすいアドホックの例です。

SACOを使用した境界ループ

SACOは、同時オブジェクトの静的分析器であり、他のプロパティの中でも、ループの反復数の上限を推測できます。これは、スマートコントラクトのガス消費を推測するための最初の重要なステップであることに注意してください。

SACOの内部表現は、マイナーな構文翻訳後にETHIRによって生成されたRBRの文法と一致します。これのおかげで、いくつかの例に含まれるループの終了を証明し、それらのループに線形結合を生成することができます。フォルダーの例に含まれるスマートコントラクトのいくつかについて、SACOによって推測されるループ境界の一部を以下に示します。

スマートコントラクト	バウンド	スマートコントラクト	バウンド
ブロック	NAT（G8/10）*36+8934493	Cryptophoenix	NAT（G3）*228409344+4113285485
ループ1	NAT（A）*25+234	エリグマ	NAT（_NumberOfReturns）*2628+134
宝くじ	159	ブロックsquareseriea	286
飛び地	268	auctusether	264
広告	Inf	validtoken	Inf

SACOは、上の表に示されている最初の4つのスマートコントラクトに線形バインドを行います。スマートコントラクトの範囲はブロックされ、暗号化された契約は、フィールドの1つの値（それぞれ8番目と3番目）の値に依存します。スマートコントラクトループ1とエリグマの場合、得られた境界は、その機能のいくつかの引数に依存しています（aおよび_ numberofturns）。スマートコントラクトに宝くじ、ブロックスケアレシエア、飛び地、またはすべて攻撃などのループが含まれていない場合、SACOは一定の縛られています。

SACOの精度の制限（ビット操作がなく、機能SHA3のモデルがありません）のため、アナライザーはビット変数に関する情報を忘れていることに注意してください。この要因により、SACOは、validtokenやAdvertisementなどのいくつかのスマートコントラクトの拘束力を推測することができず、 INFを返します。

整数遷移システムやホーン条項（Aprove、T2、verymax、coflocoなど）などの中間形式で機能する他の高レベルの分析装置は、ETHIRが生成するRBR翻訳プログラムで作業するために簡単に適応できます。

Pull-Requestまたは新しい問題を介してSACOに連絡するSACO開発者と共同でEthirを使用するのが興味深い場合。

ここで最初のプロトタイプを試すことができます。 GASTAPは、各トランザクションに関与するガスの上限を導きます。

拡大する