Fix constant folding & constraint set slicing #1706

feliam · 2020-05-13T21:59:48Z

Improved constant folding simplifier ( several bugfixes related with signed ints vs. bitvectors)
This PR contains a single testcase that reproduces Flaw in __get_related core logic #1679 And its "fix"
ConstraintSet slicing is optional and disabled by default.

feliam · 2020-05-15T19:49:16Z

manticore/core/smtlib/constraints.py

@@ -146,7 +146,7 @@ def __get_related(self, related_to=None):
                            break

                    variables = get_variables(constraint)
-                    if related_variables & variables:
+                    if related_variables & variables or not variables:


With this added "this" test passes with both get_related enabled and disabled

As long as both are passing, let's set the default back to True

Well I'm not 100% This single testcase representes all possible fails explained in issue #1679

Devils advocate, here... What if related_to is A and constraint is something like B && !B, i.e., constraint is unsatisfiable and has variables, but they do not overlap with those of related_to?

Yes get_related should work only on previously feasible path contraints.
If you have feasible A & B & C and want to check if B \/ C can be True then you do not need to bother the solver with the A.

Yes. I know it is not enforced.
We should make it a pre-condition or attempt to solve the full constraint set and trust that some cache magic prevents it to do the solving over the whole thing again and again.

Yes. I know it is not enforced.
We should make it a pre-condition or attempt to solve the full constraint set and trust that some cache magic prevents it to do the solving over the whole thing again and again.

I don't know how reasonable this approach is. __get_related is called by to_string, and to_string is something that one might reasonably call to debug a bad constraint set.

Moreover, to_string is called by can_be_true:

manticore/manticore/core/smtlib/solver.py

Line 433 in 2c90ee0

self._reset(constraints.to_string())

So there's a little bit of a chicken-and-egg problem here.

If it were up to me, I would not insist that __get_related be called on only satisfiable constraint sets.

Many constraints do not overlap in terms of the memory they reference. Constraint independence divides constraint sets into disjoint independent subsets based on the symbolic variables and memory cells they reference. By explicitly tracking these subsets, it can frequently eliminate irrelevant constraints prior to sending it to the solver.
For example, given the constraint set {i < j, j < 20, k > 0}, a query of whether i = 20 just requires the first two constraints. This was first explained in [EXE] https://web.stanford.edu/~engler/exe-ccs-06.pdf

We can move the optimizations/transformations that are controlled via kwargs in the to_string() to a different ConstraintSet method. Like slice_related_to(..) and make_bindings so it is done more explicit.

If the problem is to print a ConstraintSet for debugging you can just just do not slice the ConstraintSet.

print (str(cs))

There is also a forgotten pretty_print for expressions.

Fwiw, I use the pretty_print all the time while debugging

Moved the disabled get_related as a special method of a ConstraintSet to slice it when the user wants it.
Also added "some" tests for it.

smoelius · 2020-05-19T01:30:02Z

tests/ethereum/test_regressions.py

+        from manticore.core.smtlib.visitors import translate_to_smtlib
+        from manticore.core.smtlib import ConstraintSet, Z3Solver, Operators, BitVecConstant
+        import pickle, sys
+        filename = os.path.abspath(os.path.join(DIRPATH, "data", "ErrRelated.pkl.gz"))


What's in this file?

Also, should this test be in ethereum directory?

My guess is that it's a state that exhibits the get_related bug, but pickled and gzipped so that we don't need to construct it from the source code.

Yes. Not the state but the ConstraintSet that showed the problem. This is not really ethereum specific.

Is it expensive to construct from source? A binary isn't easy to peruse over the web, for example.

I saved the constraint and the constraintset that found to have trouble with old get_related.
I re build the constraint but the constraintset was big ish so I left it all binary and obscure.
Its a hack. I'll be much better to produce the testcases ourselves.
As it is still disabled by default I could remove this unintelligible test.

tests/ethereum/test_regressions.py

ekilmer

Looking good! Just a few type more type annotations we could add and some questions/comments. 👍

manticore/core/smtlib/constraints.py

manticore/core/smtlib/solver.py

manticore/core/smtlib/visitors.py

tests/other/test_smtlibv2.py

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

…to dev-get-related

manticore/core/smtlib/constraints.py

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

…to dev-get-related

manticore/core/smtlib/solver.py

ehennenfent

Hooray, the tests are passing! We've both been over this one in detail, so I think we should merge it before it grows any larger. As noted at the meeting, we should still fix the Rust test that was causing sporadic CI failures, but we'll do that in a separate PR.

