Add Manticore native State-specific hooks (trailofbits#1777) #7
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Github automatically parses the issue templates and adds them to the config file, so they don't need to be included here.
* Add a warning when selected no methods for inclusion * CC
* FIx enable/disable magic * CC * Test enable/disable * Remove duplicated code
* Experimental coverage changes Tells coverage.py to record coverage for individual test cases, and makes CodeCov tolerate a small drop in overall coverage percentage to account for nondeterministic gas tests. * Use workspace * Remove explicit concurrency type declaration Appears to break use of subprocess in integration tests * Eliminate dynamic context * Make all CI respect rcfile * Use environment variable
* Use merge SHA instead of head Github Actions doesn't update the head variable despite the checkout action merging the active branch into `master`, so the commit range specified was invalid * Start from common ancestor * Omit explicit SHA * Lint HEAD instead of merge * Manually fetch base SHA * Print the names of files to be diffed * Update ci.yml * Modify a Python file * Blacken everything that was missing The modified files got missed due to black not properly running on our CI
* Snapshots * CC * Allow snapshooting just from main() * A test * Test and fix is_main * CC * review * ismain vs is_running * is main to is main script * Remove unused member variable * Fix is main variable * Update manticore/core/manticore.py Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com> * review * blkn * Betteer Exception handling * Lint and test Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
* New upstream auto-VMTests tests for istanbul * Removed redundant tests * bugfix * Reset CI * Debug CI 1 * debug CI * wakey wakey GitHub Actions * Poke GH * Fix detector * New CI weaky weaky * Change default smtlib max memory usage weaky weaky * ci weaky waky * ci weaky waky * CI waky weaky * Fix test_general weaky weaky * Fix ethtests. weaky waky * Unittest driven bugfixes. weaky waky * Avoid check-sat in the middle of a solving. weaky wakey * Fix config. weaky wakey * Reduce queries in IO detector * CC * CC * fix nativve tests * CC and solver defaults * merge. weaky waky * Fixing tests * Remove debug print * Fix in DetectUninitializedMemory * Change truffle test state count * CC * Better forking on failed transactions * CC * Fix truffle tst state count * Improve z3 speed * Fix truffle test state count * Change default gas concretization in CALL * Better logging at fork * Insane commit to fix several bugfixes and refator stuff * black * Fix selfdestruct test * Fix some unittests * Default to bytes fo constant calldata * Fix tests * Better doc * https://github.com/trailofbits/manticore/pull/1676/files#r426927762 * https://github.com/trailofbits/manticore/pull/1676/files#r426946198 * Leave native alone and fix pyevmasm dep * Update manticore/platforms/evm.py Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com> * Update manticore/platforms/evm.py Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com> * isSeven * OPTI/PESI * Truffle optimistic * truffle fix * Truffle state count * CC * Fix tests PESI/OPTI * Update manticore/core/state.py Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com> * Better policy naming * Update manticore/platforms/evm.py Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com> * Update manticore/ethereum/manticore.py Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com> * Update manticore/platforms/evm.py Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com> * PESi PESSI * blkn * weaky * wakey wakey * blkn * unreachable * Fix state count in checkpoint test (merge) * remove unused exception var Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com> Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com>
* Rollback to support yices again * CC * Test yices * Better get-value handling * Z3/CVC4/YICES * CC * Yices/CVC4 * CC * Default yices * Default debug level fix * Quick auto solver * shutil.which * CC * Default yices for testing * Remove old commented out code * Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Remove unused class * Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Readme hack * CC/lint * Fix typing * z3 back to the rodeo * lint * Fancy optimize * Fix lint * CC reviewed Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>
* Working copy for strcpy - without symbolic input * Corrected null term error * Needs to be tested but general algorithm idea for handling symbolic input * Updated according to feedback * Beginning of strcpy tests * Revising strcpy algorithm - realised it was flawed * This should be a more correct way of handling symbolic bytes. Needs testing * Get rid of redundant code * Fixed another typo * Update manticore/native/models.py Co-Authored-By: Eric Kilmer <eric.d.kilmer@gmail.com> * Clarified and updated comments * Fixed some errors in model while working on tests * Progress on tests * Found typo in models * Removed unnecassary whitespace * Added some helper functions for tests and to clean things up * Added comments for helper functions * WIP: current state of strcpy tests * Updated type hints from Expression to BitVec * Fixed linter complaints * Updated strcpy return type to make linter happy * Added some helper properties to expression BitVecITE * Overwrote equal op in ArraySelect * Fixed formatting in expression * Almost done just needs some cleaning * Attempt at overriding __eq__ again * Cleaned up tests some still have unresolved __eq__ issues * Removed stuff from expression and updated test_models.py * Removed stuff from expression and updated test_models.py * Basicly done probably needs some more comments for clarity * Cleaned up the tests a little * Corrected linter error and added more comments to strcpy model functions * Remove duplicated word in comment Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Update manticore/native/models.py Co-authored-by: Brad Larsen <brad.larsen@trailofbits.com> * Update manticore/native/models.py Co-authored-by: Brad Larsen <brad.larsen@trailofbits.com> * Update tests/native/test_models.py Co-authored-by: Brad Larsen <brad.larsen@trailofbits.com> * Updates according to feedback * Swapped can_be_true and must be true * Updates for feedback * Forgot to lint * Fixed some typos * Largely simplified ITE being built * Forgot to lint * This is messy but seems to be concretizing to the correct states * Very very messy state of the code before attempting to concretize on every possible NULL * Cleaned up model with forking on every possible NULL * Removed trailing whitespace for CodeClimate * Added state.context for offset value back * New symbolic test with regex for expected output * New symbolic test with regex for expected output * Updated for mypy * Updated comments in tests * Updated cant_be_null to cannot_be_null * Corrected docstring location for _test_strcpy * Add break for efficiency * Added compiler information and source file * Updated regex to use raw strings Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> Co-authored-by: Brad Larsen <brad.larsen@trailofbits.com>
* Add ONE failing test * Fix test * Try fix get-related * Move regression to other * blkn * blkn * Move get related * CC * fix concolic * lint * DivByZero default to zero * blkn * Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Update manticore/core/smtlib/constraints.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Update manticore/core/smtlib/constraints.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * remove odd string * lint * mypy lint * Update manticore/core/smtlib/visitors.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * lint * Add Docs * Replace modulo with masks * Blacken * blkn * fix mypy * fix mypy * Add tests for signed LT behavior * New test * Fix constant folding * lint * lint * lint * Unittesting power * Permisive read_buffer * Preserve precision in constant folding * Strip left-in print debugging * fix wasm * Fix * REmove get_related from the default path and fix arm test * blkn * fix related to tests * blkn * Fix bug in test and disable debug messages in Solver * smtlib config to disable multiple check-sat in newer z3 * Disable log test and fix merging poc vs variable migration * blkn * Avoid exception in some callbacks * can_raise at did_will * slightly better z3 onfiguration * lint Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
* Remove/procrastinate solver query in etherleak detector * blkn
* Experiment with testing on OSX Not committing to front-lining OSX support as a feature because there are some fundamental performance concerns, but I would like to see how the tests behave. * solc --> usr/local/bin * Don't fail fast * Require Unicorn 1.0.2rc2 ¯\_(ツ)_/¯ * Update Bash on OSX builds * Use mac solc * Simpler solidity installation * Fix wasm tests maybe? * Swap `ls` args in truffle tests * Good 'ol printf debugging * OSX Keystone install * Truffle test miscounting fix? * Add unzipping timeout * Remive timeout _and_ `yes` * Allow output check to work on OSX * Add list wrapper to filter * Remove print statements * yolo keystone via homebrew * Try again w/ Keystone Brew * typo * Create osx.yml * Revert to Master's ci.yml * Update to checkout@v2 universally * Save checkout version change for another PR It maybe breaks codecov? * Add Truffle Tests * Fix Truffle * Make native an option * See if native works? * Revert "See if native works?" This reverts commit ce90d8b. * Replace actions content w/ script * Update number of Truffle tests * Force working directory * Remove shebang, fix YAML * Fix incorrect path to script? * Why are the docs always wrong * YAML syntax * Fix usage of GITHUB_WORKSPACE * Forget the workspace, just copy the script to the root * Revert workspace path changes * Fix VM test generation * Whitespace fixes * Only run on a schedule * Install Yices and CVC4
* Add ONE failing test * Fix test * Try fix get-related * Snapshots * CC * Allow snapshooting just from main() * A test * Test and fix is_main * CC * review * ismain vs is_running * is main to is main script * Remove unused member variable * initial import manticore verifier * Fix verifier installation * clear ready states * CC and smoke test * CC * Increase cov * Move regression to other * blkn * blkn * Move get related * CC * fix concolic * lint * DivByZero default to zero * blkn * Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Update manticore/core/smtlib/constraints.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Update manticore/core/smtlib/constraints.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * remove odd string * lint * mypy lint * Update manticore/core/smtlib/visitors.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * lint * Add Docs * blkn * blkn * Replace modulo with masks * Blacken * blkn * fix mypy * fix mypy * Add tests for signed LT behavior * New test * Fix constant folding * lint * blkn * lint * Fixes... * lint * Unittesting power * Permisive read_buffer * Fix optimize * Preserve precision in constant folding * Strip left-in print debugging * blkn * remove wasm_sym temporarily * Better simplification for constants * Add json * blkn * Better commmandline args * blkn * fix wasm * Fix * better commanlining * REmove get_related from the default path and fix arm test * blkn * fix related to tests * blkn * Fix bug in test and disable debug messages in Solver * smtlib config to disable multiple check-sat in newer z3 * Disable log test and fix merging poc vs variable migration * blkn * Avoid exception in some callbacks * can_rais at did_will * yikes! * blkn * Yices found one more states in truffle * Add a config constant to ignore symbolic balances * Add a config constant to ignore symbolic balances 2 * Relax truffle state count * Relax truffle state count 2 * Change cli name and test * Clear redy states in verifier workspace * Clear ready states in verifier workspace * Relative ws path on verifier output. Clean CREATE testcase example * Blkn * Improve coverage and funcid solving * lint * Better testcase generation at verifier * Better testcase generation at verifier and typos * Better output and default re * Test must revert * Better output and default re * move generate_testcase_ex to private method Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
* Revert 1e23f7a Remove psutil as a dependency * Bump version numb, update changelog * Re-do updated model not available message * Update for latest PRs * Update dates
* Add Github Actions config * Handle nightly versioning * Fix typos in README and PyPI upload * Make image URL global * Attempt today's upload * Install wheel * Fix indentation * Only run on schedule * Use versioned action, add nightly to readme * Retest upload w/ hard-coded version * Apparently v1 doesn't parse * Revert to only scheduled
* Specialized itereative serialization for Array * lint
* New working model of strlen - Symbolic Test yet to be updated * Updated modeling test for all symbolic input * Fixed code climate issue * Adding binary for new test * Updated test to use sets for compairison * Removed length compairison * Fix argument concretization indexing * Preserve both model implementation strategies * Corrected formatting * Removed whitespace for code climate * Removed whitespace for code climate Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>
* Add doc, fix output bugs * Apply suggestions from code review Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com> * Readme link Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
* Add strncpy model * Forgot to remove an edit * Adding model tests * Added strncpy c file and created a directory for all string modeling binaries * Update to argument ordering in manticore/native/models.py Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com> * Removed dead code Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>
* Capture return value * Increase verifier test timeout * Fix typo * Add more frequent checks to m.is_killed
* Use coveralls * Use python coveralls * Try again with different casing * Use coveralls repo token from web page * Use GITHUB_TOKEN in github action parallel-finished * Remove codecov config * Add note for final coverage job * Swap Readme coverage badge
Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
* Use default handler for symbolic system call arguments This will only be called when there is an implementation of the system call in the concrete Linux class and no implementation in the symbolic SLinux. The action is simply to concretize any found symbolic system call arguments. This should hopefully ease the use of Manticore when it encounters symbolic arguments to system calls that don't have specially implemented symbolic handling. A debug message is printed when this happens. * Make sure to return passed implementation * Use rsplit instead of indexing to get owner class of method Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
* Linux: Add stat method for FdLike * Add tests * Don't try to cover abstract class function bodies * Update test file names * Try again to not cover abstract methods * Add typehint to Directory stat() Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com> * Fix typehints with os.stat * Adjust type for stat object Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
* Add Manticore native State-specific hooks * Add tests * Add type hints when setting state * Add back needed assertion for PC hook * Test that hook actually executes in test Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.