212 Commits

Author SHA1 Message Date
Alex Groce dd4c17e918 fix message on program exit to not claim internal error 2018-07-14 11:38:51 -07:00
ggrieco-tob 23a1da2c7c Fix for hook_MaxUInt and hook_MinUInt in Manticore
(untested!)
2018-07-14 09:44:03 -03:00
Alex Groce 751fe57042 change to not access state.solver 2018-07-13 15:14:33 -07:00
Alex Groce dcb1ce6518 clean up pyflakes issues, fix args missing in angr error message, and run pyflakes on deepstate code 2018-07-13 10:47:31 -07:00
ggrieco-tob dd0fdc27ed Fixed missing default value in run_test
This small fix will enables Manticore to work properly as a backend.
2018-07-12 17:38:14 -03:00
ggrieco-tob 5d91dfd00b improved selection of base address in case of executables and shared objects 2018-07-11 10:24:18 -03:00
ggrieco-tob 4df001bf29 fixed manticore backend 2018-07-04 08:43:31 -03:00
Alex Groce b0be9abf18 fix args missing in run_tests 2018-07-02 15:22:20 -07:00
arunjohnkuruvilla 72aea332aa Used toplevel manticore.issymbolic instead of manticore.utils.helpers.issymbolic. Fixed Issue #14 2018-03-02 20:15:04 -05:00
Joe Ranweiler 35f73f2496 Add KLEE support to Manticore executor 2018-02-25 10:27:48 -08:00
Joe Ranweiler 96dafe6f41 Fix wrapped indentation 2018-02-25 10:27:48 -08:00
Joe Ranweiler 376235808a Internally support varying take-over symbols in Manticore executor 2018-02-25 10:27:48 -08:00
Joe Ranweiler 330f58b944 Add KLEE support to angr executor 2018-02-25 10:27:47 -08:00
Joe Ranweiler 4edfccd953 Internally support varying take-over symbols in angr executor 2018-02-25 10:27:47 -08:00
Joe Ranweiler 2ea978999b Replace DeepState_TakeOver() with Manticore function model
Now we have API parity with the angr executor, and return 1 from
`DeepState_TakeOver()` when it is hooked for symbolic execution under
the Manticore backend.
2018-02-20 15:43:34 -08:00
Joe Ranweiler 9e7266399c Add TakeOver impl to Manticore executor 2018-02-20 15:43:34 -08:00
Joe Ranweiler 353bed10ee Factor out unit test running in Manticore executor 2018-02-20 15:43:34 -08:00
Joe Ranweiler 76965704b4 Add TakeOver impl to angr executor
- Add `--take_over` flag
- Allow running tests from non-function instruction addr
- Hook `DeepState_TakeOver()` with a `SimProcedure` that returns 1
- Make a fake test case that starts after `TakeOver` returns
2018-02-20 15:43:34 -08:00
Joe Ranweiler 0a746ca078 Factor out deepstate-angr API hook setup, unit test exec 2018-02-20 10:31:24 -08:00
Joe Ranweiler 20781f91d0 Add default output directory for saved test cases 2018-02-20 10:01:45 -08:00
Joe Ranweiler b7aca2196c Add explicit deepstate-manticore executor script
This matches the command-line API described in the paper, and lets users
invoke the Manticore backend without relying on the fact that it is the
default (which might change).
2018-02-19 18:23:58 -08:00
Alex Groce ff3ae3debd remove unused variable i 2018-02-19 14:52:08 -07:00
Peter Goodman 956ee3261e Update main_manticore.py 2018-02-19 11:45:23 +08:00
Peter Goodman 7e69ee208f Merge pull request #33 from trailofbits/improve-mc-crash-saving
Be stricter about what terminated states are saved as crashes
2018-02-18 12:00:45 +08:00
alex 4cb2354759 Better failure when using Manticore but Z3 is not installed 2018-02-16 16:26:50 -08:00
Joe Ranweiler 39e57b6725 Be stricter about what terminated states are saved as crashes
We only want to save a `.crash` file if the input would cause a crash
when executing using the native harness. The old impl treated any state
termination as a crash. Now we add a predicate which checks the `reason`
and decides if the termination represents a crash in the program being
analyzed.

