Oyente+ – an Analysis Tool for Smart Contracts

History

Oyente+ is a modernized version of the original Oyente symbolic execution tool for Ethereum smart contracts. Oyente and Oyente+ are designed to detect smart-contract weaknesses like reentrancy, integer overflow, and timestamp dependence. As one of the earliest tools in the field, Oyente has served as a foundation for extensions and as a reference point for evaluating new approaches. Over time, however, it has become increasingly difficult to use: it cannot analyze newer contracts that rely on EVM instructions introduced after its initial release (for example, the shift opcodes or PUSH0), and it depends on Python 2 and outdated libraries, which complicates installation. Oyente+ preserves Oyente's analysis capabilities while providing full support for the current EVM instruction set. The codebase has been ported to Python 3 and updated to follow contemporary software-engineering practices

Installation

Dependencies

• Python 3.8+ (excluding 3.12.0, but 3.12.1+ is fine)
• Poetry - PEP 621 compliant dependency management
• Solidity compiler (solc) - Contract compilation
• Docker (optional) - For containerized deployment

Installation

# Start by cloning the repository.
git clone https://github.com/smartbugs/oyente_plus.git
cd oyente_plus

Option 1: setup script

./scripts/setup-venv.sh  # setup virtual env with all dependencies
source venv/bin/activate # activate virtual env

Option 2: make (poetry required)

make setup

Option 3: manual setup (poetry required)

poetry install --with dev  # install with development tooling
# or alternatively
poetry install --only main # install for production only

Option 4: docker

# make sure you have Docker installed
docker pull smartbugs/oyente_plus
docker run -it smartbugs/oyente_plus

Dependency: the Solidity compiler

# Use solc-select for version management (recommended)
solc-select install latest
solc-select use latest

# Ubuntu/Debian
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc

Usage

# Analyze Solidity contract
python oyente/oyente.py -s contract.sol

# Analyze with assertion checking
python oyente/oyente.py -a -s contract.sol

# Analyze EVM bytecode
python oyente/oyente.py -s bytecode_file -b

# Analyze remote contract
python oyente/oyente.py -ru https://example.com/contract.sol

# Get help
python oyente/oyente.py --help

Sample Contracts

The samples/ directory contains test contracts including:

• SimpleDAO.sol - Reentrancy vulnerability
• EtherLotto.sol - Randomness issues
• Government.sol - Access control patterns

Resources

• Original Paper: Oyente: Making Smart Contracts Safer

Contributing

We welcome contributions! Please:

1. Open an Issue: Report bugs or suggest features on our issue tracker
2. Submit PRs: Feel free to send us a PR for changes you want to see!
3. Follow Standards: Ensure all quality checks pass with make all

See the development guide for more information on the architecture of Oyente+ and the development environment.