Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Slottify expressions #1729

Draft
wants to merge 147 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
147 commits
Select commit Hold shift + click to select a range
1d24ef9
Quick fix to serialize big concrete Arrays
feliam Jan 17, 2020
d76d8b1
blacken
feliam Jan 20, 2020
f4ba546
smtlib expressions with kwargs and slots
feliam Jan 23, 2020
5c187bd
remove debug script:
feliam Jan 28, 2020
3467886
blkn
feliam Jan 28, 2020
f24b7eb
Merged
feliam May 4, 2020
0cd1bc5
Add ONE failing test
feliam May 13, 2020
609a37e
Fix test
feliam May 13, 2020
b29f3ac
Try fix get-related
feliam May 13, 2020
3bbb483
Playing with mypy
feliam May 26, 2020
154326c
CC
feliam May 26, 2020
f4eac7f
merge
feliam May 27, 2020
4192b6e
Test fix
feliam May 27, 2020
7885c84
Fixing ArrayProxy usages
feliam May 27, 2020
df96058
Remove bytearray from expression and tests
feliam May 28, 2020
cc24e0d
Fix uses of unhasheable arrayproxy
feliam Jun 1, 2020
1146104
blkn
feliam Jun 1, 2020
51a67a2
Merge branch 'master' into dev-fix-arrayproxy
feliam Jun 1, 2020
79aa5cc
Move regression to other
feliam Jun 2, 2020
7339eb9
blkn
feliam Jun 2, 2020
c121c38
blkn
feliam Jun 2, 2020
b40de82
Various expression.py refactors
feliam Jun 3, 2020
b5d6b9c
blkn
feliam Jun 3, 2020
198e0d8
fix tests
feliam Jun 3, 2020
d82b398
CC
feliam Jun 3, 2020
487f2bb
underlying_variable
feliam Jun 3, 2020
ec250a0
CC
feliam Jun 3, 2020
f922e6f
Add .name
feliam Jun 3, 2020
3476a11
blkn
feliam Jun 3, 2020
866bc0b
fix array name
feliam Jun 3, 2020
3ff6b95
Move get related
feliam Jun 5, 2020
02b4c69
Merge branch 'master' into dev-get-related
feliam Jun 5, 2020
00e8199
CC
feliam Jun 5, 2020
6b7f671
fix concolic
feliam Jun 5, 2020
6732eb2
lint
feliam Jun 5, 2020
d54ba40
merge
feliam Jun 5, 2020
4adeac2
DivByZero default to zero
feliam Jun 5, 2020
7565b4a
blkn
feliam Jun 5, 2020
1680397
Update manticore/core/smtlib/solver.py
feliam Jun 5, 2020
cbe55b9
Update manticore/core/smtlib/constraints.py
feliam Jun 5, 2020
315ef64
Update manticore/core/smtlib/constraints.py
feliam Jun 5, 2020
6155a4d
remove odd string
feliam Jun 5, 2020
38dbfd6
Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…
feliam Jun 5, 2020
1491cbd
lint
feliam Jun 5, 2020
264eb04
mypy lint
feliam Jun 5, 2020
e0130a4
Update manticore/core/smtlib/visitors.py
feliam Jun 5, 2020
d0e9abf
lint
feliam Jun 5, 2020
9807b37
Add Docs
feliam Jun 8, 2020
728e021
Merge branch 'master' into dev-get-related
feliam Jun 9, 2020
e584fb2
merge
feliam Jun 9, 2020
bf3a2b9
Replace modulo with masks
Jun 10, 2020
3eb96f8
Blacken
Jun 10, 2020
5e54189
blkn
feliam Jun 10, 2020
a0ab429
Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…
feliam Jun 10, 2020
536ec71
fix mypy
feliam Jun 10, 2020
a83e8c2
fix mypy
feliam Jun 10, 2020
37144d9
Add tests for signed LT behavior
Jun 10, 2020
1b8754d
New test
feliam Jun 10, 2020
787e51f
Fix constant folding
feliam Jun 10, 2020
dca9adb
merge
feliam Jun 10, 2020
dfa7a84
lint
feliam Jun 10, 2020
b841038
lint
feliam Jun 10, 2020
735a963
lint
feliam Jun 10, 2020
b54a448
Unittesting power
feliam Jun 10, 2020
02563cd
Permisive read_buffer
feliam Jun 10, 2020
3fab981
Preserve precision in constant folding
Jun 10, 2020
f7fb8bb
Strip left-in print debugging
Jun 11, 2020
2f5d4d2
fix wasm
feliam Jun 11, 2020
18064f8
Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…
feliam Jun 11, 2020
52d8eb4
Fix
feliam Jun 11, 2020
f1dfb80
REmove get_related from the default path and fix arm test
feliam Jun 12, 2020
d5b577e
blkn
feliam Jun 12, 2020
79b42ed
fix related to tests
feliam Jun 12, 2020
ec8489f
blkn
feliam Jun 12, 2020
2113a73
Fix bug in test and disable debug messages in Solver
feliam Jun 12, 2020
c2a21ba
smtlib config to disable multiple check-sat in newer z3
feliam Jun 12, 2020
f87e1e2
Disable log test and fix merging poc vs variable migration
feliam Jun 15, 2020
2eb630d
blkn
feliam Jun 15, 2020
8818ea3
Avoid exception in some callbacks
feliam Jun 15, 2020
27db1b8
can_raise at did_will
feliam Jun 15, 2020
e5cebb1
merge
feliam Jun 15, 2020
e717bf3
merge
feliam Jun 15, 2020
937d988
blkn
feliam Jun 15, 2020
85263a8
wip
feliam Jun 17, 2020
6e161d1
merge
feliam Jul 14, 2020
685beed
merge
feliam Jul 16, 2020
df4d457
WIP
feliam Jul 17, 2020
9896b72
merge
feliam Jul 20, 2020
5690dc5
OMG expression refactor AHHH!
feliam Aug 17, 2020
0e58c3e
merge
feliam Aug 17, 2020
21be706
mypy + Z3->SelectedSolver
feliam Aug 17, 2020
5ac21a4
lint
feliam Aug 17, 2020
19f4d43
BitVec Bitvec
feliam Aug 17, 2020
cbe2174
fix tests
feliam Aug 17, 2020
354cec3
Various Expression refactors and docs
feliam Sep 8, 2020
94232b9
blkn
feliam Sep 8, 2020
570b1e4
Asorted expression fixes and refactors
feliam Sep 29, 2020
7168829
blkn
feliam Oct 7, 2020
d669e41
Silence CClimate
feliam Oct 7, 2020
cce9dd4
Silence CClimate
feliam Oct 7, 2020
d5cffe6
Merge master in
feliam Oct 7, 2020
37446fc
Silence black
feliam Oct 7, 2020
bc81838
BitVec -> Bitvec
feliam Oct 7, 2020
f163497
blkn
feliam Oct 7, 2020
c232d58
Lint
feliam Oct 8, 2020
9200178
Lint
feliam Oct 8, 2020
ef844bd
Fix debug assertion
feliam Oct 8, 2020
79c0b66
blkn
feliam Oct 8, 2020
f17bd7f
Apply suggestions from code review
feliam Oct 15, 2020
b7a5bc0
Apply suggestions from code review
feliam Oct 15, 2020
e57975e
review comments
feliam Oct 15, 2020
c0ea781
review comments
feliam Oct 15, 2020
a102dae
blkn
feliam Oct 16, 2020
87a6887
backpedal on ABC
feliam Oct 16, 2020
9123dcf
relax size test
feliam Oct 16, 2020
0595ce0
lint
feliam Oct 16, 2020
d45e01b
Fixed some tests
feliam Oct 19, 2020
2aa5b70
blkn
feliam Oct 19, 2020
188054c
Disable wasm
feliam Oct 20, 2020
ba5499b
Apply suggestions from code review
feliam Oct 20, 2020
2fe9a06
Fix tests
feliam Oct 20, 2020
8d33428
CI Test
feliam Dec 1, 2020
ed11626
Format with black 19.10b0
ekilmer Jan 11, 2021
5ffe40a
Add toposort dependency
ekilmer Jan 12, 2021
6a9f392
Fix x86 NEG instruction Python implementation
ekilmer Jan 12, 2021
1cb97be
Fix BitVecUnsignedDiv division by zero
ekilmer Jan 12, 2021
c220799
Update setup-python GHA
ekilmer Jan 12, 2021
5eea790
Update mypy to 0.790 and add examples directory to checking
ekilmer Jan 12, 2021
f44d570
debug: No fast-fail for matrix
ekilmer Jan 12, 2021
2fa2561
Fix coveralls uploading
ekilmer Jan 12, 2021
2605e46
merge
feliam Jan 13, 2021
487e5f4
merge
feliam Jan 13, 2021
4323bef
merge
feliam Jan 14, 2021
d46eea1
merge master in
feliam Jan 15, 2021
6ff1e87
Ek testing dev expressions (#2388)
ekilmer Jan 19, 2021
8e0797d
Add comment
feliam Jan 19, 2021
e0e6584
merge
feliam Jan 19, 2021
4843f90
Remove unused/wrong operator
feliam Jan 19, 2021
d27068c
fix changelog
feliam Feb 2, 2021
49d82da
fix cache
feliam Feb 8, 2021
2c6cffa
CC
ekilmer Feb 18, 2021
38a261c
Merge branch 'master' into dev-expressions
ekilmer Feb 18, 2021
a81f8e8
Upgrade mypy and linting fixes
ekilmer Feb 19, 2021
6610f0c
Make sure concatenation variable is unique
ekilmer Feb 23, 2021
dda6d6a
Don't pin pytest dependencies
ekilmer Feb 23, 2021
58136f0
Implement __bool__ for BoolEqual. Return True by default
ekilmer Feb 23, 2021
f2055be
Fix some wasm tests due to bad changes made to generator script
ekilmer Feb 23, 2021
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 8 additions & 7 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@ jobs:
steps:
- uses: actions/checkout@v2
- name: Set up Python 3.6
uses: actions/setup-python@v1
uses: actions/setup-python@v2
with:
python-version: 3.6
python-version: '3.6'
- name: Lint
if: github.event_name == 'pull_request'
env:
Expand All @@ -41,14 +41,15 @@ jobs:
tests:
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "other", "wasm", "wasm_sym"]
steps:
- uses: actions/checkout@v1
- name: Set up Python 3.6
uses: actions/setup-python@v1
uses: actions/setup-python@v2
with:
python-version: 3.6
python-version: '3.6'
- name: Install NPM
uses: actions/setup-node@v1
with:
Expand Down Expand Up @@ -98,9 +99,9 @@ jobs:
steps:
- uses: actions/checkout@v2
- name: Set up Python 3.6
uses: actions/setup-python@v1
uses: actions/setup-python@v2
with:
python-version: 3.6
python-version: '3.6'
- name: Build Dist
run: |
python3 -m pip install wheel
Expand Down
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ nosetests.xml
coverage.xml
*,cover
.hypothesis/
mcore_*

