🐣 Examples
Here we show some examples to demonstrate the usage of some of the greed APIs and how to levereage them to accomplish a few interesting tasks.
(1) Reachibility of a CALL statement
In this example, we show how to automatically synthetize the CALLDATA
to reach an arbitrary CALL
statement in an unverified contract 0x204Db9Ca00912c0F9e6380342113f6A0147E6f8C
on chain.
First, you should download the contract bytecode and place it in a contract.hex
file:
Then, use our script analyze_hex.sh
(shipped with greed) to run Gigahorse against it:
( the script is in the /greed/resources/
folder)
This will produce many artifacts in the current folder:
$ ls
ActualReturnArgs.csv
AllCALLsClassified.csv
Analytics_ArrayCopy.csv
Analytics_ArrayHasTwoElementLengths.csv
Analytics_BlockHasNoTACBlock.csv
Analytics_BlockInMultipleFunctions.csv
Analytics_BlockInNoFunctions.csv
Analytics_BlockIsEmpty.csv
[ ... ]
Now, we have everything we need to start using greed! This is our example analysis script to automatically generate the
CALLDATA
needed to reach the target CALL
statement (follow the comments).
import logging
from greed import Project, options
from greed.exploration_techniques import ExplorationTechnique, DirectedSearch, HeartBeat, Prioritizer, DFS
from greed.utils.extra import gen_exec_id
from greed.solver.shortcuts import *
LOGGING_FORMAT = "%(levelname)s | %(message)s"
logging.basicConfig(level=logging.INFO, format=LOGGING_FORMAT)
log = logging.getLogger("example")
log.setLevel(logging.INFO)
def config_greed():
options.WEB3_PROVIDER = 'http://0.0.0.0:8545' # your web3 RPC node.
options.GREEDY_SHA = True
options.LAZY_SOLVES = False
options.STATE_INSPECT = True
options.MAX_SHA_SIZE = 300
options.OPTIMISTIC_CALL_RESULTS = True
options.DEFAULT_EXTCODESIZE = True
options.DEFAULT_CREATE2_RESULT_ADDRESS = True
options.DEFAULT_CREATE_RESULT_ADDRESS = True
options.MATH_CONCRETIZE_SYMBOLIC_EXP_EXP = True
options.MATH_CONCRETIZE_SYMBOLIC_EXP_BASE = True
def main():
config_greed()
block_ref = 16489409
# This is the PC of the target call
#(according to the contract.tac file in the Gigahorse analysis folder )
call_pc = "0x1f7"
# Create the greed project
proj = Project(target_dir="./contracts/0x204Db9Ca00912c0F9e6380342113f6A0147E6f8C/")
# We want to reach this call statement
call_stmt = proj.statement_at[call_pc]
# Get information about the block to concretize the block context
block_info = proj.w3.eth.get_block(block_ref)
# Create the initial context
init_ctx = {
"CALLER": "0x6b6Ae9eDA977833B379f4b49655124b4e5c64086",
"ORIGIN": "0x6b6Ae9eDA977833B379f4b49655124b4e5c64086",
"ADDRESS": "0x204Db9Ca00912c0F9e6380342113f6A0147E6f8C",
"NUMBER": block_info.number,
"DIFFICULTY": block_info["totalDifficulty"],
"TIMESTAMP": block_info["timestamp"]
}
# Generate a new execution id
xid = gen_exec_id()
# Create the entry state
entry_state = proj.factory.entry_state(
xid=xid,
init_ctx=init_ctx,
max_calldatasize=2048,
partial_concrete_storage=True
)
# Setting up the simulation manager!
simgr = proj.factory.simgr(entry_state=entry_state)
# Enabling directed symbolic execution
directed_search = DirectedSearch(call_stmt)
simgr.use_technique(directed_search)
# Together with the prioritizer, this technique will prioritize states that are closer to the target
prioritizer = Prioritizer(scoring_function=lambda s: -s.globals['directed_search_distance'])
simgr.use_technique(prioritizer)
# Some nice output :)
heartbeat = HeartBeat(beat_interval=1, show_op=True)
simgr.use_technique(heartbeat)
print(f" Symbolically executing...")
while True:
try:
# Run the simulation manager until we reach the call statement
simgr.run(find=lambda s: s.curr_stmt.id == call_stmt.id)
except Exception as e:
print(e)
continue
# Found a state at the call statement!
if len(simgr.found) == 1:
print(f" ✅ Found state for {call_stmt.__internal_name__} at {call_stmt.id}!")
state = simgr.one_found
# Get a solution for the calldata, this is the value that we should pass to
# reach the call statement!
calldata_sol = state.solver.eval_memory(state.calldata, length=BVV(1024, 256))
print(f" 📥 Calldata: {calldata_sol}")
break
elif len(simgr.found) == 0:
# if we are here, it is not possible to reach the call statement given
# the current context
print(f" ❌ No state found for {call_stmt.__internal_name__} at {call_stmt.id}!")
break
if __name__ == "__main__":
main()
(2) Retrieve the slot IDs involved in access control checks
This example shows how to fetch all the slot ids holding addresses of account involved in an access control check. The script makes use of a builtin analysis offered by greed. Specifically, this analysis employs a backward slice against the static use-def graph of the TAC opcodes to detect patterns of access control routines.
As explained before, first analyze the contract with Gigahorse. Then, you can use the following script:
from greed import Project
from greed.analyses.access_control_slots import get_access_control_slots
p = Project(target_dir="./0xdAC17F958D2ee523a2206206994597C13D831ec7/")
get_access_control_slots(p)
Will output:
Essentially, this is saying that slot 0x0
holds an address that is checked against msg.sender before executing some code in the contract.
(3) Mint a PudgyPenguin
In this example we show how one can synthetize the CALLDATA
and the CALLVALUE
necessary to mint() a PudgyPenguin(🐧) in the contract at 0xBd3531dA5CF5857e7CfAA92426877b022e612cf8
.
After analyzing the contract as explained in the previous example, you can use the following script:
import web3
import logging
from greed import Project, options
from greed.exploration_techniques import ExplorationTechnique, DirectedSearch, HeartBeat, Prioritizer, DFS
from greed.utils.extra import gen_exec_id
from greed.solver.shortcuts import *
LOGGING_FORMAT = "%(levelname)s | %(message)s"
logging.basicConfig(level=logging.INFO, format=LOGGING_FORMAT)
log = logging.getLogger("example")
log.setLevel(logging.INFO)
def config_greed():
options.GREEDY_SHA = True
options.LAZY_SOLVES = False
options.STATE_INSPECT = True
options.MAX_SHA_SIZE = 300
options.OPTIMISTIC_CALL_RESULTS = True
options.DEFAULT_EXTCODESIZE = True
options.DEFAULT_CREATE2_RESULT_ADDRESS = True
options.DEFAULT_CREATE_RESULT_ADDRESS = True
options.MATH_CONCRETIZE_SYMBOLIC_EXP_EXP = True
options.MATH_CONCRETIZE_SYMBOLIC_EXP_BASE = True
def main():
config_greed()
# 4 bytes of the mint() function
# 0 --> 3
calldata = "0x40c10f19"
block_ref = 12878195
# Create the greed project
proj = Project(target_dir="./contracts/0xBd3531dA5CF5857e7CfAA92426877b022e612cf8/")
# this is the pc of the STOP opcode in the mint function
STOP = "0x43f"
stop_stmt = proj.statement_at[STOP]
block_info = proj.w3.eth.get_block(block_ref)
# Let's set the CALLER to my account
init_ctx = {
"CALLDATA": calldata,
"CALLER": "0x6b6Ae9eDA977833B379f4b49655124b4e5c64086",
"ORIGIN": "0x6b6Ae9eDA977833B379f4b49655124b4e5c64086",
"ADDRESS": "0xBd3531dA5CF5857e7CfAA92426877b022e612cf8",
"NUMBER": block_info.number,
"DIFFICULTY": block_info["totalDifficulty"],
"TIMESTAMP": block_info["timestamp"]
}
xid = gen_exec_id()
# Create the entry state
entry_state = proj.factory.entry_state(
xid=xid,
init_ctx=init_ctx,
max_calldatasize=68,
partial_concrete_storage=True
)
# The second argument of mint is the "amount" of penguins to mint, we want that to be non-zero!
entry_state.add_constraint(NotEqual(entry_state.calldata[BVV(67,256)], BVV(0,8)))
# Set a constraint on the CALLVALUE
entry_state.add_constraint(BV_ULE(entry_state.ctx['CALLVALUE'], BVV(0x6000000000000000, 256)))
# When a Penguin is minted, we see a LOG4, let's setup an inspection
# point and show a message!
def hi(simgr, state):
log.debug(f'Emitted LOG4 at {state.curr_stmt.id}!')
entry_state.inspect.stop_at_stmt(stmt_name="LOG4", func=hi)
# Setting up the simulation manager
simgr = proj.factory.simgr(entry_state=entry_state)
directed_search = DirectedSearch(stop_stmt)
simgr.use_technique(directed_search)
prioritizer = Prioritizer(scoring_function=lambda s: -s.globals['directed_search_distance'])
simgr.use_technique(prioritizer)
heartbeat = HeartBeat(beat_interval=100, show_op=True)
simgr.use_technique(heartbeat)
print(f" Symbolically executing...")
while True:
try:
simgr.run(find=lambda s: s.curr_stmt.id == stop_stmt.id)
except Exception as e:
print(e)
continue
if len(simgr.found) == 1:
print(f" ✅ Found state for {stop_stmt.__internal_name__} at {stop_stmt.id}!")
state = simgr.one_found
# Fix the shas!
if len(state.sha_observed) > 0:
shas = state.sha_resolver.fix_shas()
if shas != None:
print(f'Fixed {len(shas)} shas in the state!')
else:
print('Could not fix shas solutions, state is unsat')
assert(False)
# Get a solution for the CALLDATA
calldata_sol = state.solver.eval_memory(state.calldata, length=BVV(68,256), raw=True)
# Get a solution for CALLVALUE (i.e., how much we paid for a penguin)
# (Note: Yices2 does not expose a min() function, but you can find the minimum value
# by using a bisection search)
callvalue = state.solver.eval(state.ctx['CALLVALUE'])
print(f" 📥 Calldata: {hex(bv_unsigned_value(calldata_sol))}")
print(f" 💸 Callvalue: {callvalue}")
break
elif len(simgr.found) == 0:
print(f" ❌ No state found for {stop_stmt.__internal_name__} at {stop_stmt.id}!")
break
if __name__ == "__main__":
main()