* master: Create a model for strncpy (#1770) Add doc, fix output bugs (#1769) Update EVM usage example (#1772) New working model of strlen (#1725) Typo (#1768) Specialized iterative serialization for Array (#1756) Enable nightly uploads to PyPI (#1757) Manticore 0.3.4 (#1720) Manticore verifier (#1717) Nightly MacOS Tests (#1614) Remove/procrastinate solver query in ether leak detector (#1727) Fix constant folding & constraint set slicing (#1706)

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

feliam added 3 commits May 13, 2020 18:48

Add ONE failing test

0cd1bc5

Fix test

609a37e

Try fix get-related

b29f3ac

feliam marked this pull request as ready for review May 13, 2020 22:40

feliam commented May 15, 2020

View reviewed changes

feliam requested review from ehennenfent and smoelius May 15, 2020 19:49

smoelius reviewed May 19, 2020

View reviewed changes

feliam commented May 29, 2020

View reviewed changes

tests/ethereum/test_regressions.py Outdated Show resolved Hide resolved

feliam added 6 commits June 2, 2020 17:29

Move regression to other

79aa5cc

blkn

7339eb9

blkn

c121c38

Move get related

3ff6b95

Merge branch 'master' into dev-get-related

02b4c69

CC

00e8199

feliam force-pushed the master branch from 3ff6b95 to 4495b6f Compare June 5, 2020 17:31

feliam added 4 commits June 5, 2020 16:08

fix concolic

6b7f671

lint

6732eb2

DivByZero default to zero

4adeac2

blkn

7565b4a

ekilmer reviewed Jun 5, 2020

View reviewed changes

feliam and others added 5 commits June 5, 2020 17:55

Update manticore/core/smtlib/solver.py

1680397

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

Update manticore/core/smtlib/constraints.py

cbe55b9

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

Update manticore/core/smtlib/constraints.py

315ef64

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

remove odd string

6155a4d

Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…

38dbfd6

…to dev-get-related

ekilmer reviewed Jun 5, 2020

View reviewed changes

manticore/core/smtlib/constraints.py Outdated Show resolved Hide resolved

feliam and others added 3 commits June 5, 2020 18:12

lint

1491cbd

mypy lint

264eb04

Update manticore/core/smtlib/visitors.py

e0130a4

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

Strip left-in print debugging

f7fb8bb

MatthewARinehart added this to Review in progress in Manticore Jun 11, 2020

MatthewARinehart marked this pull request as draft June 11, 2020 20:56

MatthewARinehart moved this from Review in progress to In progress in Manticore Jun 11, 2020

ehennenfent linked an issue Jun 11, 2020 that may be closed by this pull request

Flaw in __get_related core logic #1679

Closed

feliam added 2 commits June 11, 2020 18:27

fix wasm

2f5d4d2

Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…

18064f8

…to dev-get-related

feliam marked this pull request as ready for review June 11, 2020 21:43

feliam added 11 commits June 11, 2020 18:59

Fix

52d8eb4

REmove get_related from the default path and fix arm test

f1dfb80

blkn

d5b577e

fix related to tests

79b42ed

blkn

ec8489f

Fix bug in test and disable debug messages in Solver

2113a73

smtlib config to disable multiple check-sat in newer z3

c2a21ba

Disable log test and fix merging poc vs variable migration

f87e1e2

blkn

2eb630d

Avoid exception in some callbacks

8818ea3

can_raise at did_will

27db1b8

feliam changed the title ~~Dev get related~~ Fix constant folding & constraint set slicing Jun 15, 2020

ehennenfent reviewed Jun 16, 2020

View reviewed changes

manticore/core/smtlib/solver.py Outdated Show resolved Hide resolved

feliam added 2 commits June 16, 2020 16:23

slightly better z3 onfiguration

64a03a7

lint

380fb31

ehennenfent approved these changes Jun 17, 2020

View reviewed changes

Manticore automation moved this from In progress to Reviewer approved Jun 17, 2020

feliam merged commit 099dc47 into master Jun 17, 2020

Manticore automation moved this from Reviewer approved to Done Jun 17, 2020

feliam deleted the dev-get-related branch June 17, 2020 00:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix constant folding & constraint set slicing #1706

Fix constant folding & constraint set slicing #1706

feliam commented May 13, 2020 •

edited

Loading

feliam May 15, 2020

ehennenfent May 15, 2020

feliam May 18, 2020

smoelius May 19, 2020

feliam May 19, 2020

feliam May 19, 2020

smoelius May 23, 2020

feliam May 26, 2020

ehennenfent May 28, 2020

feliam Jun 5, 2020

smoelius May 19, 2020

smoelius May 19, 2020

ehennenfent May 28, 2020

feliam May 28, 2020

smoelius May 28, 2020

feliam May 29, 2020

ekilmer left a comment

ehennenfent left a comment

Fix constant folding & constraint set slicing #1706

Fix constant folding & constraint set slicing #1706

Conversation

feliam commented May 13, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ekilmer left a comment

Choose a reason for hiding this comment

ehennenfent left a comment

Choose a reason for hiding this comment

feliam commented May 13, 2020 •

edited

Loading