YulTracer

YulTracer is a bounded safety checker (finds assertion violations) and interpreter for Yul. YulTracer performs reachability analysis for programs written in Yul and is also able to analyse smart contracts written in Solidity via the Solidity compiler --- we provide examples in this repository showing automatic tool-chains set up to analyse large code bases.

YulTracer is intended for semi-automatic use by developers and auditors. It automatically explores possible executions and detects a range of runtime failures, including failed value transfers due to insufficient balance. Users can additionally specify project-specific safety properties with assertions, and may configure exploration parameters for larger or more complex projects.

---

Table of Contents

• Releases
  • Current Release (0.2.x)
  • Previous Release (0.1.x)
• Testing
• Usage
• Compilation
  • 1. Installing the OCaml Package Manager opam
    • Ubuntu
    • Fedora, CentOS and RHEL
    • macOS
  • 2. Initialising opam
  • 3. Installing Dependencies
  • 4. Compiling YulTracer
• Directory Structure:
• EVM Dialect and Instruction Set
  • Custom Instructions
  • Print Instructions

---

Releases

Current Release (0.2.x)

DOI: 10.5281/zenodo.19868351
Report: arXiv:2512.22417

The 0.2.x release series introduces an attacker/environment model, based on Game Semantics, that drives YulTracer’s trace exploration. This model represents the possible interactions between external users and the contracts under analysis, allowing the tool to enumerate all reachable traces within a user-provided exploration bound. The current 0.2.1 release improves the analysis pipeline and scripts, and includes several bug fixes.

During analysis, YulTracer performs an on-the-fly bounded reachability analysis over the Game Semantics model of the analysed contracts. It constructs a finite exploration tree, corresponding to an unfolding of the interaction LTS, and reports a counterexample trace whenever an assertion-violating configuration is reachable within the explored depth.

Subject to the exploration bound and the fidelity of our Yul interpreter and EVM model, YulTracer is sound and complete for trace enumeration: counterexample traces are not introduced by over-approximate trace generation. The Yul interpreter implements a CEK machine based on our formal small-step operational semantics for Yul (see 10.1007/978-3-031-77382-2_19). The EVM model is a line-by-line port of the Shanghai fork of the Ethereum Execution Client Specifications, extended with symbolic execution and abstracted for compatibility with Yul and the Game Semantics model.

Symbolic execution is currently supported only in a limited form, via Z3 BitVectors. Symbolic reasoning is implemented for arithmetic and branching, but not for symbolic pointers. Consequently, symbolic execution is not recommended at this stage and is not used in any of the smart contract use-case examples provided in this repository.

Previous Release (0.1.x)

DOI: 10.5281/zenodo.12511493
Publication: 10.1007/978-3-031-77382-2_19

For the previous interpreter-only version 0.1 of YulTracer, please see commit 57f9202 and release 0.1.1.

---

Testing

Provided under YulTracer/test/ are two directories:

• smart_contracts: Contains directories documenting our application of YulTracer to various real-world on-chain smart contracts exploits and benchmarks from literature. Each subdirectory contains its own README file explaining how to compile and run the examples:
  • gigahorse-bench/ --- Gigahorse benchmarks with tool comparison scripts
  • DAO/ --- Seven analysis variants of the original on-chain DAO contracts
  • BurgerSwap/ --- BurgerSwap/DemaxPair exploit demo
  • Lendf.Me/ --- dForce Lendf.Me exploit analysis
  • PredyPool/ --- Predy Finance exploit analysis
  • SmartShot_listing1/ --- SmartShot paper Listing 1 example
• yul_tests: Contains tests from the previous release written in Yul to test the interpreter.

Usage

For a step-by-step guide on setting up a new project to analyse Solidity smart contracts, see GUIDE.md.

To run YulTracer on a given program, use the -i option (within the tool directory tree):

dune exec -- yult -i <target-path>.yul

This compiles the project and runs the resulting binary with option -i <path>.yul, which evaluates the target program without running any games. For games (and safety analysis), we use the -g option, which enables games, together with the -abi option, which defines the set methods to explore. For more help on the options available, use the -help or --help option.

In practice, we use previously prepared scripts in project directories (especially for large complex projects) to automatically compile Solidity sources, link the resulting Yul objects that need linking, and provide other necessary options (like ABI and exploration parameters). See the test/smart_contracts directory for examples.

Compilation

To compile YulTracer, if you have all dependencies, run:

dune build

The dependencies are:

• Opam package manager (+initialisation)
• OCaml 4.10+ compiler (up to 4.14.2 for stable hashing of hardcoded addresses)
• Dune build system for OCaml projects
• Menhir parser generator
• Z3 package for OCaml bindings
• Zarith package for arbitrary-precision integers
• Yojson and ppx_deriving_yojson

All the above dependencies can be obtained from Opam package manager after setting up Opam. For more detailed instructions, the instructions below were tested on Linux and macOS. For Windows, we have tested the Ubuntu instructions on WSL (Ubuntu) under Windows 11 and observed no unexpected behaviour. For native Windows support, please refer to the official OCaml website. We were unable to build Z3 natively on Windows through Opam+Cygwin; at present, this seems to require manually compiling Z3 with OCaml bindings.

1. Installing the OCaml Package Manager opam

All dependencies are obtainable through OCaml's official package manager opam. Installation of opam is system specific so you may need to refer to their website linked above. Instructions for some common systems are listed below:

Ubuntu

add-apt-repository ppa:avsm/ppa
apt update
apt install opam

Fedora, CentOS and RHEL

dnf install opam

macOS

# Homebrew
brew install gpatch
brew install opam

# MacPort
port install opam

2. Initialising opam

opam needs to be set up after installation, which may also be system dependent. First one needs to initialise it:

