Delay WASM Branch Condition Concretization #1641

jimpo · 2020-03-28T02:43:18Z

The Wasm platform can sometimes silently skip execution paths due to the way it concretizes branch conditions. The issue is that Wasm branch instructions take integers as input and the Wasm symbolic execution engine concretizes the whole integer to continue execution, instead of just the binary condition needed. Aside from being inefficient, the concretization logic prevents forking into more than a small number of values and silently skips exploration of other values.

This change proposes a way to concretize boolean conditions used as advice for execution, imposing the minimal constraints necessary. The engine raises a ConcretizeCondition exception to determine the branch path and constrain the state minimally. The feasible boolean values are put on the stack and read when the instruction in re-executed. If there's a better approach, please do let me know.

CLAassistant · 2020-03-28T02:43:23Z

All committers have signed the CLA.

ehennenfent

First: thank you for the PR! The WASM branching logic is a particularly gnarly bit of code and I'm thrilled to have another pair of eyes on it.

Second, I've renamed this PR to (IMO) more accurately reflect its contents. This particular bug could be equally well described as the default behavior being poorly optimized for certain problems - which threw me off when I was first trying to understand what was going on.

For my colleagues: if you look at the examples added to the tests, you'll notice that all of them branch on an unconstrained integer (referred to herein as x) fairly early-on. On other platforms, that might look something like this: PC = Operations.ITE(x == 0, branch_target_pc, PC + 1). Manticore can then ask the solver for all possible values of <unconstrained_integer> == 0, and create new states based on that. Unfortunately, the WASM stack machine doesn't specify anything like a PC. Control flow for WASM looks like the following:

if x == 0:
    # push instructions from new branch
else:
    # continue on current branch

