EthIR
1.0.0
Ein Rahmen für eine hochrangige Analyse von Ethereum-Bytecode. Ethir erstellt eine vollständige und solide CFG eines Ethereum-Bytecode und generiert eine regelbasierte Darstellung (RBR) des Programms. Diese hochrangige Darstellung ermöglicht die Anwendung vorhandener hochrangiger Analysen, um die Eigenschaften des EVM-Codes zu schließen.
Laden Sie die Ordnerquelle herunter, die eine statische ausführbare Datei des Soliditätskompilers enthält.
Fügen Sie es dem Pfad hinzu und testen Sie, dass es installiert ist.
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
Falls Sie die neueste Version installieren möchten:
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
Eine statische ausführbare Datei wird in der Ordnerquelle angegeben.
Fügen Sie OT zum Pfad hinzu und testen Sie, dass er installiert ist.
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
Falls Sie die neueste Version installieren möchten:
sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum
Laden Sie den Quellcodeordner herunter.
Dekomprimieren Sie den Ordner und installieren Sie ihn.
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
Verwenden Sie den Befehl pip install , um sechs zu installieren, fordert Python -Bibliotheken an.
pip install six
pip install requests
Die obigen Befehle können je nach PIP -Version fehlschlagen. Wenn dies der Fall ist, führen Sie den folgenden Befehl anstelle der vorherigen aus.
python -m pip install six
python -m pip install requests
Um die Version zu überprüfen, führen Sie den Befehlspip pip -V aus.
Führen Sie zum Ausführen von Ethir einen der folgenden Befehle im Ordnerethir aus:
./oyente-ethir -s file_name.sol
./oyente-ethir -s file_name.evm -b
./oyente-ethir -s file_name.disasm -disasm
Der Befehl ./oyente-ethir -h zeigt eine Liste mit allen verfügbaren Optionen von Ethir an. Einige der relevantesten sind:
./oyente-ethir -s filename -cfg
./oyente-ethir -s filename -saco
./oyente-ethir -s filename -d
Alle von Ethir während seiner Ausführung generierten Dateien werden im Direcrtory/TMP/Costabs/gespeichert.
Sobald Ethir installiert ist, möchten wir den RBR der Demontagedatei blocking.evm.disasmus in den Ordner Beispielen generieren. Zunächst müssen wir in das Ethir -Verzeichnis gehen und den Befehl ausführen ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm dort.
Während der Ausführung hat ETHIR das Verzeichnis /TMP/Costabs erstellt/ wo es die mit blocking.evm.disasm -Datei zugeordnete RBR speichert. Wenn wir dieses Verzeichnis inspizieren, finden wir eine Datei namens RBR.RBR , die die RBR enthält. Wenn wir die Datei mit einem gemeinsamen Editor (Gedit, EMACs) öffnen, können wir die generierte RBR sehen. Unten finden Sie eine Skecth der RBR, die für Blocking.evm.Disasm -Datei erzeugt wurde:
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))
Wenn wir den Befehl ausführen ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -eop anstelle des oben genannten Eins, hat der RBR, den Ethir erzeugt, NOPS -Annotationen, wobei der EVM -Bytecode im Text eingegrenzt ist. Unten finden Sie eine Skizze des RBR mit NOPS -Anmerkungen, die für Blocking erzeugt wurden.
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 ermöglicht es uns auch, den CFG der analysierten Datei zu speichern. In diesem Fall müssen wir den Befehl ausführen ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -cfg . Ethir speichert den CFG in einer Datei mit .CFG -Erweiterung im Verzeichnis /TMP/Costabs/ .
Beachten Sie, dass eine Datei möglicherweise mehr als einen intelligenten Vertrag enthält. In diesem Fall generiert Ethir eine Datei pro Vertrag RBR0.rbr, RBR1.rbr, ... rbrn.rbr.
Die Beispiele der Ordner enthalten laufende Beispiele, um das Tool zu testen. Es gibt sowohl Soliditäts-, EVM- als auch Demontagedateien.
Die meisten Beispiele wie bloccing.evm.disasasmus, advertisement.sol, validToken.sol oder Cryptophoenix.sol sind reale Verträge, die aus der Blockchain erhalten wurden, während andere wie Loop1.Sol und Summe.
SACO ist ein statischer Analysator für gleichzeitige Objekte, der unter anderem Obergrenzen auf die Anzahl der Iterationen von Schleifen schließen kann. Beachten Sie, dass dies der erste entscheidende Schritt ist, um den Gasverbrauch von intelligenten Verträgen zu schließen.
Die interne Darstellung von SACO entspricht der Grammatik des RBR, die nach geringfügigen syntaktischen Übersetzungen von Ethir erzeugt wird. Dank dessen kann die Beendigung der Schleifen nachweisen, dass einige der Beispiele eine lineare Grenze für diese Schleifen enthalten. Hier sind einige der von Saco abgeleiteten Schleifengrenzen für einige der in den Ordner Beispiele enthaltenen intelligenten Verträgen:
| Intelligenter Vertrag | Gebunden | Intelligenter Vertrag | Gebunden |
|---|---|---|---|
| Blockierung | Nat (G8/10)*36+8934493 | Cryptophoenix | Nat (G3)*228409344+4113285485 |
| Loop1 | Nat (a)*25+234 | Eligma | nat (_numberofReturns)*2628+134 |
| Lotterie | 159 | Blocksquareseriea | 286 |
| Enklaven | 268 | Auctusether | 264 |
| Werbung | Inf | gültig | Inf |
SACO färbt eine lineare Grenze für die ersten vier intelligenten Verträge in der obigen Tabelle. Die Grenzen von Smart Contracts blockieren und kryptophoenix hängen vom Wert eines ihrer Felder (dem achten bzw. dritten) ab. Für Smart Contracts Loop1 und Eligma stützen sich die erhaltenen Grenzen auf Argumente einiger seiner Funktionen (A und _NumberofReturns). Falls intelligente Verträge keine Schleife als Lotterie, Blocksquareseriea, Enklaven oder auctusether enthalten, färbt SACO eine konstante Grenze.
Beachten Sie, dass der Analysator aufgrund von Präzisionsbeschränkungen von SACO (keine Bitoperationen und ein Modell zur Funktion SHA3) die Informationen zu Bitvariablen vergisst. Aufgrund dieses Faktors ist SACO nicht in der Lage, auf einige der intelligenten Verträge wie validToken oder Werbung und Renditen inf zu schließen.
Andere hochrangige Analysatoren, die an Zwischenformen wie Integer-Übergangssystemen oder Hornklauseln (z. B. Aprove, T2, SyMax, Cofloco) arbeiten, können ebenfalls leicht an die von Ethir produzierten RBR-Programme angepasst werden.
Wenn Sie interessant sind, Ethir gemeinsam mit SACO-Kontakt-SACO-Entwicklern durch eine Pull-Request oder ein neues Problem zu verwenden.
Sie können hier einen ersten Prototyp ausprobieren. Gastap färbt eine Obergrenze des an jeder Transaktion beteiligten Gases.
