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

Unsound symbolication - A general approach to handle symbolic imprecisions #1526

Merged
merged 45 commits into from
Oct 31, 2019
Merged
Changes from 1 commit
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
4046047
Unsound symbolication and asorted fixes
feliam Sep 16, 2019
b667b98
Add test for ULE
feliam Sep 16, 2019
9665aa1
More operators tests
feliam Sep 16, 2019
d021257
remove TT
feliam Sep 16, 2019
87df083
remove TT
feliam Sep 16, 2019
ee2dea1
remove TT
feliam Sep 16, 2019
fd55973
Add test for simple sha3 concretization
feliam Sep 16, 2019
c8653b4
Add test for simple sha3 concretization
feliam Sep 16, 2019
482ed11
Add coverage to integration tests
feliam Sep 17, 2019
e2ecac1
Add coverage to integration tests
feliam Sep 17, 2019
c8f3f25
Added timeout to sha3 matching
feliam Sep 23, 2019
7422bc0
2 files reformatted
feliam Sep 23, 2019
401e06c
Review fixes
feliam Sep 24, 2019
31aa8eb
black
feliam Sep 24, 2019
a958d71
Fix KeepOnlyIfStorageChanges test
feliam Sep 24, 2019
d0099cd
remove dead code
feliam Sep 24, 2019
0b0c193
cleanups
feliam Sep 26, 2019
f7d94f3
remove unused code
feliam Sep 27, 2019
4098ee5
Blacken
Oct 1, 2019
270102c
Better concretize and calldataload
feliam Oct 1, 2019
406692d
Merge branch 'dev-unsound-symb' of github.com:trailofbits/manticore i…
feliam Oct 1, 2019
0471086
black
feliam Oct 1, 2019
1de2fbd
blkn
feliam Oct 1, 2019
31f79c4
mulmod fix
feliam Oct 2, 2019
b11bd92
Blacken
Oct 2, 2019
fa47381
Merge branch 'dev-unsound-symb' of github.com:trailofbits/manticore i…
feliam Oct 3, 2019
5ec8afc
fix calldata rel tests
feliam Oct 3, 2019
632221c
blk
feliam Oct 3, 2019
7b32c59
Merge branch 'master' into dev-unsound-symb
feliam Oct 3, 2019
f482842
Better doc- review
feliam Oct 10, 2019
870fa05
Better doc. Cleanups. sha3timeout changed
feliam Oct 11, 2019
b66dff1
Merge branch 'dev-unsound-symb' of github.com:trailofbits/manticore i…
feliam Oct 11, 2019
c3ff249
Merge branch 'master' into dev-unsound-symb
feliam Oct 12, 2019
d3a5e8a
sha3 - 42mins
feliam Oct 15, 2019
ac14ec3
Merge branch 'dev-unsound-symb' of github.com:trailofbits/manticore i…
feliam Oct 15, 2019
7893d93
blkn
feliam Oct 15, 2019
2d2a3ee
Fix spelling issues, duplicate code, and add type hints
Oct 23, 2019
4370551
Merge branch 'master' into dev-unsound-symb
Oct 23, 2019
df15457
Rm commented code
Oct 23, 2019
07edfd5
review
feliam Oct 30, 2019
47105d5
blkn
feliam Oct 30, 2019
f3db81d
Remove hardcoded conf
feliam Oct 30, 2019
b88ed27
Fix expression bool test
feliam Oct 30, 2019
4c79130
Fix sha3concrete test
feliam Oct 30, 2019
d52ccbd
Merge branch 'master' into dev-unsound-symb
feliam Oct 30, 2019
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
Prev Previous commit
Next Next commit
2 files reformatted
feliam committed Sep 23, 2019
commit 7422bc059e0de1d052cdda5bf52249c80bf1bf84
19 changes: 16 additions & 3 deletions manticore/ethereum/manticore.py
Original file line number Diff line number Diff line change
@@ -66,7 +66,11 @@ def from_string(cls, name):
default=Sha3Type.concretize,
description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with gout of cycle FP killing",
)
consts.add("sha3timeout", 60*20, "Default timeout for matching sha3 for unsound states (see unsound symbolication).")
consts.add(
"sha3timeout",
60 * 20,
"Default timeout for matching sha3 for unsound states (see unsound symbolication).",
)


def flagged(flag):
@@ -1270,7 +1274,14 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
seen = Operators.OR(Operators.AND(x == x_concrete, y == y_concrete), seen)
with state as temp_state:
temp_state.constrain(seen)
if match(temp_state, func, new_symbolic_pairs, new_concrete_pairs, depth + 1, start=start):
if match(
temp_state,
func,
new_symbolic_pairs,
new_concrete_pairs,
depth + 1,
start=start,
):
concrete_pairs.update(new_concrete_pairs)
return True
return False
@@ -1290,7 +1301,9 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
# symbolic_pairs = graph_sort(state, symbolic_pairs)
known_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", set())
new_known_pairs = set(known_pairs)
if not match(state, functions[table], symbolic_pairs, new_known_pairs, start=time.time()):
if not match(
state, functions[table], symbolic_pairs, new_known_pairs, start=time.time()
):
ethereum_context["soundcheck"] = False
return False

2 changes: 1 addition & 1 deletion manticore/platforms/evm.py
Original file line number Diff line number Diff line change
@@ -1213,7 +1213,7 @@ def setstate(state, value):
raise Concretize(
"Concretize PC", expression=expression, setstate=setstate, policy="ALL"
)
#print(self)
# print(self)
try:
# import time
# limbo = 0.0