For now, we only flag `InvalidMemoryAccess` exceptions as crashes, as
identified by the `message` property on a `TerminateState` exception.
2018-02-16 12:31:33 -08:00
Joe Ranweiler 4814e8184b Flag unknown Manticore state terminations as crashes
This is an over-approximation, which we will tighten later.
2018-02-15 10:54:47 -08:00
Joe Ranweiler c1b91432fd Fix executor docstrings 2018-02-14 14:26:24 -08:00
Joe Ranweiler 7fbb966777 Detect, report crashes in deepstate-angr 2018-02-14 12:24:33 -08:00
Joe Ranweiler 8ede1e2ddc Remove stray whitespace 2018-02-14 12:06:26 -08:00
Peter Goodman ee80baa0ea Minor fix. 2018-01-18 14:24:08 -05:00
Peter Goodman 2eaeb7480c Adding Google Flags-like command-line option parsing, though implemented in C, to the main executable. The code is ported from Granary2. 2018-01-07 16:25:31 -05:00
Peter Goodman 49524e610d Symbol lookup refactor. 2017-12-14 14:56:09 -05:00
Alex Groce 0d934d4fac Attempt at OS X symbol lookup fix 2017-12-14 11:39:37 -08:00
Peter Goodman 31838780c3 Trim out trailing newlines and stuff 2017-12-14 00:56:22 -05:00
Peter Goodman 7c585f5c44 Add 32-bit support, i.e. libdeepstate32 2017-12-13 21:53:33 -05:00
Peter Goodman e9bd6dc177 Fixes one or two subtle issues. But the more interesting fix is that I implemented puts in terms of DeepState_Log. Calls to printf that had no format arguments are transformed by the compiler into calls to puts, but that wasn't being wrapped by DeepState, so it was appearing as though those log messages never actually happened. 2017-12-12 14:01:41 -05:00
Peter Goodman 8248bbdcbc Removed usage of old name, added in a Euler power of like primes example. When the pairwise ASSERT_NEs are absent, you get interesting results that show examples of integer overflows. 2017-12-10 20:08:08 -05:00
Peter Goodman fcd000dc14 Added a maximize objective API to DeepState. 2017-12-10 13:37:47 -05:00
Peter Goodman 188d4517d8 Added prime polynomial example, new Pumping function to address scalability challenges with primality testing, and some improvements to the streaming interface, where if you don't stream in values, then the python side doesn't end up printing out some 'empty' stream infos. 2017-12-09 16:43:43 -05:00
Peter Goodman a5ce3eaf31 Fix issue where I passed cast_to to min. 2017-12-03 20:57:15 -05:00
Peter Goodman 29f2465ebf Fixes issue with logger. Fixes issue where we weren't get the minimum value SATed. 2017-11-21 13:01:32 -05:00
Peter Goodman 5f36822021 Made the report function concretize using the minimizer, so that eventually we'll be able to compare inputs generated across tools 2017-11-09 10:35:48 -05:00
Peter Goodman 6ec7d71188 Added error checking. 2017-11-02 01:05:15 -04:00
Peter Goodman c4f74e2389 Adds some error checking around finding important symbols and initializing Manticore/Angr. Adds the ability to save concretized bytes to an output directory. For the time being, I'm going with the approach of the user specifying a output dir, then within that I create directories for each file basename in the tests, and subdirectories for each test name, and in there I put binary test files. 2017-11-02 00:54:18 -04:00
Peter Goodman bc208dbd4d Fixes issue where the angr script printed out the wrong symbol bytes. 2017-11-01 21:27:08 -04:00
Peter Goodman 4f914e4eee Fixes to stream formatting of doubles, they weren't being streamed before. Implemented the chk versions of printf and such, so that they all route through the logging interface as well. Implemented the concretization APIs. 2017-11-01 17:56:54 -04:00
Peter Goodman d2bc82fc35 Renaming from McTest to DeepState. 2017-11-01 13:38:32 -04:00
Peter Goodman f7f029965b Whatever I had before renaming. 2017-11-01 12:14:22 -04:00
Peter Goodman a46e06b03b Refactored to split common code between Manticore and Angr out into common.py. Implemented the new deferred streaming stuff, it seems to work semi-well for this simple cases I've tested, but there's still work to do. The latest code has some remaining issues. Printing out the final input bytes in Angr shows the wrong thing, although what gets streamed out is right. This is visible when running mctest-angr examples/ArtihmeticProperties. With Manticore, the big issue is that it doesn't properly pickle smt expressions (or something to this effect), so I'm ending up with multiple definitions of the same stuff and that throws exceptions. This is tricky to deal with because the streaming of output needs to be able to save symbolic data. 2017-11-01 02:42:31 -04:00