首頁>JSP源碼>其他類別
下載

ethir

以太坊字節碼的高級分析的框架。 Ethir構建了以太坊字節碼的完整而聲音的CFG，並生成了程序的基於規則的表示（RBR）。這種高級表示可以應用現有的高級分析來推斷EVM代碼的屬性。

安裝（Ubuntu）

1。安裝堅固編譯器（最後版本測試了0.4.25）

下載包含固體編譯器的靜態可執行文件的文件夾源。

將其添加到路徑中並測試安裝它。 

 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命令安裝六個，請求Python庫。 

 pip install six
pip install requests

以上命令可能會根據PIP版本失敗。如果是這種情況，請運行以下命令而不是先前的命令。 

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

檢查版本運行命令pip -V 。

運行Ethir

要執行Ethir，請在文件夾Ethir中運行以下命令之一：

  1. 從堅固文件運行Ethir： 
 ./oyente-ethir -s file_name.sol
  1. 從EVM文件運行Ethir： 
 ./oyente-ethir -s file_name.evm -b
  1. 從拆卸EVM文件運行Ethir： 
 ./oyente-ethir -s file_name.disasm -disasm

選項

命令./oyente-ethir -h顯示一個列表，其中包含Ethir的所有可用選項。一些最相關的是：

  1. 將Control-Folw-Graph存儲在文本模式下，並以圖形方式存儲在點文件中： 
 ./oyente-ethir -s filename -cfg
  1. 生成saco rbr 
 ./oyente-ethir -s filename -saco
  1. 顯示調試信息： 
 ./oyente-ethir -s filename -d

Ethir在執行過程中生成的所有文件都存儲在DiRecrtory/TMP/Costabs/中。

運行示例

安裝Ethir後，假設我們要生成文件夾示例中可用的拆卸文件blockking.evm.disasm的RBR。首先，我們必須去Ethir目錄並執行命令./oyente-ethir -s ../examples/blockking.evm.disasm -disasm 。

在執行過程中，Ethir創建了目錄/TMP/Costabs/它存儲與Blockking.evm.disasm文件相關的RBR的位置。如果檢查此目錄，我們會找到一個名為rbr.rbr的文件，其中包含RBR。如果我們使用任何通用編輯器（GEDIT，EMAC）打開文件，我們可以看到生成的RBR。以下是用於blockking.evm.disasm文件的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具有NOPS註釋，EVM Bytecode在文本中交織在一起。以下是RBR的草圖，該rbr具有用於blockking.evm.disasm的NOPS註釋： 

 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將CFG存儲在文件/tmp/costabs/Costabs/Costabs中的文件中。

請注意，文件可能包含多個智能合約。在這種情況下，Ethir每個合同RBR0.RBR，rbr1.rbr，... rbrn.rbr產生一個文件。

智能合約示例

文件夾示例包含運行示例來測試該工具。既有固體，EVM和拆卸文件。

大多數示例，例如bloccking.evm.disasm，advertisement.sol，valialToken.sol或cryptophoenix.sol.sol是從區塊鏈中獲得的真實合同，而其他諸如loop1.sol和sum.sol等其他合同則是更容易理解分解過程的雜物示例。

使用Saco邊界循環

SACO是並發對象的靜態分析儀，可以推斷出循環迭代次數的其他屬性。請注意，這是推斷智能合約的氣體消耗的第一步。

SACO的內部表示與小句法翻譯後Ethir產生的RBR的語法相匹配。因此，它可以證明某些示例包含的循環的終止，並為這些循環產生線性結合。以下是Saco推斷出的一些循環範圍，用於文件夾示例中包含的一些智能合約：

智能合約邊界智能合約邊界
蓋帽NAT（G8/10）*36+8934493隱態NAT（G3）*228409344+4113285485
loop1 NAT（A）*25+234 Eligma NAT（_NUMBEROFRETURNS）*2628+134
彩票159 Blocksquareseriea 286
飛地268 auctusether 264
廣告inf有效的語inf

Saco侵入上表中顯示的前四個智能合約的線性綁定。智能合約的界限阻礙和隱腳質取決於其一個字段的價值（分別為第八和第三個領域）。對於Smart Contracts Loop1和Eligma，獲得的界限取決於其某些功能的參數（a和_numberofturns）。如果智能合約不包含任何循環，例如彩票，塊秒，飛地或送禮，薩科會延伸一個恆定的結合。

請注意，由於SACO的精確限制（它沒有比特操作和功能SHA3的模型），分析儀忘記了位變量的信息。由於這一因素，Saco無法推斷出某些智能合約（例如有效的或廣告）並返回INF的某些智能合約。

在整數過渡系統或Horn條款（例如，Aprove，T2，非常Max，Cofloco）等中間形式上工作的其他高級分析儀也可以很容易地適應Ethir生產的RBR翻譯程序。

如果您在與SACO聯合使用Ethir通過拉裝或新問題聯合使用Ethir。

您可以在此處嘗試第一個原型。 Gastap注入每次交易中涉及的氣體的上限。

展開
附加信息
相關應用
爲您推薦
相關資訊 全部