EthIR
1.0.0
Uma estrutura para análise de alto nível do bytecode Ethereum. Ethir cria um CFG completo e sólido de um bytecode Ethereum e gera uma representação baseada em regras (RBR) do programa. Essa representação de alto nível permite a aplicação de análises de alto nível existentes para inferir as propriedades do código EVM.
Faça o download da fonte da pasta que contém um executável estático do Solity Compiler.
Adicione -o ao caminho e teste que ele está instalado.
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
Caso você queira instalar a versão mais recente:
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
Um executável estático é fornecido na fonte da pasta.
Adicione OT ao caminho e teste que ele está instalado.
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
Caso você queira instalar a versão mais recente:
sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum
Faça o download da pasta de código -fonte.
Descompacte a pasta e instale -a.
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 o comando pip install para instalar seis, solicita bibliotecas python.
pip install six
pip install requests
Os comandos acima podem falhar dependendo da versão pip. Se for o caso, execute o seguinte comando em vez dos anteriores.
python -m pip install six
python -m pip install requests
Para verificar a versão, execute o comando pip -V .
Para executar o Ethir, execute um dos seguintes comandos dentro da pasta Ethir :
./oyente-ethir -s file_name.sol
./oyente-ethir -s file_name.evm -b
./oyente-ethir -s file_name.disasm -disasm
O comando ./oyente-ethir -h exibe uma lista com todas as opções disponíveis do ethir. Alguns dos mais relevantes são:
./oyente-ethir -s filename -cfg
./oyente-ethir -s filename -saco
./oyente-ethir -s filename -d
Todos os arquivos gerados pelo ETHIR durante sua execução são armazenados no diretor/tmp/costabs/.
Depois que o Ethir estiver instalado, suponha que queremos gerar o RBR do arquivo de desmontagem bloqueando.evm.disaSasmo disponível nos exemplos de pastas. Primeiro, temos que ir ao diretório Ethir e executar o comando ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm lá.
Durante a execução, a Ethir criou o diretório /tmp/costabs/ onde armazena o RBR associado ao arquivo bloqueador.evm.disasm . Se inspecionarmos este diretório, encontramos um arquivo chamado RBR.RBR que contém o RBR. Se abrirmos o arquivo com qualquer editor comum (GEDIT, EMACS), podemos ver o RBR gerado. Abaixo está um skecth do RBR gerado para bloquear .
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))
Se executarmos o comando ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -eop em vez do acima, o RBR que a Ethir produz tem anotações, com o EVM bytecode intercodo no texto. Abaixo está um esboço do RBR com anotações NOPs geradas para bloquear .
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 também nos permite armazenar o CFG do arquivo analisado. Nesse caso, temos que executar o comando ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -cfg . Ethir armazena o CFG em um arquivo com extensão .cfg no diretório /tmp/costabs/ .
Observe que um arquivo pode conter mais de um contrato inteligente. Nesse caso, a Ethir gera um arquivo de acordo com cada contrato rbr0.rbr, rbr1.rbr, ... rbrn.rbr.
Os exemplos de pasta contêm exemplos de execução para testar a ferramenta. Existem arquivos de solidez, EVM e desmontagem.
A maioria dos exemplos como Bloccking.EVM.DisaM, publicidade.sol, ValidToken.sol ou Cryptophoenix.sol são contratos do mundo real obtidos da blockchain, enquanto outros como Loop1.sol e Sum.Sol são exemplos ad-hoc, onde é mais fácil entender o processo de decomposição.
O Saco é um analisador estático para objetos simultâneos que, é capaz de inferir, entre outras propriedades, limites superiores no número de iterações de loops. Observe que esta é a primeira etapa crucial para inferir o consumo de gás de contratos inteligentes.
A representação interna do SACO corresponde à gramática do RBR gerada por Ethir após traduções sintáticas menores. Graças a isso, é capaz de provar o término dos loops que alguns dos exemplos contêm e produzem um limite linear para esses loops. Aqui estão alguns dos limites de loop inferidos por Saco para alguns dos contratos inteligentes contidos nos exemplos de pastas:
| Contrato inteligente | Vinculado | Contrato inteligente | Vinculado |
|---|---|---|---|
| Bloqueando | Nat (G8/10)*36+8934493 | Cryptophoenix | NAT (G3)*228409344+4113285485 |
| Loop1 | nat (a)*25+234 | Elegma | Nat (_NumberOfReturns)*2628+134 |
| Loteria | 159 | Blocksquareseriea | 286 |
| Enclaves | 268 | AUCTUSTHERTH | 264 |
| Anúncio | inf | ValidToken | inf |
O SACO infere um limite linear para os quatro primeiros contratos inteligentes mostrados na tabela acima. Os limites dos contratos inteligentes bloqueando e Cryptophoenix dependem do valor de um de seus campos (o oitavo e o terceiro, respectivamente). Para contratos inteligentes Loop1 e elegma, os limites obtidos dependem de argumentos de algumas de suas funções (A e _NumberOfreTurns). Caso os contratos inteligentes não contenham nenhum loop como loteria, Blocksquareseriea, enclaves ou Auctusether, o Saco infere um limite constante.
Observe que, devido às limitações de precisão do SACO (ele não possui operações de bits e um modelo para a função sha3), o analisador esquece as informações sobre as variáveis de bits. Devido a esse fator, o SACO não é capaz de inferir um limite para alguns dos contratos inteligentes, como ValidToken ou Anúncio e Retorna Inf .
Outros analisadores de alto nível que trabalham em formas intermediárias, como sistemas de transição inteira ou cláusulas de buzina (por exemplo, APROVE, T2, IURMAX, COFLOCO) podem ser facilmente adaptadas também para trabalhar em programas traduzidos RBR produzidos por Ethir.
Se você é interessante em usar o Ethir em conjunto com os desenvolvedores do Saco, entre em contato com uma solicitação puxada ou uma nova edição.
Você pode tentar um primeiro protótipo aqui. Gastap infere um limite superior do gás envolvido em cada transação.
