# SAFEVM: A Safety Verifier for Ethereum Smart Contracts

## TL;DR

SAFEVM is a verification tool for Ethereum smart contracts that leverages C program verification engines to detect vulnerabilities, supporting Solidity and EVM bytecode, and handling array access safety verification.

## Contribution

It introduces SAFEVM, a novel verification approach that adapts C verification engines for Ethereum smart contract safety analysis, including array access verification.

## Key findings

- Successfully verified over 24,000 contracts from Etherscan.
- Effective detection of safety violations in smart contracts.
- Demonstrated compatibility with multiple verification engines.

## Abstract

Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code, or in compiled EVM bytecode), optionally with assert and require verification annotations, and produces in the output a report with the verification results. Besides general safety annotations, SAFEVM handles the verification of array accesses: it automatically generates SV-COMP verification assertions such that C verification engines can prove safety of array accesses. Our experimental evaluation has been undertaken on all contracts pulled from etherscan.io (more than 24,000) by using as back-end verifiers CPAchecker, SeaHorn and VeryMax.