# Translations
*.mo
Expand Down
20 changes: 11 additions & 9 deletions examples/evm/asm_to_smtlib.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@
from manticore.utils import log

# log.set_verbosity(9)
config.out_of_gas = 1
# FIXME: What's the equivalent?
consts = config.get_group("evm")
consts["oog"] = "complete"


def printi(instruction):
Expand Down Expand Up @@ -42,11 +44,11 @@ def printi(instruction):
)


data = constraints.new_array(index_bits=256, name="array")
data = constraints.new_array(index_size=256, name="array")


class callbacks:
initial_stack = []
class Callbacks:
initial_stack: List[BitVec] = []

def will_execute_instruction(self, pc, instr):
for i in range(len(evm.stack), instr.pops):
Expand All @@ -57,8 +59,8 @@ def will_execute_instruction(self, pc, instr):

class DummyWorld:
def __init__(self, constraints):
self.balances = constraints.new_array(index_bits=256, value_bits=256, name="balances")
self.storage = constraints.new_array(index_bits=256, value_bits=256, name="storage")
self.balances = constraints.new_array(index_size=256, value_size=256, name="balances")
self.storage = constraints.new_array(index_size=256, value_size=256, name="storage")
self.origin = constraints.new_bitvec(256, name="origin")
self.price = constraints.new_bitvec(256, name="price")
self.timestamp = constraints.new_bitvec(256, name="timestamp")
Expand Down Expand Up @@ -112,10 +114,10 @@ def send_funds(self, address, recipient, value):
value = constraints.new_bitvec(256, name="value")

