# A Semantic Framework for the Security Analysis of Ethereum smart contracts

arXiv: https://arxiv.org/abs/1802.08660 · HTML: https://mlsanity.com/paper/1802.08660/

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Feb 2018.

## Built on by (most cited first, 16 of 16)

- [Combining Graph Neural Networks with Expert Knowledge for Smart Contract Vulnerability Detection](https://mlsanity.com/paper/2107.11598/) (2021)
- [Smart Contract Vulnerability Detection: From Pure Neural Network to Interpretable Graph Feature and Expert Pattern Fusion](https://mlsanity.com/paper/2106.09282/) (2021)
- [Eth2Vec: Learning Contract-Wide Code Representations for Vulnerability Detection on Ethereum Smart Contracts](https://mlsanity.com/paper/2101.02377/) (2021)
- [Usenix'23 Extended Version: Smart Learning to Find Dumb Contracts](https://mlsanity.com/paper/2304.10726/) (2023)
- [CodeBC: A More Secure Large Language Model for Smart Contract Code Generation in Blockchain](https://mlsanity.com/paper/2504.21043/) (2025)
- [SINGA-Easy: An Easy-to-Use Framework for MultiModal Analysis](https://mlsanity.com/paper/2108.02572/) (2021)
- [VisualTextRank: Unsupervised Graph-based Content Extraction for Automating Ad Text to Image Search](https://mlsanity.com/paper/2108.02725/) (2021)
- [Text is NOT Enough: Integrating Visual Impressions into Open-domain Dialogue Generation](https://mlsanity.com/paper/2109.05778/) (2021)
- [Discovering Personalized Semantics for Soft Attributes in Recommender Systems using Concept Activation Vectors](https://mlsanity.com/paper/2202.02830/) (2022)
- [Reinforced MOOCs Concept Recommendation in Heterogeneous Information Networks](https://mlsanity.com/paper/2203.11011/) (2022)
- [Explanation-Guided Fairness Testing through Genetic Algorithm](https://mlsanity.com/paper/2205.08335/) (2022)
- [Using Graph Neural Networks for Program Termination](https://mlsanity.com/paper/2207.14648/) (2022)
- [Tribe or Not? Critical Inspection of Group Differences Using TribalGram](https://mlsanity.com/paper/2303.09664/) (2023)
- [A Survey on Blockchain-based Supply Chain Finance with Progress and Future directions](https://mlsanity.com/paper/2408.08915/) (2024)
- [Tailored Prompts, Targeted Protection: Vulnerability-Specific LLM Analysis for Smart Contracts](https://mlsanity.com/paper/2605.03697/) (2026)
- [Benchmarking LLM-Based Static Analysis for Secure Smart Contract Development: Reliability, Limitations, and Potential Hybrid Solutions](https://mlsanity.com/paper/2605.11163/) (2026)

## Abstract (arXiv)

Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of smart contracts, it is of paramount importance to formalize their semantics as well as the security properties of interest, in particular at the level of the bytecode being executed. In this paper, we present the first complete small-step semantics of EVM bytecode, which we formalize in the F* proof assistant, obtaining executable code that we successfully validate against the official Ethereum test suite. Furthermore, we formally define for the first time a number of central security properties for smart contracts, such as call integrity, atomicity, and independence from miner controlled parameters. This formalization relies on a combination of hyper- and safety properties. Along this work, we identified various mistakes and imprecisions in existing semantics and verification tools for Ethereum smart contracts, thereby demonstrating once more the importance of rigorous semantic foundations for the design of security verification techniques.