evm lisa Téléchargement - evm lisa Source Téléchargement du code

evm lisa

Autres catégories

1.0.0

Télécharger

EVMLISA: Un analyseur statique basé sur l'interprétation abstrait pour EVM Bytecode

EVMLISA est un analyseur statique basé sur l'interprétation abstraite pour les bytecode EVM des contrats intelligents déployés sur Ethereum Blockchain et construit sur Lisa. Étant donné un contrat intelligent EVM Bytecode, EVMLISA construit un graphique de contrôle de contrôle sonore et précis du contrat intelligent.

Evmlisa est basé sur la publication évaluée par des pairs

Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella. "Vers une construction sonore de graphiques de flux de contrôle Bytecode EVM" . Dans les actes du 26e atelier international ACM sur les techniques formelles pour les programmes de type Java (FTFJP 2024), colocalisé avec ECOOP 2024.

? Bâtiment evmlisa

La compilation d'Evmlisa nécessite:

Jdk> = 11
Gradle> = 6,6
Clé API Etherscan

Vous devez:

Clone le référentiel:

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

Importez le projet dans l'espace de travail Eclipse / IntelliJ en tant que projet Gradle (facultatif).

Running Evmlisa

Avant d'exécuter EVMLISA, assurez-vous d'avoir configuré une variable d'environnement avec votre clé API EthersCan. Suivez les étapes ci-dessous pour configurer la variable d'environnement:

Commencez par créer un fichier nommé .env dans le projet EVMLISA.
À l'intérieur du fichier .env , ajoutez la ligne suivante:

 ETHERSCAN_API_KEY=<your_etherscan_api_key>

Remplacez <your_etherscan_api_key> par votre clé API Etherscan.

Ici, vous pouvez trouver comment générer une clé API Etherscan.

Une fois que vous avez configuré la variable d'environnement, vous pouvez exécuter EVMLISA via Docker ou via Bash.

Via Docker

Construisez le conteneur:

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

Ensuite, vous pouvez exécuter Evmlisa avec:

 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 : montez le fichier .env .
-v $(pwd)/execution/docker:/app/execution/results : partagez le dossier des résultats.

Remplacez <smart_contract_address> par l'adresse du contrat Smart Ethereum que vous souhaitez analyser.

Via bash

Construisez le projet:

./gradlew build

Créer un zip de distribution:

./gradlew distZip

Décomposer la distribution:

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

Ensuite, vous pouvez exécuter Evmlisa avec:

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

Remplacez <smart_contract_address> par l'adresse du contrat Smart Ethereum que vous souhaitez analyser.

Cette commande lancera le processus d'analyse du contrat intelligent spécifié, fournissant des informations et des résultats basés sur le code EVM du contrat.

 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

? Domaine de set de pile abstrait

Dans l'analyse des programmes EVM Bytecode, EVMLISA utilise un domaine d'ensembles de piles abstraites pour améliorer la précision, en particulier lorsque des boucles sont rencontrées dans le code source.

Evmlisa présente le domaine de la Power PowerSet abstrait $ texttt {setst} _ {k, h, l} $ qui consiste en ensembles de piles abstraites avec au plus $ l $ éléments et une hauteur au plus $ h $ . Ce domaine permet à l'analyseur de maintenir des collections de piles abstraites, en évitant la nécessité de calculer le lub et de permettre à chaque élément d'une pile abstraite d'être un $ k $ Ensemble entier.

? Exemple de course

Voici un exemple de la façon d'exécuter Evmlisa. Dans cet exemple, nous analyserons un contrat intelligent à l'adresse 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B avec des options spécifiques pour la taille de la pile, la taille de la pile, l'utilisation de stockage en direct et le vidage du CFG:

Frapper:

./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

Utilisez docker run -a stderr pour vider uniquement le rapport JSON comme sortie standard.

La sortie attendue est la suivante:

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

Classification de saut

Résolu : toutes les destinations du nœud de saut ont été résolues;
Certainement inaccessible : le nœud de saut est inaccessible (c'est-à-dire qu'il est atteint avec l'état abstrait inférieur);
Peut-être inaccessible : le nœud de saut n'est pas accessible dans le CFG, à partir de son point d'entrée, mais il peut être accessible via un (peut-être) un nœud de saut (le cas échéant);
Usinaire : le nœud de saut est atteint au moins avec une pile avec une valeur numérique inconnue qui peut correspondre à une destination de saut valide comme élément supérieur;
Peut-être un peu : l'ensemble de pile a dépassé la taille maximale de la pile.