13 Commits

Author SHA1 Message Date
feliam
8591bff45f EVM support (#521)
* WIP New Policy class

* WIP pubsub

* Update Signal tests

* EVM support - Wip

* EVM support - dependencies fixed

* EVM support - fix decree merge

* fix decode instrucion event

* Fix small bugs in evm opcodes (too many arguments + wrong LOG name) (#380)

Fix wrong call parameters + typo

* Fix Create/Call

* Fix depth

* Default fixed point in arithmetic simplifier

* small fixes from github comments

* Fix event decode_instruction signature

* wip wip

* Auto tests for evm

* New EVM tests

* Ran 9556  FAILED (failures=166, errors=8, skipped=62)

* Fix some arithmetic instructions

* Ran 9556  FAILED (failures=136, errors=8, skipped=62)

* More instructions - Optimizing symbolic memory

* Added gas to opcodes description - FIX DELEGATECALL POPS

* Add wip wallet example

* The tests

* Solidity constructors need argument after bytecode

* Simple integer overflow working

* Good merge

* Good good merge

* WIP manticore refactor

* Fix default old-style initial state

* context now working

* Fix context serialization

* Fix test models.  Can not set a state constraints

* typo

* A few typos (constraints setter) and use of public properties in internal methods

* Fix init wallet example

* State __init__ needs to initialize platform constraints

* Internal methods use internal properties

* Better attack modeling

* Better example layout

* Storage backup on CALL is now faster .. and correct

* Add LOG support

* Minimal SE test

* Added examples

* Send ether bugfix

* EVM: Fix wrong balance destination on CALL + decrease caller balance on CREATE

* New balance management

* Trying to maintain known hashes

* Known hash concretization policy

* CALLDATA max size bugfix

* Minimal SE example

* Remove evm tests

* add -> enqueue

* @m.init

* Fix workspace url

* Some test skipped

* Ad Fixme to platform specific stuff in State

* add -> enqueue

* Enqueue created state

* Fix m.init

Use a messy hack to adhere to the spec (callback func receive 1 state argument)

* Add _coverage_file ivar to Manticore

* Fix symbolic files

* remove extra enqueue

* Fixing __main__

* comments

* Fix visitors oddity

* setup merged

* remove duplicates and add pysha3

* Remove EVMTests import

* Refactor platform specific code out of ManticoreOutput (#505)

* Initial moving work

* Clean

* Make linux.generate_workspace_files work

* Fix

* clean

* Add test

* Test workspace for platform files

* Skip EVM cpu pretty print

* Remove bad import

* Fix coverage.py for testing

* Clean comment

* Comment hack

* Print evm cpu

* pretty print evm world instead of platform

* delet old scripts/examples

* delet old tests

* Remove z3 install script

* Array.max_size can be None, include check for that

* Rm unused _symbolic_files

add_symbolic_files was moved to linux, so this is not needed

* Rm unused args

* Import evm

* Rm dup function

* Rm stray prints

* Add docs for new classmethod apis

* minimal

* minimal example

* fix minimal

* Fair symbolic SHA3 handling

* Simple mapping example

* coverage example

* fix tests

* fix minimal

* Some eko fixes

* New SETH

* integer_overflow refactored

* Fixing the examples

* init_bytecode -> init
'

* Concrete reentrancy exampole

* concrete reentrancy selfdestruct

* Update minimal.py

* It's a new Minimal

* Integer overflow example

* New minimal

* minimal fix

* Examples last minute fixes

* Remove debug print

* add plugin.py

* Fixing event subscription

* remove temp params

* Remove param

* Update uncovered will_exec callback prototype

* Clean up debug output

* Automatically generated intruction tests

* Uninplemented instruction test removed

* Unused concretization policy removed

* Fixes enabling default bplugins

* solc from PATH

* Removed unused import

* Logger name updated
2017-10-17 19:47:20 -03:00
Mark Mossberg
1d8e051522 Fix state.generate_testcase (#451)
* Use correct event name

* Add test for state.generate_testcase

Test merely tests that this function publishes the 'will_generate_testcase' event

* Properly test; make sure the callback executes and error if not

This is the most convoluted unit test I've ever written.

* "better"
2017-08-14 14:44:53 -04:00
feliam
3b57c0d502 Fix context serialization (#425)
* Fix context serialization

* Fix test models.  Can not set a state constraints

* typo

* A few typos (constraints setter) and use of public properties in internal methods

* State __init__ needs to initialize platform constraints

* Internal methods use internal properties

* test_record_branches removed
2017-08-01 14:08:54 -03:00
Eric Hennenfent
51837df98b Add Taint Parameters (#414)
* Add taint args to buffer creation

Allows the `new_symbolic_buffer` and `symbolicate_buffer` functions to take keyword args for tainting. Defaults to frozenset in both cases.

* Add unit tests and ArrayProxy taint propery

Adds simple unit tests for tainted buffers. Added a property to the ArrayProxy class in smtlib.expression so that it's possible to access the taint of the proxied ArrayVariable.

* Updated docstrings
2017-07-28 11:58:25 -04:00
feliam
76357216da Pub-sub like events (#371)
* WIP New Policy class

* WIP pubsub

* Update Signal tests

* small fixes from github comments

* Fix event decode_instruction signature

* Good merge

* Good good merge

* Eventful class commented

* The million typos

* Code revision

* Fix tests for new mor strict Eventful
2017-07-27 19:41:08 -03:00
feliam
520a9be47d Dev - events (#341)
* Wip refactoring

* Executor and exceptions refactor wip wip

* Fixing all_insts auto tests

* Visited and generate testcase now at manticore api level

* Aggregating state statistics into executor statistics

* Wip refactoring

* Executor and exceptions refactor wip wip

* Fixing all_insts auto tests

* Visited and generate testcase now at manticore api level

* Aggregating state statistics into executor statistics

* forwarding events wip

* state setstate fix and setup_stack merge fix

* will_terminate_state fix and tests skipped

* Update all ConcretizeRegister and ConcretizeMemory

* Wip refactoring

* Executor and exceptions refactor wip wip

* Fixing all_insts auto tests

* Visited and generate testcase now at manticore api level

* Aggregating state statistics into executor statistics

* Wip refactoring

* Executor and exceptions refactor wip wip

* Fixing all_insts auto tests

* Visited and generate testcase now at manticore api level

* Aggregating state statistics into executor statistics

* forwarding events wip

* state setstate fix and setup_stack merge fix

* will_terminate_state fix and tests skipped

* Update all ConcretizeRegister and ConcretizeMemory

* Exceptions are crazy crazy crazy

* fix last merge

* Merge merge until it pass

* Instructions count default to 0

* will/did execute/emulate

* Delayed keybpoard interrupt now shutdowns nicely

* fix auto test generator x86

* Undo bad merge

* utterly hopeless

* basic working

* Fix merge bugs and github comments

* Remove unnecesary comment - github comments

* trace_item not used there

* model-platform and system.py fixed

* backup/restore to store/load -- cpu.instruction property

* Slightly better did/will naming and dynamic signal forwarding

* platform.constraints and cpu.instruction as properties

* Fix forward signals getattr

* set las decoded pc at decode_instruction() / reenable instruction_cache

* Signals name convention: did/will/on

* Forward normal signals

* Maintain last decoded pc in abstractcpu

* Changed context manager so it just wont raise interrupt

* Decree now forwards signals and sets constraints

* linux.SymbolicFile does not need to maintain constraints

* remove debbug print

* Assimilating some PR commets

* size_total == size

* better merge of manticore.py

* typo

* Forwarding only specified objects in signal arguments

* Fix few broken tests

* revert + merge

* remove some unused stuff from manticore()

* manticore context <-> executor context

* manticore context <-> executor context2

* context context context

* forgotten return

* Fix basix.arm

* arm bitwise fix

* fix context

* Comment 1

* Comment 2

* Comment 3

* Comment 4

* Comment 5

* Comment 6

* Fix (still needs refactor but it works) profiling

* Fix (still needs refactor but it works) profiling

* The forgotten bit

* Update tests to reflect current output

* Verbosity fix

* Fix verbosity test
2017-06-26 18:06:18 -03:00
Theofilos Petsios
e2c0414dca added _multiprocess_can_split_ directive (#351)
* added _multiprocess_can_split_ directive

* renamed Readme
2017-06-23 17:53:19 -04:00
Mark Mossberg
92eaf76236 Add strcmp model (#251)
* add models

* wip strcmp tests

* t

* Add some tests

* Better asserts

* More pythonic

* Add effectivene null test

* Handle symbolic pointer arguments
2017-05-17 11:44:10 -04:00
Mark Mossberg
e4a4916597 Rename os model terminology from "models" to "platforms" (#243)
* Rename

* rename in manticore.py

* rename in executor.py

* big rename

* big rename

* update changelog
2017-05-09 19:25:32 -04:00
Mark Mossberg
44d365ff4c Formalize API for constraining a State (#232)
* Rename state.add to state.constrain

* Update all uses of state.constrain

* Rm check param

* Added changelog

* Update changelog

* Update

* Minor clean
2017-05-05 13:31:43 -04:00
Yan
0b850dba40 Make unicorn be pull-based (#97)
* Enable simple ARM register concretization for Unicorn

* Add canonical_registers property to abstractcpu

* cpu to self

* Check for regs_access better

* Emulate a single instruction

* Bypass capstone 3.0.4 arm bug

* Dealing with capstone

* Temporary disable ASR and remobe BitVec.Bool from test

* WIP WIP debug prints WIP WIP

* Unicorn fallback working (using unicorn master)

* HAck to support unicorn 1.0.0

* WIP

* Unicorn hack to handle PC updates

* [WIP] do not do anything with this commit; for debugging only

* Adding before clean up

* emulation more or less works; need to work out more unicorn bugs

* clean up emulate() caller code

* move hooks to methods; cleanup

* Concretize memory when emulating

* Re-add Bool()

* Update tests to start at offset 4

 When an instruction branches to the previous instruction,
Unicorn attempts to dereference that memory. We'd like to use
unit tests to also make sure Unicorn emulation is in line with
our own semantics. If we start all tests at offset 4, we can
jump to a previous instruction and not fault when Unicorn
dereferences it.

* Fix concretization

* Clean up test imports; upper-case Cpu

* Unicorn tests

 * Add tests for all the ARM semantics, but make sure they're equivalent
   on unicorn.
 * Add a few tests to make sure unicorn correctly concretizes the memory
   it references

* Fix broken import

* Add symbolic register tests

* Re-introduce the unicorn hack

* Add the 'ONE' concretization policy

* Rm unused function

* Update concretization; add comments

* Add ONE policy test

* Create a base class for all concretization exceptions

* Remove Armv7Cpu._concretize_registers

* Check for enabled logging in a more idiomatic way

* [wip] intermediate testing commit

* Reimplement hooks and execution with unicorn

* Add a DMB (mem barrier) instruction; nop

* simplify instruction resolution

* improve unicorn error handling

* explicitly delete emu

* Handle ARM helpers inline

* map fetched memory

* Narrow exception handling

* Update DMB docs; make __kuser_dmb match real implementation

* Fix typo; add comment; remove extraneous parameter

* typos++
2017-04-03 16:00:49 -04:00
Mark Mossberg
5368716e42 Fix state.branches (#74)
* init

* rm old code

pretty sure it's wrong

* Clean

* rm

* Rename record_fork, move to ConcretizeRegister exception handler

It doesn't need to be in fork() because it's only relevant for when
we fork due to PC.

* Add test for record_branches

* Add back record_branches which got removed in rebase

Rebase went oddly because State got moved to a new file
2017-03-20 17:56:25 -04:00
JP Smith
ca0bee2377 Rename test -> tests (#66)
* rename test -> tests

* re-add ignored tests
2017-03-13 14:06:36 -05:00