opam init

After initialisation, one has to create the switch to a specific compiler. Any version 4.10 and over works. The command below uses 4.10.1, but one can use the latest version listed.

opam switch create 4.10.1

If this does not work, it could be because opam is missing a dependency. This depends on how minimal the installation of the system is. Check the error messages to know what is missing. From our experience, these are the dependencies typically missing for a fresh installation of Ubuntu:

apt install build-essential
apt install gcc
apt install bubblewrap

The above correspond to make, gcc and bwrap, which are often missing in fresh installations.

Finally, initialising opam updates your ~/.profile file, so you may have to source it on Linux:

source ~/.profile

3. Installing Dependencies

With opam set up, installing dependencies becomes very easy.

opam install dune
opam install menhir
opam install zarith
opam install z3
opam install yojson
opam install ppx_deriving_yojson

Note that Z3 takes a long time to install.

4. Compiling YulTracer

With all dependencies installed and ~/.profile sourced, call the build system:

dune build

This produces an executable binary yult.exe usually located at _build/default/bin/.

Directory Structure:

This project has the following directory structure. This may change in the future.

YulTracer/
├── bin/     # contains main file; produces the executable
├── lib/     # contains implementation of Yul interpreter, EVM and Games
└── test/    # contains our smart contract tests and yul tests.

A typical project directory in our tests has the following structure:

<project-name>/
├── abi/     # contains ABI (.json) files for the project
├── scripts/ # contains scripts for pre-/post-compilation processing
├── src/     # contains Solidity (.sol) source files
└── Makefile # stages the compilation, processing scripts, and runs YulTracer

A README is provided with each example.

---

EVM Dialect and Instruction Set

Provided in this repository is a partial implementation of the EVM based on the Shanghai update of the EVM execution specifications. This means the tool supports EVM behaviours up to, without including, the addition of transient storage.

The following opcode categories are implemented:

Category	Instructions
Arithmetic	add, sub, mul, div, sdiv, mod, smod, addmod, mulmod, exp, signextend
Bitwise	and, or, xor, not, byte, shl, shr, sar
Block	coinbase1, timestamp, chainid1, number1, gaslimit1
Comparison	lt, gt, slt, sgt, eq, iszero
Control-flow	stop, pc1, gas
Data2	datasize3, dataoffset3, datacopy3
Environment	address, caller, codesize, callvalue, codecopy, calldataload, calldatasize, balance, calldatacopy, returndatasize, returndatacopy, extcodesize, WAIT4, MK_SYMBOL4, EXT_FUND4
Immutable2	setimmutable3, loadimmutable3
Keccak	keccak
Linker2	SETLINKER4, linkersymbol3
Log	log11, log21, log31, log41
Memory	mload, mstore, mstore8, msize, memoryguard3
Stack	pop1
Storage	sload, sstore
System	revert1, return, call, staticcall, delegatecall, create, create2, START_ANALYSIS4/LAUNCH_OPPONENT4, IMPERSONATECALL4, REVEAL_UINT4, REVEAL_ADDR4
Print2	PRINT3, PRINT_signed3, PRINT_HEX3, PRINT_hex3, PRINT_bin3, PRINT_object3, PRINT_IDS3, PRINT_names3, PRINT_sigma3, PRINT_z33, PRINT_mem3, PRINT_ascii3

¹ Instructions with simpler or dummy implementations.
² Unofficial instruction categories needed for Yul.
³ Official Yul-only instructions that are not part of the EVM specs.
⁴ Custom YulTracer-only instructions in all-caps.

Data, Immutable and Linker are unofficial categories added to support official instructions specified only in the Yul documentation. These Yul-only instructions are not part of the EVM specification, but are still necessary to analyse real-world Yul objects (in particular, those produced by the Solidity compiler). Since the semantics of these instructions is not formally specified, their behaviour was inferred from the documentation. Additionally, some instructions were not compatible with Yul or not necessary for safety analysis of the contracts we checked. These were implemented as simpler or dummy versions. Lastly, a few custom opcodes were added for analysis — these are all in uppercase.

Custom Instructions

Instruction	Description
ASSERT(b)	Checks assertion condition b; reports a violation when b is false.
WAIT(n)	Increases the current timestamp by n seconds.
MK_SYMBOL()	Creates a fresh symbolic uint256.
EXT_FUND(n)	Increases the balance of the current address by n wei.
SETLINKER(s,n)	Sets string s to point at uint256 n in the linker table used by the linkersymbol instruction.
START_ANALYSIS()	Passes control to the opponent; equivalent to LAUNCH_OPPONENT.
IMPERSONATECALL(c,g,t,v,i,s1,o,s2)	Variant of call that spoofs the calling address; behaves as if called from address c.
REVEAL_UINT(n)	Passes the uint256 word n to the opponent as a value.
REVEAL_ADDR(n)	Passes the uint256 word n to the opponent as an address.

Print Instructions

Instruction	Description
PRINT	Print a uint256 word as an unsigned decimal integer.
PRINT_signed	Print a uint256 word as a signed decimal integer.
PRINT_HEX	Print a uint256 word in uppercase hexadecimal.
PRINT_hex	Print a uint256 word in lowercase hexadecimal.
PRINT_bin	Print a uint256 word in binary.
PRINT_object	Print the current object.
PRINT_IDS	Print all discovered object IDs.
PRINT_names	Print all discovered object names.
PRINT_sigma	Print the symbolic environment (sigma) directly.
PRINT_z3	Print the symbolic environment (sigma) via Z3.
PRINT_mem	Print the current memory.
PRINT_ascii	Print the ASCII string interpretation of a uint256 word.

Note: All uint words are uint256 by default.

See GUIDE.md for the corresponding Solidity helper functions implementing these instructions.