EthIR
1.0.0
Un cadre pour l'analyse de haut niveau de Ethereum Bytecode. Ethir construit un CFG complet et sonore d'un Bytecode Ethereum et génère une représentation basée sur des règles (RBR) du programme. Cette représentation de haut niveau permet l'application d'analyses existantes de haut niveau pour déduire les propriétés du code EVM.
Téléchargez la source de dossier qui contient un exécutable statique de Solidity Compiler.
Ajoutez-le au chemin et testez qu'il est installé.
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
Dans le cas où vous souhaitez installer la dernière version:
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
Un exécutable statique est fourni dans la source du dossier.
Ajoutez OT au chemin et testez qu'il est installé.
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
Dans le cas où vous souhaitez installer la dernière 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
Téléchargez le dossier de code source.
Décompressez le dossier et installez-le.
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
Utilisez la commande pip install pour installer six, demande des bibliothèques Python.
pip install six
pip install requests
Les commandes ci-dessus peuvent échouer en fonction de la version PIP. Si c'est le cas, exécutez la commande suivante au lieu des précédentes.
python -m pip install six
python -m pip install requests
Pour vérifier la version, exécutez la commande pip -V .
Pour exécuter Ethir, exécutez l'une des commandes suivantes à l'intérieur du dossier Ethir :
./oyente-ethir -s file_name.sol
./oyente-ethir -s file_name.evm -b
./oyente-ethir -s file_name.disasm -disasm
La commande ./oyente-ethir -h affiche une liste avec toutes les options disponibles d'Ethir. Certains des plus pertinents sont:
./oyente-ethir -s filename -cfg
./oyente-ethir -s filename -saco
./oyente-ethir -s filename -d
Tous les fichiers générés par Ethir lors de son exécution sont stockés dans le direcrtory / tmp / costabs /.
Une fois Ethir installé, supposons que nous voulons générer le RBR du fichier de démontage blockking.evm.disasm disponible dans les exemples de dossiers. Tout d'abord, nous devons aller au répertoire Ethir et exécuter la commande ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm là-bas.
Pendant l'exécution, Ethir a créé le répertoire / tmp / costabs / où il stocke le RBR associé au fichier blockking.evm.disasm . Si nous inspectons ce répertoire, nous trouvons un fichier nommé rbr.rbr qui contient le RBR. Si nous ouvrons le fichier avec un éditeur commun (GEDIT, EMACS), nous pouvons voir le RBR généré. Vous trouverez ci-dessous un skecth du RBR généré pour Blockking.evm.Disasm Fichier:
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))
Si nous exécutons la commande ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -eop au lieu de celle ci-dessus, le RBR que Ethir produit a des annotations, avec le bytecode EVM entrelacé dans le texte. Vous trouverez ci-dessous un croquis du RBR avec des annotations NOPS générées pour blocking.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 nous permet également de stocker le CFG du fichier analysé. Dans ce cas, nous devons exécuter la commande ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -cfg . Ethir stocke le CFG dans un fichier avec extension .cfg dans le répertoire / tmp / costabs / .
Notez qu'un fichier peut contenir plus d'un contrat intelligent. Dans ce cas, Ethir génère un fichier pour chaque contrat rbr0.rbr, rbr1.rbr, ... rbrn.rbr.
Les exemples de dossiers contient des exemples en cours d'exécution pour tester l'outil. Il existe à la fois des fichiers Solidity, EVM et Disassembly.
La plupart des exemples tels que BlocCking.Evm.Disasm, publicités.sol, validtoken.sol ou cryptophoenix.sol sont des contrats réels obtenus à partir de la blockchain tandis que d'autres tels que Loop1.sol et Sum.sol sont des exemples adhoc où il est plus facile de comprendre le processus de décompilation.
SACO est un analyseur statique pour les objets simultanés qui, est capable de déduire, entre autres propriétés, des limites supérieures sur le nombre d'itérations de boucles. Notez qu'il s'agit de la première étape cruciale pour déduire la consommation de gaz des contrats intelligents.
La représentation interne de SACO correspond à la grammaire du RBR généré par Ethir après des traductions syntaxiques mineures. Grâce à cela, il est capable de prouver la fin des boucles que certains exemples contiennent et produisent une liaison linéaire pour ces boucles. Voici quelques-unes des limites de boucle déduites par SACO pour certains des contrats intelligents contenus dans des exemples de dossiers:
| Contrat intelligent | Lié | Contrat intelligent | Lié |
|---|---|---|---|
| Blocking | Nat (G8 / 10) * 36 + 8934493 | Cryptophoenix | Nat (G3) * 228409344 + 4113285485 |
| Loop1 | nat (a) * 25 + 234 | Éligma | nat (_numberofreturns) * 2628 + 134 |
| Loterie | 159 | Blocksquareserieea | 286 |
| Enclaves | 268 | Auctusher | 264 |
| Publicité | infirme | valide | infirme |
SACO déduit une linéaire à destination des quatre premiers contrats intelligents indiqués dans le tableau ci-dessus. Les limites des contrats intelligents bloquants et Cryptophoenix dépendent de la valeur de l'un de leurs champs (les huitième et troisième respectivement). Pour les contrats intelligents Loop1 et Eligma, les limites obtenues reposent sur les arguments de certaines de ses fonctions (A et _numberofreturns). Dans le cas où les contrats intelligents ne contiennent pas de boucle comme loterie, blocsquareseriea, enclaves ou auctusher, Saco infère une limite constante.
Notez qu'en raison des limites de précision de SACO (il n'a pas de opérations bit et un modèle de fonction SHA3), l'analyseur oublie les informations sur les variables bit. En raison de ce facteur, SACO n'est pas en mesure de déduire un lien pour certains des contrats intelligents tels que ValidToken ou publicités et Renvoie Inf .
D'autres analyseurs de haut niveau qui travaillent sur des formes intermédiaires comme les systèmes de transition entière ou les clauses de corne (par exemple, Aprove, T2, trèsmax, cofloco) pourraient également être facilement adaptés pour travailler sur les programmes traduits par RBR produits par Ethir.
Si vous êtes intéressant à utiliser Ethir conjointement avec SACO Contactez les développeurs SACO via une nouvelle demande ou un nouveau problème.
Vous pouvez essayer un premier prototype ici. Gastap déduit une limite supérieure du gaz impliqué dans chaque transaction.