If you've seen the Unimplemented: __bool__ for Bool error before, you know this won't work. x == 0 will create a Bool from x's BitVec, and Python doesn't know what to do with that. In order to handle this (and execute both branches of the if statement) we need to fork into two states first. Before this PR, the WASM branch did so by concretizing x into all of its possible values and forking into one state for each of those. If, as in these examples, x is an unconstrained value, in theory you'll instantly get a 2**sizeof(x)-sized state explosion. In practice, Manticore will silently limit you to a subset of those states. Right now, it's 7 states. Hence, on these examples, instead of getting all possible behaviors, you get 7 possible behaviors, which don't even exhaustively test all possible paths through the program. You may ask: Why 7? And why don't we warn users about this? I'm not certain, but I'm pretty sure this an EVM-related optimization. We dropped the number of solutions from 1000(!) to 5 as a part of the EVM refactor (#843). Later, in our work on DELEGATECALL (#1108) we raised it to 7, but also silenced the exception that would have alerted users if they were forking on an underconstrained value. While that exception was important (if you're forking on an underconstrained value, you may need to rethink your approach) I don't think we have a good interface for letting the user choose to silence it if they need to - which may be why we disabled it entirely.

Anyway, to fix this problem, this PR defers concretization by pushing a Condition - a new type of value that acts as a stand-in for x == 0 - to the stack. Then, after forking, the branch instruction pops the Condition off the stack and uses the possible values of the conditional, not all possible values of x.

Finally, as a structural suggestion - when building this module, I generally tried to avoid putting anything on the stack that wasn't explicitly specified by the WASM spec. That's because stack operations are (thanks to the events API) somewhat user-facing, and I wanted to avoid any undue confusion that would result from having Manticore do internal record-keeping on the stack. Based on my reading of this, it seems like there should never be more than one Condition on the stack at any given time, and at that, it should always be on top. With that in mind, could we instead add a branch_condition field to the ModuleInstance and store the Condition there?

ehennenfent · 2020-04-01T22:21:51Z

manticore/wasm/structure.py

+        """
+
+        def setstate(state, value: bool):
+            state.platform.stack.data[-1] = Condition(value)


state.stack.push(Condition(value))

Pushing a None to the stack makes me uncomfortable, and should be unnecessary. In theory, one should be able to use the push and pop methods to adjust the stack from setstate, as shown above. However, there appears to be a bug in the StateBase context manager preventing this from working. I'm making a note here so I don't forget about it, but we should fix it in a different PR.

Right. I tried that first, but StateBase.__enter__ does not make a copy of the execution state stored on the platform, namely the stack. I'm still not familiar enough with the architecture to know how to fix that one properly...

ehennenfent · 2020-04-01T22:22:25Z

manticore/core/state.py

@@ -263,6 +263,7 @@ def new_symbolic_value(self, nbits, label=None, taint=frozenset()):
    def concretize(self, symbolic, policy, maxcount=7):
        """ This finds a set of solutions for symbolic using policy.
            This raises TooManySolutions if more solutions than maxcount
+            ^REVIEW: This comment is incorrect because silent=True is used.


This is a good catch and I think it's worth updating the whole comment to reflect the actual behavior.

ehennenfent · 2020-04-01T22:24:54Z

manticore/wasm/structure.py

@@ -1667,16 +1707,31 @@ def __init__(self, arity, frame, expected_block_depth=0):
        self.expected_block_depth = expected_block_depth


+@dataclass
+class Condition:


SMTLib provides a class called BoolConstant that I think might be a suitable replacement for this. It adds some additional helper methods, and wouldn't require us to add a brand new type.

My intention in defining a new is just for semantics. Having a raw boolean on the stack would be kind of confusing and out of context.

Having a raw boolean on the stack would be kind of confusing and out of context

Agree with this, but I think the Condition class and the BoolConstant class serve more or less the same purpose. If you look at the implementations, they're almost identical

class Condition: value: bool #: The boolean condition value def __init__(self, value: bool): self.value = value

class BoolConstant(Bool): __slots__ = ["_value"] def __init__(self, value: bool, *args, **kwargs): self._value = value super().__init__(*args, **kwargs) def __bool__(self): return self.value @property def value(self): return self._value

jimpo · 2020-04-02T03:21:51Z

@ehennenfent Thanks for giving this a look!

Finally, as a structural suggestion - when building this module, I generally tried to avoid putting anything on the stack that wasn't explicitly specified by the WASM spec. That's because stack operations are (thanks to the events API) somewhat user-facing, and I wanted to avoid any undue confusion that would result from having Manticore do internal record-keeping on the stack. Based on my reading of this, it seems like there should never be more than one Condition on the stack at any given time, and at that, it should always be on top. With that in mind, could we instead add a branch_condition field to the ModuleInstance and store the Condition there?

I was intending that there could be multiple Conditions on the stack as a solution to #1642 for Wasm. In particular, on an i32.div_s instruction, the engine would concretize both the zero-division and division-overflow conditions, ultimately getting both Conditions pushed to the top of the stack and proceeding accordingly. So I think some sort of stack is the right abstraction. But I understand the desire to use a separate structure. I view the Conditions as "execution advice". Perhaps it makes sense to have another stack on WasmWorld, like condition_stack or aux_stack or advice_stack or something?

ehennenfent · 2020-04-02T20:05:42Z

Perhaps it makes sense to have another stack on WasmWorld, like condition_stack or aux_stack or advice_stack or something?

This sounds good to me! We actually already use one auxiliary stack for control flow (block_depths in ModuleInstance) so that we can correctly flatten the nested expression blocks into a single instruction queue.

ehennenfent · 2020-04-06T20:59:38Z

Looks like Github Actions' checkout@v1 script is having some issues right now. If you update from master, it should bump it to checkout@v2.

The issue is that the Wasm symbolic execution engine concretizes the integer input to branching instructions. Aside frome being inefficient, the concretization logic prevents forking into more than a small number of values and silently skips exploration of other values.

The engine raises a ConcretizeCondition exception to determine the branch path and constrain the state minimally.

It's unnecessary because c_int32 truncates to 32 bits and it's weird because this bitwise and isn't there for I64.

ehennenfent · 2020-04-07T17:10:01Z

Looking pretty good to me. I notice you move the advice list around a lot and modify it in some slightly unconventional ways - like in ConcretizeCondition, where you pass the old advice as an argument and completely overwrite it, rather than just using .append. I'm guessing that was to get around the issue you encountered before, where calling stack.push resulted in duplicated values?

Also, I notice that you only ever access advice[0] in this code. So, perhaps for this use case, it doesn't need to be a list, but it sounds like if we were to use it for i32.div_s we'd need multiple conditions? In that case, may as well be prepared for the future.

jimpo · 2020-04-07T17:33:28Z

@ehennenfent Yes, in part I pass the advice to ConcretizeCondition to circumvent the bug with state copying in ManticoreBase._fork. But the bigger motivation is that I think it's easiest to clear advice on the state after each instruction execution, regardless of outcome. Another behavior that could work is to clear the advice on any outcome of instruction execution aside from a Concretize exception (which is the only case where the instruction execution didn't complete/resolve and the last instruction is requeued).

And yes, the thought with allowing for multiple conditions in the advice is to handle i32.div_s.

ehennenfent · 2020-04-07T21:56:18Z

Glad we're on the same page. I do find all the shuffling-around of advice to be a bit convoluted, but we can fix that when we get around to fixing state copying. Thanks again for the PR!

