EVMLiSA is a static analyzer based on abstract interpretation for EVM bytecode of smart contracts deployed on Ethereum blockchain and built upon LiSA. Given a EVM bytecode smart contract, EVMLiSA builds a sound and precise control-flow graph of the smart contract.

EVMLiSA is based on peer-reviewed publications:

1. Vincenzo Arceri, Saverio Mattia Merenda, Luca Negrini, Luca Olivieri, Enea Zaffanella. "EVMLiSA: Sound Static Control-Flow Graph Construction for EVM Bytecode". Blockchain: Research and Applications, 2025 (doi: 10.1016/j.bcra.2025.100384).
2. Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella. "Towards a Sound Construction of EVM Bytecode Control-Flow Graphs". In Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2024), co-located with ECOOP 2024 (doi: 10.1145/3678721.3686227).

• Requirements
• Installation
  • Environment Setup
• Execution Methods
  • Using Docker
  • Using CLI
• Options
• The Abstract Stack Set Domain
• Jump Classification
• Usage Example
  • Example Output
• EVMLiSA as a Library

To build and run EVMLiSA, you will need:

• JDK 11 or higher (optional when using Docker)
• Gradle 8.0 or higher (optional when using Docker)
• Etherscan API key

1. Clone the repository:

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

2. (Optional) Import the project into Eclipse or IntelliJ as a Gradle project.

Before running EVMLiSA, you must configure your Etherscan API key:

1. Create a .env file in the project root directory.
2. Add the following line to the file:

   ETHERSCAN_API_KEY=<your_etherscan_api_key> 

3. Replace <your_etherscan_api_key> with your actual key from Etherscan.

Alternatively, you can pass your API key directly using the --etherscan-api-key <key> option when executing the analyzer.

1. Build the Docker container:

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

2. Run EVMLiSA with Docker:

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

   • -v $(pwd)/.env:/app/.env: Mounts your environment file
   • -v $(pwd)/execution/docker:/app/execution/results: Shares the results directory

1. Build the project:

   ./gradlew assemble

2. Run EVMLiSA:

   java -jar build/libs/evm-lisa-all.jar [options]

Options: -a,--address <arg> Address of an Ethereum smart contract. --abi <arg> ABI of the bytecode to be analyzed (JSON format). --abi-path <arg> Filepath of the ABI file. -b,--bytecode <arg> Bytecode to be analyzed (e.g., 0x6080...). --benchmark <arg> Filepath of the benchmark. --bytecode-path <arg> Filepath of the bytecode file. -c,--cores <arg> Number of cores used in benchmark. --checker-all Enable all security checkers. --checker-reentrancy Enable reentrancy checker. --checker-timestampdependency Enable timestamp-dependency checker. --checker-txorigin Enable tx-origin checker. --etherscan-api-key <arg> Insert your Etherscan API key. --link-unsound-jumps-to-all-jumpdest Link all unsound jumps to all jumpdest. --output-directory-path <arg> Filepath of the output directory. --show-all-instructions-in-cfg Show all instructions in the CFG representation. --stack-set-size <arg> Dimension of stack-set (default: 8). --stack-size <arg> Dimension of stack (default: 32). --use-live-storage Use the live storage in SLOAD. 

In analyzing EVM bytecode programs, EVMLiSA employs a domain of sets of abstract stacks to enhance precision, particularly for code containing loops.

The analyzer introduces the abstract stack powerset domain $\texttt{SetSt}_{k,h,l}$ consisting of sets of abstract stacks with at most $l$ elements and a maximum height of $h$. This domain allows the analyzer to maintain collections of abstract stacks, avoiding the need to compute the least upper bound (lub) and allowing each element of an abstract stack to be a $k$ integer set.

EVMLiSA classifies jump instructions in the following categories:

• Resolved: All destinations of the jump node have been successfully resolved
• Definitely unreachable: The jump node is unreachable (reached with the bottom abstract state)
• Maybe unreachable: The jump node is not reachable from the entry point, but may be reachable via a potentially unsound jump node
• Unsound: The jump node is reached with a stack containing an unknown numerical value that may correspond to a valid jump destination
• Maybe unsound: The stack set exceeded the maximum configured stack size

Analyze a smart contract with specific configuration parameters:

Using Command Line:

java -jar build/libs/evm-lisa-all.jar \ -a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B \ --stack-size 64 \ --stack-set-size 10 \ --link-unsound-jumps-to-all-jumpdest

Using 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 \ --link-unsound-jumps-to-all-jumpdest

Tip: Use docker run -a stderr to output only the JSON report to standard output.

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

EVMLiSA can be integrated as a Java library to analyze EVM smart contracts programmatically:

// Analyze by contract address EVMLiSA.analyzeContract(new SmartContract("0x123456...")); // Analyze from bytecode file path EVMLiSA.analyzeContract(new SmartContract(Path.of("bytecode", "code.bytecode"))); // Analyze from bytecode string EVMLiSA.analyzeContract(new SmartContract().setBytecode("0x6080...")); // Analyze multiple contracts EVMLiSA.analyzeSetOfContracts(Path.of("list-of-contracts.txt"));