world = DummyWorld(constraints)
callbacks = callbacks()
callbacks = Callbacks()

# evm = world.current_vm
evm = EVM(constraints, 0x41424344454647484950, data, caller, value, code, world=world, gas=1000000)
evm = EVM(0x41424344454647484950, data, caller, value, code, world=world, gas=1000000)
evm.subscribe("will_execute_instruction", callbacks.will_execute_instruction)

print("CODE:")
Expand All @@ -138,5 +140,5 @@ def send_funds(self, address, recipient, value):
print(constraints)

print(
f"PC: {translate_to_smtlib(evm.pc)} {solver.get_all_values(constraints, evm.pc, maxcnt=3, silent=True)}"
f"PC: {translate_to_smtlib(evm.pc)} {SMTLIBSolver.get_all_values(constraints, evm.pc, maxcnt=3, silent=True)}"
)
3 changes: 1 addition & 2 deletions examples/evm/coverage.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,8 @@

user_account = m.create_account(balance=1000)

bytecode = m.compile(source_code)
# Initialize contract
contract_account = m.create_contract(owner=user_account, balance=0, init=bytecode)
contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)

m.transaction(
caller=user_account,
Expand Down
28 changes: 15 additions & 13 deletions examples/evm/mappingchallenge.py
Original file line number Diff line number Diff line change
Expand Up @@ -30,22 +30,24 @@ class StopAtDepth(Detector):
""" This just aborts explorations that are too deep """

def will_run_callback(self, *args):
with self.manticore.locked_context("seen_rep", dict) as reps:
reps.clear()
if self.manticore:
with self.manticore.locked_context("seen_rep", dict) as reps:
reps.clear()

def will_decode_instruction_callback(self, state, pc):
world = state.platform
with self.manticore.locked_context("seen_rep", dict) as reps:
item = (
world.current_transaction.sort == "CREATE",
world.current_transaction.address,
pc,
)
if not item in reps:
reps[item] = 0
reps[item] += 1
if reps[item] > 2:
state.abandon()
if self.manticore:
with self.manticore.locked_context("seen_rep", dict) as reps:
item = (
world.current_transaction.sort == "CREATE",
world.current_transaction.address,
pc,
)
if not item in reps:
reps[item] = 0
reps[item] += 1
if reps[item] > 2:
state.abandon()


m.register_plugin(StopAtDepth())
Expand Down
4 changes: 3 additions & 1 deletion examples/evm/minimal-json.py
Original file line number Diff line number Diff line change
Expand Up @@ -1047,7 +1047,9 @@
user_account = m.create_account(balance=1000, name="user_account")
print("[+] Creating a user account", user_account.name_)

contract_account = m.json_create_contract(truffle_json, owner=user_account, name="contract_account")
contract_account = m.solidity_create_contract(
truffle_json, owner=user_account, name="contract_account"
)
print("[+] Creating a contract account", contract_account.name_)
contract_account.sendCoin(1, 1)

Expand Down
5 changes: 3 additions & 2 deletions examples/evm/minimal.py
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,14 @@
}
}
"""
user_account = m.create_account(balance=m.make_symbolic_value(), name="user_account")

user_account = m.create_account(balance=10 ** 10, name="user_account")
print("[+] Creating a user account", user_account.name_)

contract_account = m.solidity_create_contract(
source_code, owner=user_account, name="contract_account"
)
print("[+] Creating a contract account", contract_account.name_)
print(f"[+] Creating a contract account {contract_account}")
contract_account.named_func(1)

print("[+] Now the symbolic values")
Expand Down
4 changes: 4 additions & 0 deletions examples/evm/use_def.py
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@
class EVMUseDef(Plugin):
def did_evm_write_storage_callback(self, state, address, offset, value):
m = self.manticore
if not m:
return
world = state.platform
tx = world.all_transactions[-1]
md = m.get_metadata(tx.address)
Expand All @@ -55,6 +57,8 @@ def did_evm_write_storage_callback(self, state, address, offset, value):

def did_evm_read_storage_callback(self, state, address, offset, value):
m = self.manticore
if not m:
return
world = state.platform
tx = world.all_transactions[-1]
md = m.get_metadata(tx.address)
Expand Down
6 changes: 2 additions & 4 deletions examples/linux/binaries/concrete_solve.py
Original file line number Diff line number Diff line change
@@ -1,16 +1,14 @@
from manticore import Manticore
from manticore.native import Manticore


def fixme():
raise Exception("Fill in the blanks!")


# Let's initialize the manticore control object
m = Manticore("multiple-styles")

# First, let's give it some fake data for the input. Anything the same size as
# the real flag should work fine!
m.concrete_data = "infiltrate miami!"
m = Manticore("multiple-styles", concrete_start="infiltrate miami!")

# Now we're going to want to execute a few different hooks and share data, so
# let's use the m.context dict to keep our solution in
Expand Down
2 changes: 1 addition & 1 deletion examples/linux/binaries/symbolic_solve.py
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
from manticore import Manticore
from manticore.native import Manticore


def fixme():
Expand Down
5 changes: 3 additions & 2 deletions examples/script/concolic.py
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
import queue
import struct
import itertools
from typing import Any

from manticore import set_verbosity
from manticore.native import Manticore
Expand Down Expand Up @@ -234,7 +235,7 @@ def constraints_are_sat(cons):


def get_new_constrs_for_queue(oldcons, newcons):
ret = []
ret: List[Any] = []

# i'm pretty sure its correct to assume newcons is a superset of oldcons

Expand Down Expand Up @@ -299,7 +300,7 @@ def concrete_input_to_constraints(ci, prev=None):

def main():

q = queue.Queue()
q: queue.Queue = queue.Queue()

# todo randomly generated concrete start
stdin = ints2inp(0, 5, 0)
Expand Down
2 changes: 1 addition & 1 deletion examples/script/introduce_symbolic_bytes.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
#!/usr/bin/env python

import sys
import capstone

from manticore import issymbolic
from manticore.native import Manticore
Expand Down Expand Up @@ -64,7 +65,6 @@ def introduce_sym(state):
state.cpu.write_int(state.cpu.RBP - 0xC, val, 32)

def has_tainted_operands(operands, taint_id):
# type: (list[manticore.core.cpu.abstractcpu.Operand], object) -> bool
for operand in operands:
op = operand.read()
if issymbolic(op) and taint_id in op.taint:
Expand Down
2 changes: 2 additions & 0 deletions manticore/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@


def main() -> None:
import pdb

"""
Dispatches execution into one of Manticore's engines: evm or native.
"""
Expand Down
Loading