EthIR
1.0.0
Un marco para el análisis de alto nivel del bytecodo Ethereum. Ethir construye un CFG completo y sólido de un bytecodo Ethereum y genera una representación basada en reglas (RBR) del programa. Esta representación de alto nivel permite la aplicación de análisis de alto nivel existentes para inferir propiedades del código EVM.
Descargue la fuente de carpetas que contiene un ejecutable estático de compilador de solidez.
Agrégalo a la ruta y pruebe que está instalado.
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
En caso de que desee instalar la última versión:
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
Se proporciona un ejecutable estático en la fuente de la carpeta.
Agregue OT a la ruta y pruebe que está instalado.
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
En caso de que desee instalar la última versión:
sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum
Descargue la carpeta del código fuente.
Descomprima la carpeta e instálela.
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
Use el comando pip install para instalar seis, solicita bibliotecas de Python.
pip install six
pip install requests
Los comandos anteriores pueden fallar según la versión PIP. Si es el caso, ejecute el siguiente comando en lugar de los anteriores.
python -m pip install six
python -m pip install requests
Para verificar la versión, ejecute el comando pip -V .
Para ejecutar ETHIR, ejecute uno de los siguientes comandos dentro de la carpeta ETHIR :
./oyente-ethir -s file_name.sol
./oyente-ethir -s file_name.evm -b
./oyente-ethir -s file_name.disasm -disasm
El comando ./oyente-ethir -h muestra una lista con todas las opciones disponibles de ETHIR. Algunos de los más relevantes son:
./oyente-ethir -s filename -cfg
./oyente-ethir -s filename -saco
./oyente-ethir -s filename -d
Todos los archivos generados por ETHIR durante su ejecución se almacenan en DirecrTory/TMP/Costabs/.
Una vez que se instala ETHIR, supongamos que queremos generar el RBR del archivo de desmontaje en bloque.evm.disasm disponible en los ejemplos de carpetas. Primero, tenemos que ir al directorio Ethir y ejecutar el comando ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm allí.
Durante la ejecución, ETHIR ha creado el directorio /TMP/Costabs/ donde almacena el RBR asociado con el archivo blockking.evm.disasm . Si inspeccionamos este directorio, encontramos un archivo llamado RBR.RBR que contiene el RBR. Si abrimos el archivo con cualquier editor común (GEDIT, EMACS) podemos ver el RBR generado. A continuación se muestra un skecth del RBR generado para blockking.evm.disasm archivo:
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 ejecutamos el comando ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -eop en lugar del anterior, el RBR que produce Ethir tiene anotaciones NOPS, con el bytecodo EVM intercalado en el texto. A continuación se muestra un bosquejo del RBR con anotaciones NOPS generadas para Blockking .
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 también nos permite almacenar el CFG del archivo analizado. En ese caso, tenemos que ejecutar el comando ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -cfg . Ethir almacena el CFG en un archivo con la extensión .cfg en el directorio /tmp/costabs/ .
Tenga en cuenta que un archivo puede contener más de un contrato inteligente. En ese caso, ETHIR genera un archivo por cada contrato RBR0.RBR, RBR1.RBR, ... RBRN.RBR.
Los ejemplos de carpetas contienen ejemplos de ejecución para probar la herramienta. Hay archivos de solidez, EVM y desmontaje.
La mayoría de los ejemplos, como bloccking.evm.disasm, anuncios.sol, validToken.sol o cryptophoenix.sol son contratos del mundo real obtenidos de la cadena de bloques, mientras que otros como Loop1.sol y Sum.sol son ejemplos ad-hoc en los que es más fácil entender el proceso de descompilación.
SACO es un analizador estático para objetos concurrentes que, es capaz de inferir, entre otras propiedades, los límites superiores en el número de iteraciones de los bucles. Tenga en cuenta que este es el primer paso crucial para inferir el consumo de gas de contratos inteligentes.
La representación interna de SACO coincide con la gramática de la RBR generada por ETHIR después de traducciones sintácticas menores. Gracias a esto, es capaz de probar la terminación de los bucles que contienen algunos de los ejemplos y producen un límite lineal para esos bucles. Estos son algunos de los límites de bucle inferidos por SACO para algunos de los contratos inteligentes contenidos en ejemplos de carpetas:
| Contrato inteligente | Atado | Contrato inteligente | Atado |
|---|---|---|---|
| Bloqueo | Nat (G8/10)*36+8934493 | Criptophoenix | NAT (G3)*228409344+4113285485 |
| Bucle1 | nat (a)*25+234 | Elegancia | nat (_numberofreturns)*2628+134 |
| Lotería | 159 | Blocksquareseriea | 286 |
| Enclaves | 268 | Auctusether | 264 |
| Anuncio | inferior | validoso | inferior |
SACO infiere un límite lineal para los primeros cuatro contratos inteligentes que se muestran en la tabla de arriba. Los límites de los contratos inteligentes bloquean y criptophoenix dependen del valor de uno de sus campos (el octavo y el tercero respectivamente). Para Smart Contracts Loop1 y Elegma, los límites obtenidos dependen de los argumentos de algunas de sus funciones (A y _numberOfreturns). En caso de que los contratos inteligentes no contengan ningún bucle como lotería, blocksquareseriea, enclaves o auctusETHER, SACO infiere un límite constante.
Tenga en cuenta que debido a las limitaciones de precisión de SACO (no tiene operaciones de bits y un modelo para la función SHA3), el analizador olvida la información sobre las variables de bits. Debido a este factor, SACO no puede inferir un límite para algunos de los contratos inteligentes, como validToken o publicidad y devoluciones, INF .
Otros analizadores de alto nivel que trabajan en formas intermedias como sistemas de transición enteros o cláusulas de bocina (p. Ej., Aprove, T2, MyMax, CoFloco) podrían adaptarse fácilmente también para trabajar en programas traducidos RBR producidos por ETHIR.
Si te interesa usar ETHIR conjuntamente con los desarrolladores de Saco Contact SACO a través de una solicitud de extracción o un nuevo problema.
Puede probar un primer prototipo aquí. Gastap infiere una parte superior del gas involucrada en cada transacción.