* master: (28 commits) Rework syscall invocation for proper behavior under typeguard (#1672) printable_bytes (#1671) Fix several incorrect type hints (#1668) Add type hints to several parts of Manticore (#1667) Fix type confusion in manual CPU tests; delete dead testing code (#1669) Rework WASM Imports and Fix Typos (#1666) Work on "Model is not Available" errors in tests (#1659) Fix TypeGuard Errors in WASM Module (#1601) Remove unused arg ans separate output from workspace (#1651) Add a badge to README.md for LGTM (#1647) Fix 2 problems in Linux `sys_open` support & add type hints (#1657) Fix LGTM Errors (#1656) Delay WASM Branch Condition Concretization (#1641) Add feature for SymbolicSocket through sys_accept (#1618) Add a bunch of type hints & fix a few issues with Linux platform emulation (#1645) Bump to CheckoutV2 (#1654) Add support for `sys_arm_fadvise64_64` (#1648) Add __slots__ to expressions (#1635) Swap remaining uses of `Z3Solver()` to use the singleton interface (#1649) CI: have pytest report 100 slowest tests (#1646) ...

The complete changelog up to this version: ## 0.3.4 - 2020-06-26 Thanks to our external contributors! - [jimpo](https://github.com/trailofbits/manticore/commits?author=jimpo) - [langston-barrett](https://github.com/trailofbits/manticore/commits?author=langston-barrett) ### Ethereum * Support and test against EVM Istanbul [#1676](trailofbits/manticore#1676) * **[Added API]** Added a `manticore-verifier` script for checking properties of smart contracts [#1717](trailofbits/manticore#1717) * Fixed RETURNDATASIZE [#1612](trailofbits/manticore#1612) * Added strategies for symbolic SHA3 replacement [#1609](trailofbits/manticore#1609) * Fixed GAS instruction [#1633](trailofbits/manticore#1633) * Improved balance-related exploration [#1615](trailofbits/manticore#1615) * Add `__format__` to EVM accounts [#1613](trailofbits/manticore#1613) * Discard basic blocks that unavoidably REVERT [#1630](trailofbits/manticore#1630) * Extract printable bytes from return data [#1671](trailofbits/manticore#1671) * Support CHAINID, EXTCODEHASH, and SELFBALANCE instructions [#1644](trailofbits/manticore#1644) * **[Changed API]** Renamed several arguments in EVM API, including `gaslimit` --> `gas` [#1652](trailofbits/manticore#1652) * Explore states that self-destruct [#1699](trailofbits/manticore#1699) * Lazy solving for the Ethereum leak detector [#1727](trailofbits/manticore#1727) ### Native * Support for ARM modified-immediate encodings [#1638](trailofbits/manticore#1638) * Support for `/proc/self/maps` [#1639](trailofbits/manticore#1639) * Support for `llseek` [#1640](trailofbits/manticore#1640) * Support for `arm_fadvise64_64` [#1648](trailofbits/manticore#1648) * Allow symbolic sockets in `accept` [#1618](trailofbits/manticore#1618) * Fixes to `open` [#1657](trailofbits/manticore#1657) * Overhauled filesystem emulation [#1673](trailofbits/manticore#1673) * Fixed system call argument concretization [#1697](trailofbits/manticore#1697) * **[Added API]** Add a symbolic model for `strcpy` [#1681](trailofbits/manticore#1681) ### WASM * Delay branch condition concretization for better coverage [#1641](trailofbits/manticore#1641) ### Other * **[Added API]** Added a snapshot system [#1710](trailofbits/manticore#1710) * Transparent compression for state files [#1624](trailofbits/manticore#1624) * Unify around singleton interface for solver [#1649](trailofbits/manticore#1649) * Use `__slots__` to reduce memory usage in expression system [#1635](trailofbits/manticore#1635) * **[Removed API]** Removed `policy` argument from ManticoreBase, added `outputspace_url` to optionally separate working files from output files [#1651](trailofbits/manticore#1651) * Disable broken `get_related` logic [#1674](trailofbits/manticore#1674) * Disable flaky Z3 tactics [#1691](trailofbits/manticore#1691) * Remove Keystone engine from dependencies [#1684](trailofbits/manticore#1684) * Improved error messages [#1632](trailofbits/manticore#1632), [#1704](trailofbits/manticore#1704) * Made ConstraintSets hashable [#1703](trailofbits/manticore#1703) * Added system to dynamically enable/disable plugins [#1696](trailofbits/manticore#1696) [#1708](trailofbits/manticore#1708) * Re-establish support for Yices and CVC4 [#1714](trailofbits/manticore#1714) * Improved constant folding and constraint set slicing [#1706](trailofbits/manticore#1706) ## 0.3.3 - 2020-01-30 Thanks to our external contributors! - [catenacyber](https://github.com/trailofbits/manticore/commits?author=catenacyber) ### Ethereum * **[added API]** Flag to only generate alive states when finalizing Manticore [#1554](trailofbits/manticore#1554) * Fix gas check [#1587](trailofbits/manticore#1587) ### Native * **[added API]** Add post-instruction hooks [#1579](trailofbits/manticore#1579) * Fix issue with re-using stdio file descriptors after they'd been closed [#1604](trailofbits/manticore#1604) ### WASM * **[added API]** getattr-style calls for WASM functions [#1578](trailofbits/manticore#1578) * **[changed API]** Pass state to function calls instead of constraint sets [#1578](trailofbits/manticore#1578) * **[added API]** Added read/write helper methods to memory instances [#1589](trailofbits/manticore#1589) ### Other * **[added API]** Added streamlined state serialization interface [#1596](trailofbits/manticore#1596) * Fixed Z3 version parsing [#1551](trailofbits/manticore#1551) * Unique names for ArrayVars [#1552](trailofbits/manticore#1552) * Improve pickling and multiprocessing compatibility [#1583](trailofbits/manticore#1583) * Fix SMTLib visitor bug that broke the example tests [#1577](trailofbits/manticore#1577) * Optimize MinMax SMTLib operations [#1599](trailofbits/manticore#1599) ## 0.3.2 - 2019-11-11 Thanks to our external contributors! - [Srinivas11789](https://github.com/trailofbits/manticore/commits?author=Srinivas11789) - [catenacyber](https://github.com/trailofbits/manticore/commits?author=catenacyber) - [Boyan-MILANOV](https://github.com/trailofbits/manticore/commits?author=Boyan-MILANOV) ### Ethereum * **[added API]** Use higher-level test generation to symbolically execute SHA3 [#1526](trailofbits/manticore#1526) * **[added API]** Added fast unsound SHA3 strategy [#1549](trailofbits/manticore#1549) * **[added API]** Added plugin for discarding states without changes to storage [#1507](trailofbits/manticore#1507) * **[fixed API]** Fix `ADDMOD` and `MULMOD` [#1531](trailofbits/manticore#1531) * Warn on missing bytecode [#1534](trailofbits/manticore#1534) * Simplifiy PC upon modification [#1523](trailofbits/manticore#1523) ### Native * Better memory tests ([#1506](trailofbits/manticore#1506), [1524](trailofbits/manticore#1524)) * Memory IO performance improvements [#1509](trailofbits/manticore#1509) * **[added API]** Expose ELF dynamic load addresses [#1515](trailofbits/manticore#1515) * Optimize instruction decoding ([#1522](trailofbits/manticore#1522), [#1527](trailofbits/manticore#1527)) * Add partial support for `recvfrom` syscall [#1514](trailofbits/manticore#1514) * **[fixed API]** Add `will_write_memory` event to `write_bytes` [#1535](trailofbits/manticore#1535) * Update supported Unicorn version [#1536](trailofbits/manticore#1536) * Fix file pointer leak in ELF interpreter [#1538](trailofbits/manticore#1538) * Deduplicate socket symbol names [#1542](trailofbits/manticore#1542) * Improve environment variable parsing [#1545](trailofbits/manticore#1545) * **[fixed API]** Reduce chance of orphaned `did_execute_instruction` event [#1529](trailofbits/manticore#1529) ### WASM * **[added API]** Added initial support for webassembly [#1495](trailofbits/manticore#1495) ### Other * Incorporate type checking (mypy) into CI [#1544](trailofbits/manticore#1544) * Fixes to smtlib ([#1512](trailofbits/manticore#1512), [#1511](trailofbits/manticore#1511)) * Remove runtime type checking from smtlib to improve performance [#1543](trailofbits/manticore#1543) * Logging improvements ([#1518](trailofbits/manticore#1518), [#1520](trailofbits/manticore#1520)) * Simplify unsigned division constant folding [#1530](trailofbits/manticore#1530) * Improve signed division logic [#1540](trailofbits/manticore#1540) * **[changed API]** Move to manticore-specific exception types [#1537](trailofbits/manticore#1537) * **[changed API]** Save profiling data in the workspace instead of the current directory [#1539](trailofbits/manticore#1539) ## 0.3.1 - 2019-08-06 Thanks to our external contributors! - [arcz](https://github.com/trailofbits/manticore/commits?author=arcz) ### Ethereum * Smart contracts are now compiled using [Crytic-Compile](https://github.com/crytic/crytic-compile) [#1406](trailofbits/manticore#1406) * Added detector for strict comparisons to BALANCE [#1481](trailofbits/manticore#1481) * Added bitshift instructions [#1498](trailofbits/manticore#1498) * Added stub for STATICCALL (does not enforce static nature) [#1494](trailofbits/manticore#1494) * Updated EVM Examples [#1486](trailofbits/manticore#1486) ### Native * Fixed `getdents` syscall [#1472](trailofbits/manticore#1472) * Fixed state merging examples [#1482](trailofbits/manticore#1482) * Support LSR.W on ARMV7 [#1363](trailofbits/manticore#1363) * Fixed CrackMe Example [#1502](trailofbits/manticore#1502) * Optimize CMPXCHG8B [#1501](trailofbits/manticore#1501) * Added `fast_crash` configuration setting that causes Manticore to immediately produce a finding on memory unsafety [#1485](trailofbits/manticore#1485) ### Other * **[changed API]** Moved `issymbolic` into SMTLib to improve performance [#1456](trailofbits/manticore#1456) * Refactored API Docs [#1469](trailofbits/manticore#1469) * Fixed `FileNotFound` Error on state loading [#1480](trailofbits/manticore#1480) ## 0.3.0 - 2019-06-06 Thanks to our external contributors! - [catenacyber](https://github.com/trailofbits/manticore/commits?author=catenacyber) - [binaryflesh](https://github.com/trailofbits/manticore/commits?author=binaryflesh) ### Major Changes ##### Executor Refactor ([#1385](trailofbits/manticore#1385)) We've completed a major refactor of the core executor that reorganizes Manticore's state machine to be more amenable toward use with the multiprocesssing module. This refactor introduces some small API changes: * One must explicitly call the `finalize` method to dump test cases from a run * The `will_start_run` event has been renamed to `will_run` * The `solver` module requires explicitly accessing the Z3Solver singleton. `from manticore.core.smtlib import solver` becomes: ```python from manticore.core.smtlib.solver import Z3Solver solver = Z3Solver.instance() ``` * `manticore.running_states` has been renamed to `manticore._busy_states` For more information about changes to the state machine, see [the diagram in core/manticore.py](https://github.com/trailofbits/manticore/blob/451965f03a5e0d6766e499bf3246e4796b35638f/manticore/core/manticore.py#L132-L239) ##### Blacken ([#1438](trailofbits/manticore#1438)) We've run the [`black`](https://black.readthedocs.io/en/stable/index.html) autoformatter on the master branch of Manticore, and added a check for compliance to our CI. To ensure your code is properly formatted, run `black -t py36 -l 100 .` in your Manticore directory before committing. ##### Support for statically-linked AArch64 binaries ([#1424](trailofbits/manticore#1424)) Contractor [nkaretnikov](https://github.com/trailofbits/manticore/commits?author=nkaretnikov) spent several months adding support for AArch64 on Linux. As this is a brand new architecture, we've left in most of the debugging assertions, which may slow it down slightly. We look forward to getting feedback on this architecture so we can eventually remove the debugging assertions. ### Ethereum * Added Symbolic EVM Tests for the Frontier fork. Note that we don't support any other forks (i.e. Constantinople) yet. ([#1431](trailofbits/manticore#1431), [#1441](trailofbits/manticore#1441)) * **[fixed API]** Fixed relative paths for .sol files ([#1393](trailofbits/manticore#1393)) * **[fixed API]** Support dynamic parameters in constructors ([#1414](trailofbits/manticore#1414)) * Fixed detector failure when PC is symbolic ([#1395](trailofbits/manticore#1395)) * Transfers from etherless contracts no longer report STOP ([#1392](trailofbits/manticore#1392)) ### Native * Added stubs for missing system calls & downgraded most missing calls from exceptions to warnings ([#1384](trailofbits/manticore#1384)) * Fixed DECREE magic pages ([#1413](trailofbits/manticore#1413)) * Store x86 registers in a set instead of a list ([#1415](trailofbits/manticore#1415)) * Fix register boundary check for non-x86 architectures ([#1429](trailofbits/manticore#1429)) * Support `movhps` on x86 ([#1444](trailofbits/manticore#1444)) ### Other * Only publish events when there is at least one subscriber ([#1388](trailofbits/manticore#1388)) * Added sandshrew example ([#1396](trailofbits/manticore#1396)) * Updated Unicorn to track latest master ([#1440](trailofbits/manticore#1440)) * **[fixed API]** Now respects coverage file argument ([#1442](trailofbits/manticore#1442)) ## 0.2.5 - 2019-03-18 Thanks to our external contributors! - [werew](https://github.com/trailofbits/manticore/commits?author=werew) - [NicolaiSoeborg](https://github.com/trailofbits/manticore/commits?author=NicolaiSoeborg) - [Joool](https://github.com/trailofbits/manticore/commits?author=Joool) ### Ethereum * **[added API]** `json_create_contract` - support creating EVM contracts from Truffle JSON artifacts ([#1376](trailofbits/manticore#1376)) * **[changed API]** Moved default gas value to config module ([#1346](trailofbits/manticore#1346)) * **[fixed API]** Fixed account creation with a code field ([#1371](trailofbits/manticore#1371)) * **[fixed API]** Fixed an incorrect attribute in `last_return` ([#1341](trailofbits/manticore#1341)) * **[refactor]** Inlined get_possible solutions function as it's only used once ([#1372](trailofbits/manticore#1372)) * Fixed `_check_jumpdest` when run with detectors - this bug could lead to not detecting an int overflow due to tainting made by another detector ([#1347](trailofbits/manticore#1347)) * Made findings print addresses in hex ([#1339](trailofbits/manticore#1339)) ### Native * **[added API]** Added Unicorn preloading, for quickly performing concrete emulation until a target address is reached. ([#1356](trailofbits/manticore#1356)) * Fixed incorrect return value in `sys_lseek` ([#1355](trailofbits/manticore#1355)) * Added check for missing native packages ([#1367](trailofbits/manticore#1367)) ### Other * **[added API]** Added context managers for the config module, allowing for temporary configurations ([#1345](trailofbits/manticore#1345)) * Updated Capstone to 4.0.1 ([#1312](trailofbits/manticore#1312)) * Embedded parsetab.py so users no longer need to generate it ([#1383](trailofbits/manticore#1383)) ## 0.2.4 - 2019-01-10 ### Ethereum * **[added API]** Fixed VerboseTrace plugin ([#1305](trailofbits/manticore#1305)) and added VerboseTraceStdout plugin ([#1305](trailofbits/manticore#1305)): those can be used to track EVM execution (`m.regiser_plugin(VerboseTraceStdout())`) * **[changed API]** Made gas calculation faithfulness configurable: this way, you can choose whether you respect or ignore gas calculations with `--evm.oog <opt>` (see `--help`); also, the gas calculations has been decoupled into its own methods ([#1279](trailofbits/manticore#1279)) * **[changed API]** Changed default gas to 3000000 when creating contract ([#1332](trailofbits/manticore#1332)) * **[changed API]** Launching manticore from cli will display all registered plugins ([#1301](trailofbits/manticore#1301)) * Fixed a bug where it wasn't possible to call contract's function when its name started with an underscore ([#1306](trailofbits/manticore#1306)) * Fixed `Transaction.is_human` usage and changed it to a property ([#1323](trailofbits/manticore#1323)) * Fixed `make_symbolic_address` not preconstraining the symbolic address to be within all already-known addresses ([#1318](trailofbits/manticore#1318)) * Fixed bug where a terminated state became a running one if `m.running_states` or `m.terminated_states` were generated ([#1326](trailofbits/manticore#1326)) ### Native * **[added API]** Added symbol resolution feature, so it is possible to grab a symbol address by using `m.resolve(symbol)` ([#1302](trailofbits/manticore#1302)) * **[changed API]** The `stdin_size` CLI argument has been moved to config constant and so has to be passed using `--native.stdin_size` instead of `--stdin_size` ([#1337](trailofbits/manticore#1337)) * Speeded up Armv7 execution a bit ([#1313](trailofbits/manticore#1313)) * Fixed `sys_arch_prctl` syscall when wrong `code` value was passed and raise a NotImplementedError instead of asserting for not supported code values ([#1319](trailofbits/manticore#1319)) ### Other * **[changed API]** Fixed missing CLI arguments that came from config constants - note that `timeout` has to be passed using `core.timeout` now ([#1337](trailofbits/manticore#1337)) * We now explicitly require Python>=3.6 when using CLI or when importing Manticore ([#1331](trailofbits/manticore#1331)) * `__main__` now fetches manticore version from installed modules ([#1310](trailofbits/manticore#1310)) * Refactored some of the codebase (events [#1314](trailofbits/manticore#1314), solver [#1334](trailofbits/manticore#1334), tests [#1308](trailofbits/manticore#1308), py2->py3 [#1307](trailofbits/manticore#1307), state/platform [#1320](trailofbits/manticore#1320), evm stuff [#1329](trailofbits/manticore#1329)) * Some other fixes and minor changes ## 0.2.3 - 2018-12-11 Thanks to our external contributors! - [NeatMonster](https://github.com/NeatMonster) - [evgeniuz](https://github.com/evgeniuz) - [stephan-tolksdorf](https://github.com/stephan-tolksdorf) - [yeti-detective](https://github.com/yeti-detective) - [PetarMI](https://github.com/PetarMI) - [hidde-jan](https://github.com/hidde-jan) - [catenacyber](https://github.com/catenacyber) ### Added - Support for ARM THUMB instructions: ADR, ADDW, SUBW, CBZ, TBB, TBH, STMDA, STMDB - `State.solve_minmax()` API for querying a BitVec for its min/max values - New SMTLIB optimization for simplifying redundant concat/extract combinations; helps reduce expression complexity, and speed up queries - Ethereum: `--txpreconstrain` CLI flag. Enabling this avoids sending ether to nonpayable functions, primarily avoiding exploration of uninteresting revert states. - Research memory model (LazySMemory) allowing for symbolic memory indexing to be handled without concretization (opt in, currently for research only) ### Changed - Linux/binary analysis has been moved to `manticore.native`, `manticore.core.cpu` has been moved to `manticore.native.cpu`. Please update your imports. - The binary analysis dependencies are now not installed by default. They can be installed with `pip install manticore[native]`. This is to prevent EVM users from installing binary dependencies. - The symbolic `stdin_size` is now a config variable (in `main` config group) with a default of 256 (it was like this before). - `ManticoreEVM.generate_testcase()` 'name' parameter is now optional - Manticore CLI run on a smart contract will now use all detectors by default (detectors can be listed with --list-detectors, excluded with --exclude <detectors> or --exclude-all) - Misusing the ManticoreEVM API, for example by using old keyword arguments that are not available since some versions (like ManticoreEVM(verbosity=5)) will now raise an exception instead of not applying the argument at all. ### Fixed - Ethereum: Fixed CLI timeout support - Numerous EVM correctness fixes for Frontier fork - Fixed handling of default storage and memory in EVM (reading from previously unused cell will return a zero now) - ARM THUMB mode, Linux syscall emulation fixes - Creation of multiple contracts with symbolic arguments (ManticoreEVM.solidity_create_contract with args=None fired more than once failed before) ### Removed - `Manticore.evm` static method ## 0.2.2 - 2018-10-30 Thanks to our external contributors! - [charliecjung](https://github.com/charliecjung) - [redyoshi49q](https://github.com/redyoshi49q) - [yeti-detective](https://github.com/yeti-detective) - [Srinivas11789](https://github.com/srinivas11789) - [stephan-tolksdorf](https://github.com/stephan-tolksdorf) - [catenacyber](https://github.com/catenacyber) - [MJ10](https://github.com/MJ10) ### Added - New API for generating a testcase only if a certain condition can be true in the state. Useful for conveniently checking an invariant in a state, and (`ManticoreEVM.generate_testcase(..., only_if=)`) generating a testcase if it can be violated. - New `constrain=` optional parameter for `State.solve_one` and `State.solve_buffer`. After solving for a symbolic variable, mutate the state by applying that solution as a constraint. Useful if concretizing a few symbolic variables, and later concretizations should take into account previously solved for values. - `ManticoreEVM.human_transactions` top level API. Mirrors `ManticoreEVM.transactions`, but does not contain any internal transactions. - Emit generated transaction data in human readable format (JSON) - Warning messages if number of passed arguments to a Solidity function is inconsistent with the number declared - CLI support for the ReentrancyAdvancedDetector - Colored CLI output - Configuration system. Allows configuration options to be specified in a config file. New configurations are available, notably including solver parameters such as solver timeout, and memory limits. - Support for some unimplemented x86 XMM instructions - Customizable symbolic stdin input buffer size - Support for [Etheno](https://github.com/trailofbits/etheno) - `RaceConditionDetector` that can be used to detect transaction order dependencies bugs ### Changed - Improve the DetectExternalCallAndLeak detector and reduce false positives - Numerous improvements and changes to the SolidityMetadata API - Ethereum contract addresses are no longer random, but are deterministically calculated according to the Yellow Paper - Manticore no longer supports contracts with symbolic addresses creating new contracts. This is a consequence of supporting determinstic contrat address calculation. There are plans for reenabling this capability in a future release. ### Deprecated - Several SolidityMetadata APIs: `.get_hash()`, `.functions`, `.hashes` ### Fixed - Numerous fixes and enhancements to the Ethereum ABI implementation - Better handling of overloaded functions in SolidityMetadata, and other bug fixes - Fixes for the FilterFunctions plugin - Fixes for symbolic SHA3 handling - Many EVM correctness/consensus fixes - Numerous spelling errors ## 0.2.1.1 - 2018-09-01 In this release, the codebase has been relicensed under the AGPLv3 license. Please [contact us](opensource@trailofbits.com) if you're looking for an exception to these terms! Thanks to our external contributors! - [s0b0lev](https://github.com/s0b0lev) - [redyoshi49q](https://github.com/redyoshi49q) ### Added - Full suite of Ethereum detectors - Selfdestruct (`--detect-selfdestruct`): Warns if a selfdestruct instruction is reachable by the user - Ether Leak (`--detect-externalcall`): Warns if there is a call to the user, or a user controlled address, and ether can be sent. - External Call (`--detect-externalcall`): Warns if there is a call to the user, or a user controlled address. - Reentrancy (`--detect-reentrancy`): Warns if there is a change of storage state after a call to the user, or a user controlled address, with >2300 gas. This is an alternate implementation enabled in the CLI. The previous implementation is still available for API use (`DetectReentrancyAdvanced`). - Delegatecall (`--detect-delegatecall`): Warns if there is a delegatecall to a user controlled address, or to a user controlled function. - Environmental Instructions (`--detect-env`): Warns if certain instructions are used that can be potentially manipulated. Instructions: BLOCKHASH, COINBASE, TIMESTAMP, NUMBER, DIFFICULTY, GASLIMIT, ORIGIN, GASPRICE. - New Ethereum command line flags - `--no-testcases`: Do not generate testcases for discovered states - `--txnoether`: Do not make the transaction value symbolic in executed transactions - SMTLIB: Advanced functionality for expression migration. Expressions from arbitrary constraint sets can be mixed to create arbitrary constraints, expressions are transparently migrated from constraint set to another, avoiding SMT naming collisions. ### Changed - Command line interface uses new reentrancy detector based on detection of user controlled call addresses ### Fixed - Ethereum: Support for overloaded solidity functions - Ethereum: Significantly improved ability to create symbolic variables and constraints at the global level - Ethereum: Improved gas support - State serialization improvements and fixes ## 0.2.0 - 2018-08-10 In this release, the codebase has been ported to Python 3.6, which is a breaking change for API clients. Beginning with 0.2.0, client programs of Manticore must be compatible with Python 3.6. Thanks to our external contributors! - [ianklatzco](https://github.com/ianklatzco) - [devtty1er](https://github.com/devtty1er) - [catenacyber](https://github.com/catenacyber) ### Added - Ethereum: More flexibility for Solidity compilation toolchains - Ethereum: Detectors for unused return value, reentrancy - Ethereum: Support for Solidity `bytesM` and `bytes` types - Ethereum: Beta API for preconstraining inputs (`ManticoreEVM.constrain`) - Improved performance for smtlib module - Ability to transparently operate on bytearray and symbolic buffer (ArrayProxy) types (e.g: concatenate, slice) ### Changed - **Codebase has been entirely ported to Python 3.6+** - Ethereum: `ManticoreEVM.make_symbolic_value()` can be size adjustable - Ethereum: Ethereum ABI (`manticore.ethereum.ABI`) API refactor, including real Solidity prototype parser - Ethereum: Improved APIs for accessing transaction history - Ethereum: Significant internal refactor ### Fixed - Linux: Bugs related to handling of closed files - Ethereum: Handling of symbolic callers/addresses - Ethereum: Handling of gas handling on CALL instructions - Various smtlib/expression fixes ### Removed - Support for Python 2 - EVM disassembler/assembler module (EVMAsm) has been removed and separately released as [pyevmasm](https://github.com/trailofbits/pyevmasm) - Experimental support for Binary Ninja IL emulation ## 0.1.10 - 2018-06-22 Thanks to our external contributors! - [khorben](https://github.com/khorben) - [catenacyber](https://github.com/catenacyber) - [dwhjames](https://github.com/dwhjames) - [matiasb](https://github.com/matiasb) - [reaperhulk](https://github.com/reaperhulk) - [lazzarello](https://github.com/lazzarello) ### Added - ARM: New instructions to better support Raspberry Pi binaries (UTXH, UQSUB8) - Linux: Can use `--env` and `LD_LIBRARY_PATH` to specify alternate ELF interpreter locations for dynamic binaries - Linux: Partial chroot(2) and fork(2) models - Initial support for NetBSD hosts - Ethereum: `--avoid-constant` cli argument to enable heuristics to avoid unnecessary exploration of constant functions ### Changed - Ethereum detectors are now opt-in, via cli flags: `--detect-overflow`, `--detect-invalid`, `--detect-uninitialized-memory`, `--detect-uninitialized-storage`, `--detect-all` - Ethereum: Complete internal refactor. - Model memory using smtlib arrays to better support symbolic indexing - Numerous internal API improvements - Better symbolic gas support - More advanced overflow detection heuristics - Account names, scripts can assign names to accounts or contracts - Better ABI serializer/deserializer for canonical types, supports tuples/structs and recursive types - State list iterations improvements, modifications to state persist - Symbolic caller, address, value and data in transactions ### Fixed - Linux: Generate concretized file content for symbolic files - Linux: Fixes in various syscall models (brk, stat*), and miscellaneous fixes - Ethereum: Inaccurate transaction history in some cases

jimpo force-pushed the wasm-branch-conditions branch 2 times, most recently from e8787c0 to 32e4407 Compare March 28, 2020 20:32

ehennenfent self-assigned this Apr 1, 2020

ehennenfent changed the title ~~Fix bug with Wasm branching~~ Delay WASM Branch Condition Concretization Apr 1, 2020

ehennenfent reviewed Apr 1, 2020

View reviewed changes

jimpo force-pushed the wasm-branch-conditions branch 3 times, most recently from be1ecaf to b1f4a60 Compare April 6, 2020 17:25

jimpo added 13 commits April 6, 2020 22:08

Fix typos.

28b01bd

Create StackItem type alias.

236f625

Fix for wasm if and br_if execution.

835a89f

The engine raises a ConcretizeCondition exception to determine the branch path and constrain the state minimally.

Remove unnecessary bitwise AND.

cd83f3f

It's unnecessary because c_int32 truncates to 32 bits and it's weird because this bitwise and isn't there for I64.

Failing tests demonstrating bug in br_table and call_indirect.

336833c

Fix bugs with br_table and call_indirect using concrete conditions.

47437f3

Fix typing errors.

1c93d71

Try to get wasm tests passing.

739db26

Move advice conditions from Stack to separate structure.

fee7aa4

Fix so that multiple conditions may be concretized.

6ab81dc

Update incorrect comment on StateBase.concretize.

9b896fc

Appease type checker.

c9b0c09

jimpo force-pushed the wasm-branch-conditions branch from b1f4a60 to c9b0c09 Compare April 7, 2020 05:09

ehennenfent approved these changes Apr 7, 2020

View reviewed changes

ehennenfent merged commit 8fcdf0d into trailofbits:master Apr 7, 2020

jimpo deleted the wasm-branch-conditions branch April 8, 2020 03:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Delay WASM Branch Condition Concretization #1641

Delay WASM Branch Condition Concretization #1641

Uh oh!

jimpo commented Mar 28, 2020 •

edited

Loading

Uh oh!

CLAassistant commented Mar 28, 2020 •

edited

Loading

Uh oh!

ehennenfent left a comment

Uh oh!

ehennenfent Apr 1, 2020

Uh oh!

jimpo Apr 2, 2020

Uh oh!

ehennenfent Apr 1, 2020

Uh oh!

ehennenfent Apr 1, 2020

Uh oh!

jimpo Apr 2, 2020

Uh oh!

ehennenfent Apr 2, 2020 •

edited

Loading

Uh oh!

jimpo commented Apr 2, 2020

Uh oh!

ehennenfent commented Apr 2, 2020 •

edited

Loading

Uh oh!

ehennenfent commented Apr 6, 2020

Uh oh!

ehennenfent commented Apr 7, 2020

Uh oh!

jimpo commented Apr 7, 2020

Uh oh!

ehennenfent commented Apr 7, 2020

Uh oh!

Uh oh!

Delay WASM Branch Condition Concretization #1641

Delay WASM Branch Condition Concretization #1641

Uh oh!

Conversation

jimpo commented Mar 28, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

CLAassistant commented Mar 28, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ehennenfent left a comment

Choose a reason for hiding this comment

Uh oh!

ehennenfent Apr 1, 2020

Choose a reason for hiding this comment

Uh oh!

jimpo Apr 2, 2020

Choose a reason for hiding this comment

Uh oh!

ehennenfent Apr 1, 2020

Choose a reason for hiding this comment

Uh oh!

ehennenfent Apr 1, 2020

Choose a reason for hiding this comment

Uh oh!

jimpo Apr 2, 2020

Choose a reason for hiding this comment

Uh oh!

ehennenfent Apr 2, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jimpo commented Apr 2, 2020

Uh oh!

ehennenfent commented Apr 2, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ehennenfent commented Apr 6, 2020

Uh oh!

ehennenfent commented Apr 7, 2020

Uh oh!

jimpo commented Apr 7, 2020

Uh oh!

ehennenfent commented Apr 7, 2020

Uh oh!

Uh oh!

jimpo commented Mar 28, 2020 •

edited

Loading

CLAassistant commented Mar 28, 2020 •

edited

Loading

ehennenfent Apr 2, 2020 •

edited

Loading

ehennenfent commented Apr 2, 2020 •

edited

Loading