Skip to content

Commit

Permalink
example 1 done
Browse files Browse the repository at this point in the history
Signed-off-by: degrigis <[email protected]>
  • Loading branch information
degrigis committed Dec 19, 2023
1 parent f22d194 commit aa34679
Show file tree
Hide file tree
Showing 2 changed files with 181 additions and 1 deletion.
154 changes: 154 additions & 0 deletions docs/docs/examples.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,154 @@
# 🐣 Examples

## (1) Reaching an arbitrary 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.
This example demonstrates the usage of some of the greed APIs and how to use them to accomplish the task.

First, you should download the [contract bytecode](https://library.dedaub.com/ethereum/address/0x204db9ca00912c0f9e6380342113f6a0147e6f8c/bytecode) and place it in a `contract.hex` file:

```bash
degrigis@tati:~/contracts/0x204Db9Ca00912c0F9e6380342113f6A0147E6f8C$ cat contract.hex
0x6080604052600436106100595760003560e...
```

Then, use our script `analyze_hex.sh` (shipped with greed) to run Gigahorse against it:
( the script is in the `/greed/resources/` folder)

```bash
degrigis@tati:~/contracts/0x204Db9Ca00912c0F9e6380342113f6A0147E6f8C$ analyze_hex.sh --file ./contract.hex
```

This will produce many artifacts in the current folder:

```bash
degrigis@tati:~/contracts/0x204Db9Ca00912c0F9e6380342113f6A0147E6f8C$ ls -l
degrigis@tati:~/projects/greed-examples/contracts/0x204Db9Ca00912c0F9e6380342113f6A0147E6f8C$ ls -l
total 872
-rw-rw-r-- 1 degrigis degrigis 934 Dec 19 10:55 ActualReturnArgs.csv
-rw-rw-r-- 1 degrigis degrigis 2 Dec 19 10:55 AllCALLsClassified.csv
-rw-rw-r-- 1 degrigis degrigis 23 Dec 19 10:55 Analytics_ArrayCopy.csv
-rw-rw-r-- 1 degrigis degrigis 12 Dec 19 10:55 Analytics_ArrayHasTwoElementLengths.csv
-rw-rw-r-- 1 degrigis degrigis 0 Dec 19 10:55 Analytics_BlockHasNoTACBlock.csv
-rw-rw-r-- 1 degrigis degrigis 0 Dec 19 10:55 Analytics_BlockInMultipleFunctions.csv
-rw-rw-r-- 1 degrigis degrigis 0 Dec 19 10:55 Analytics_BlockInNoFunctions.csv
-rw-rw-r-- 1 degrigis degrigis 0 Dec 19 10:55 Analytics_BlockIsEmpty.csv
[ ... ]
```

Now, we have everything we need to start using greed! This is the analysis script to automatically generate the
`CALLDATA` needed to reach the target `CALL` statement (follow the comments).

```python
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
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) Multi-transactions analysis
28 changes: 27 additions & 1 deletion docs/docs/faq.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,13 @@

# ?FAQ


## Why is it names greed?


## How should "greed" be stylized?


## Why didn't you just implement everything on top of angr?


Expand All @@ -13,6 +20,25 @@

## Does greed work with Vyper contracts?

## Why my symbolic execution is stuck?!


## I have a problem, how can I get in touch with greed developers?


## How do I know the correspondence between TAC Statement and original opcode?


## What is the main difference between greed and Mythril?


## What is the main difference between greed and Tether?


## What is the main difference between greed and ETHBMC?



## Why did you choose to build a symbolic executor on TAC?


## I have a problem, how can I get in touch with greed developers?

0 comments on commit aa34679

Please sign in to comment.