maian-modern-opcodes

A small patch set that makes MAIAN — the 2018 symbolic-execution tool for finding suicidal, prodigal, and greedy smart contracts — actually work on bytecode compiled by modern Solidity.

TL;DR MAIAN's opcode table predates Constantinople. Modern solc dispatchers extract the function selector with PUSH1 0xE0; SHR. MAIAN never learned SHR (0x1c), so its disassembler stalls at the first unknown byte and can't reach a single function — it silently reports "not vulnerable" on essentially every contract built after ~2019. This patch adds the missing opcodes to the decode/arity tables and the symbolic executor, restoring analysis on current bytecode.

This is an unofficial community patch, not affiliated with the original authors. It is MIT-licensed, like MAIAN itself (see LICENSE).

The problem, concretely

Every Solidity contract begins with a selector dispatcher. Since solc 0.5.x it looks like this:

PUSH1 0x00
CALLDATALOAD
PUSH1 0xE0
SHR            ; <-- 0x1c: take the high 4 bytes = function selector
DUP1
PUSH4 0x...    ; compare against each function's selector
EQ
PUSH2 ...
JUMPI

MAIAN's instruction_list.py maps opcode bytes to names. 0x1b/0x1c/0x1d (SHL/SHR/SAR, added in Constantinople, EIP-145) were simply absent — the byte decoded as unknown, disassembly desynchronized, and no function body was ever explored. The result is not a crash but the worst kind of failure: a confident false negative on modern contracts.

What the patch changes

Two files, both drop-in replacements for MAIAN/tool/:

tool/instruction_list.py — opcode name table (cops) and arity table (allops):

Opcode	Byte	Notes
SHL SHR SAR	0x1b–0x1d	Constantinople bit shifts — the fix that matters most (selector dispatch)
RETURNDATASIZE RETURNDATACOPY	0x3d–0x3e	Byzantium. 0x3d was mis-mapped to MCOPY upstream
EXTCODEHASH	0x3f	Constantinople
CHAINID SELFBALANCE	0x46–0x47	Istanbul
BASEFEE	0x48	London
PUSH0	0x5f	Shanghai (solc ≥ 0.8.20 emits it constantly)
CREATE2	0xf5	Constantinople. 0xf5 was BREAKPOINT upstream

tool/execute_instruction.py — Z3 semantics and stack handlers so the symbolic executor can run those opcodes:

• SHL → z2 << z1, SHR → LShR(z2, z1) (logical), SAR → z2 >> z1 (arithmetic). EVM stack order: shift amount on top.
• PUSH0 pushes a 256-bit zero. It must be handled before the generic op.find('PUSH') branch, which would otherwise try to read a (non-existent) immediate and crash.
• SELFBALANCE mirrors MAIAN's BALANCE assumption (the current contract's balance). RETURNDATASIZE→0, BASEFEE→0, CREATE2→0 placeholder, EXTCODEHASH→ fresh symbolic value, RETURNDATACOPY is a no-op.

Caveats — read before using off BSC

These are pragmatic approximations, honestly flagged:

• CHAINID returns 56 (BNB Smart Chain). If you analyze Ethereum mainnet or another chain, change the CHAINID handler in tool/execute_instruction.py to your chain id (1 for Ethereum). It only matters for contracts that branch on block.chainid.
• RETURNDATASIZE→0 matches the common solc idiom of using it as a cheap zero, but it is not generally correct; a contract that meaningfully inspects returndata size is over-approximated.
• MAIAN already stubs external calls and treats balances symbolically, so these additions keep to the tool's existing precision philosophy rather than raising it.

Usage

Docker (recommended)

The smartbugs/maian image bundles Python 3, Z3, geth and solc. This repo just layers the two patched files on top:

docker build -t maian-modern .

# MAIAN's -b flag wants runtime bytecode as raw hex: no 0x prefix, no newline.
mkdir -p work
printf '%s' "$(cat runtime.hex)" > work/target.bin

# -c 0 suicidal | -c 1 prodigal/leak | -c 2 greedy/lock
docker run --rm -v "$PWD/work":/work maian-modern \
  bash -lc "cd /MAIAN/tool && python3 maian.py -c 0 -b /work/target.bin"

examples/get_code.py fetches a deployed contract's runtime bytecode over a public JSON-RPC endpoint (eth_getCode), and examples/run-on-address.sh wires the two together to run all three checks on a live address.

Drop-in (existing MAIAN checkout)

cp tool/instruction_list.py   /path/to/MAIAN/tool/
cp tool/execute_instruction.py /path/to/MAIAN/tool/

Integration gotcha (worth your time)

MAIAN reports a hit and a miss with almost the same sentence — they differ only by a leading No:

Suicidal vulnerability found! Confirmed!     <- vulnerable
No suicidal vulnerability found              <- safe

A naive substring match for "Suicidal vulnerability found" matches both, silently flagging every safe contract. The same trap exists for greedy (Locking vulnerability found! vs No locking vulnerability found). Prodigal happens to dodge it (miss says No prodigal…, hit says Leak…). When you parse MAIAN output, reject the negated line, e.g.:

echo "$OUT" | grep -iE '<TYPE> vulnerability found' | grep -viE '\bno\b' | grep -q .

Also note: with -b (bytecode only, no on-chain deploy) MAIAN prints Cannot confirm the bug because the contract is not deployed. These are candidates, not confirmed exploits — verify on a local fork before drawing conclusions. In particular MAIAN cannot model ecrecover, so signature-gated withdrawals frequently show up as false "prodigal" hits.

Verification

The patch was checked against positive and negative controls to confirm it discriminates rather than rubber-stamps: a contract with an unguarded selfdestruct → suicidal; the same behind an onlyOwner guard → safe; a contract that leaks ether to an arbitrary caller → prodigal; a plain contract → safe. patches/ contains the unified diffs against the pristine 2018 sources.

Credits & license

• MAIAN © 2018 Ivica Nikolic and contributors — https://github.com/ivicanikolicsg/MAIAN (MIT).
• Dockerized MAIAN by the SmartBugs project — https://github.com/smartbugs/smartbugs.
• This patch set is MIT-licensed. Upstreaming it (to SmartBugs' MAIAN image, or a maintained fork) is welcome and encouraged.