Descargar evm lisa - Descargar el código fuente de evm lisa

evm lisa

Otras categorias

1.0.0

Descargar

Evmlisa: un analizador estático basado en la interpretación abstracta para EVM Bytecode

EVMLISA es un analizador estático basado en la interpretación abstracta para EVM Bytecode of Smart Contracts implementados en Ethereum Blockchain y construido sobre LISA. Dado un contrato Smart ByTecode EVM, Evmlisa construye un gráfico de flujo de control sólido y preciso del contrato inteligente.

Evmlisa se basa en la publicación revisada por pares

Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella. "Hacia una construcción de sonido de los gráficos de flujo de control Bytecode EVM" . En Actas del 26º Taller Internacional de ACM sobre técnicas formales para programas similares a Java (FTFJP 2024), ubicado en Ecoop 2024.

? Construyendo Evmlisa

Compilar Evmlisa requiere:

Jdk> = 11
Gradle> = 6.6
Clave de la API de Esterscan

Necesitas:

Clon el repositorio:

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

Importe el proyecto en el espacio de trabajo Eclipse/IntelliJ como un proyecto de Gradle (opcional).

Ejecutando evmlisa

Antes de ejecutar EVMLISA, asegúrese de haber configurado una variable de entorno con su clave API Esterscan. Siga los pasos a continuación para configurar la variable de entorno:

Comience creando un archivo llamado .env en el proyecto Evmlisa.
Dentro del archivo .env , agregue la siguiente línea:

 ETHERSCAN_API_KEY=<your_etherscan_api_key>

Reemplace <your_etherscan_api_key> con su tecla API Esterscan.

Aquí puede encontrar cómo generar una clave API de Esterscan.

Una vez que haya configurado la variable de entorno, puede ejecutar Evmlisa a través de Docker o a través de Bash.

Via Docker

Construya el contenedor:

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

Entonces puedes ejecutar Evmlisa con:

 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 el archivo .env .
-v $(pwd)/execution/docker:/app/execution/results : comparte la carpeta de resultados '.

Reemplace <smart_contract_address> con la dirección del contrato Smart Ethereum que desea analizar.

Vía Bash

Construye el proyecto:

./gradlew build

Crear distribución zip:

./gradlew distZip

Descomprima la distribución:

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

Entonces puedes ejecutar Evmlisa con:

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

Reemplace <smart_contract_address> con la dirección del contrato Smart Ethereum que desea analizar.

Este comando iniciará el proceso de análisis para el contrato inteligente especificado, proporcionando información y resultados basados en el código de bytes EVM del 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

? Dominio de conjunto de pila abstracta

En el análisis de los programas ByTecode EVM, EVMLISA emplea un dominio de conjuntos de pilas abstractas para mejorar la precisión, particularmente cuando se encuentran bucles en el código fuente.

Evmlisa presenta el dominio de PowerSet de pila abstracta $ texttt {setst} _ {k, h, l} $ que consiste en conjuntos de pilas abstractas con la mayoría $ L $ elementos y una altura de la mayoría $ H $ . Este dominio permite que el analizador mantenga colecciones de pilas abstractas, evitando la necesidad de calcular el lub y permitiendo que cada elemento de una pila abstracta sea un $ K $ Conjunto de enteros.

? Ejemplo de ejecución

Aquí hay un ejemplo de cómo ejecutar Evmlisa. En este ejemplo, analizaremos un contrato inteligente en la dirección 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B con opciones específicas para el tamaño de la pila, el tamaño del conjunto de pilas, el uso de almacenamiento en vivo y el volcado del CFG:

Intento:

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

Estibador:

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 descargar solo el informe JSON como salida estándar.

La salida esperada es la siguiente:

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

Clasificación de salto

Resuelto : todos los destinos del nodo de salto se han resuelto;
Definitivamente inalcanzable : el nodo de salto es inalcanzable (es decir, se alcanza con el estado abstracto inferior);
Tal vez inalcanzable : el nodo de salto no es accesible en el CFG, comenzando desde su punto de entrada, pero puede ser accesible a través de un nodo de salto (tal vez) no sólido (si corresponde);
No sospechoso : el nodo de salto se alcanza al menos con una pila con un valor numérico desconocido que puede corresponder a un destino de salto válido como el elemento superior;
Tal vez no sólido : el conjunto de pila excedió el tamaño máximo de la pila.