evm lisa

EVMLISA: Um analisador estático abstrato baseado em interpretação para EVM bytecode

O EVMLISA é um analisador estático baseado na interpretação abstrata do bytecode de EVM de contratos inteligentes implantados no Ethereum Blockchain e construído em Lisa. Dado um contrato Smart EVM ByteCode, a EVMLISA cria um gráfico de fluxo de controle sólido e preciso do contrato inteligente.

EVMLISA é baseado na publicação revisada por pares

Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella. "Em direção a uma construção sólida de gráficos de controle de controle de bytecode EVM" . Em Anais do 26º Workshop Internacional da ACM, sobre técnicas formais para programas do tipo Java (FTFJP 2024), co-localizados com a ECOOP 2024.

? Construindo Evmlisa

Compilar Evmlisa requer:

• Jdk> = 11
• Gradle> = 6.6
• Chave da API EtherScan

Você precisa:

• Clone o repositório:

  git clone https://github.com/lisa-analyzer/evm-lisa.git
  cd evm-lisa

• Importe o projeto para o espaço de trabalho Eclipse/Intellij como um projeto gradle (opcional).

Executando o EVMLISA

Antes de executar o EVMLISA, verifique se você configurou uma variável de ambiente com a chave da API EtherScan. Siga as etapas abaixo para configurar a variável do ambiente:

1. Comece criando um arquivo chamado .env no projeto EVMLISA.
2. Dentro do arquivo .env , adicione a seguinte linha:

 ETHERSCAN_API_KEY=<your_etherscan_api_key>

3. Substitua <your_etherscan_api_key> pela sua chave de API EtherScan.

Aqui você pode descobrir como gerar uma chave de API éstrescan.

Depois de configurar a variável de ambiente, você pode executar o EVMLISA via Docker ou via Bash.

Via Docker

Construa o contêiner:

 mkdir -p execution/docker &&
docker build -t evm-lisa:latest .

Então você pode executar o EVMLISA com:

 docker run --rm -it 
-v $(pwd)/.env:/app/.env 
-v $(pwd)/execution/docker:/app/execution/results 
evm-lisa:latest 
-a <smart_contract_address> [options]

• -v $(pwd)/.env:/app/.env : Monte o arquivo .env .
• -v $(pwd)/execution/docker:/app/execution/results : compartilhe a pasta dos resultados.

Substitua <smart_contract_address> pelo endereço do contrato inteligente Ethereum que você deseja analisar.

Via Bash

Construa o projeto:

./gradlew build

Crie Zip de distribuição:

./gradlew distZip

Descompactar a distribuição:

unzip build/distributions/evm-lisa.zip -d execution

Então você pode executar o EVMLISA com:

./execution/evm-lisa/bin/evm-lisa 
-a < smart_contract_address > [options]

Substitua <smart_contract_address> pelo endereço do contrato inteligente Ethereum que você deseja analisar.

Este comando iniciará o processo de análise para o contrato inteligente especificado, fornecendo insights e resultados com base no bytecode EVM do contrato.

 Options:
 -a,--address <arg>          address of an Ethereum smart contract
 -b,--benchmark <arg>        filepath of the benchmark suite (i.e., a list of smart contract addresses)
 -C,--cores <arg>            number of cores to use
 -c,--dump-cfg               dump the CFG
 -d,--dump-analysis <arg>    dump the analysis (html, dot)
 -D,--download-bytecode      download the bytecode, without analyzing it
 -f,--filepath <arg>         filepath of an EVM bytecode smart contract
 -o,--output <arg>           output directory path
 -q,--stack-size <arg>       maximal height of stack
 -s,--dump-stats             dump statistics
 -S,--use-live-storage       use the live storage in SLOAD
 -w,--stack-set-size <arg>   maximal size of stack sets

? Domínio de conjunto de pilha abstrato

Na análise dos programas EVM ByteCode, a EVMLISA emprega um domínio de conjuntos de pilhas abstratas para melhorar a precisão, principalmente quando os loops são encontrados no código -fonte.

Evmlisa apresenta o domínio do Powerset de pilha abstrato $ texttt {setSt} _ {k, h, l} $ que consiste em conjuntos de pilhas abstratas com no máximo $ L $ elementos e uma altura no máximo $ h $ . Este domínio permite que o analisador mantenha coleções de pilhas abstratas, evitando a necessidade de calcular o lubrificante e permitir que cada elemento de uma pilha abstrata seja um $ k $ conjunto inteiro.

? Exemplo de execução

Aqui está um exemplo de como executar o EVMLISA. Neste exemplo, analisaremos um contrato inteligente no endereço 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B com opções específicas para tamanho de pilha, tamanho de pilha, uso de armazenamento ao vivo e dump do CFG:

• Bash:

./execution/evm-lisa/bin/evm-lisa 
-a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B 
--stack-size 64 
--stack-set-size 10 
--dump-stats 
--use-live-storage

• Docker:

docker run --rm -it 
-v $( pwd ) /.env:/app/.env 
-v $( pwd ) /execution/docker:/app/execution/results 
evm-lisa:latest 
-a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B 
--stack-size 64 
--stack-set-size 10 
--dump-stats 
--use-live-storage

Use docker run -a stderr para despejar apenas o relatório JSON como saída padrão.

A saída esperada é a seguinte:

 # #############
Total opcodes : 344
Total jumps : 45
Resolved jumps : 44
Definitely unreachable jumps : 1
Maybe unreachable jumps : 0
Unsound jumps : 0
Maybe unsound jumps : 0
# #############

Classificação de salto

• Resolvido : Todos os destinos do nó de salto foram resolvidos;
• Definitivamente inacessível : o nó do salto é inacessível (ou seja, é alcançado com o estado abstrato inferior);
• Talvez inacessível : o nó de salto não é acessível no CFG, começando a partir de seu ponto de entrada, mas pode ser alcançado por meio de um nó de salto (talvez) dono (se houver);
• Dono : o nó de salto é atingido pelo menos com uma pilha com um valor numérico desconhecido que pode corresponder a um destino de salto válido como o elemento superior;
• Talvez doentio : o conjunto da pilha excedeu o tamanho máximo da pilha.

---

Colaboradores