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
Peter Goodman
8ec44074ad
Make sure to make new lists of messages so that messages from one test don't get put into another.
2017-10-30 14:39:15 -04:00
Peter Goodman
3702bfcb81
Changed how the logging works to log to a static buffer, then the hooks pull info out from there.
2017-10-30 14:16:02 -04:00
Peter Goodman
e4f4cfe0db
Kind of feature parity between Manticore and Angr on these tests.
2017-10-30 00:45:59 -04:00
Peter Goodman
4b786adc70
Got Manticore (with some minor unpublished fixes) working for McTest, based on Yan's initial work. Most of the angr code directly ports over, which is convenient. Haven't yet implemented McTest_Log (which isn't working for angr, curiously).
2017-10-29 20:35:50 -04:00
Peter Goodman
0ec7047b0f
Merge branch 'master' of github.com:trailofbits/mctest
2017-10-29 18:54:48 -04:00
Peter Goodman
e0f104aaef
Adding logger support, and other things.
2017-10-29 18:54:41 -04:00
yan
e3d8ab9b61
Expand Manticore support
2017-10-29 18:17:15 -04:00
Peter Goodman
b8560c553f
USe a C++ style case in McTest.hpp
2017-10-28 20:23:23 -04:00
Peter Goodman
89da3e8e94
Made it so that tests can be run on their own, independent of a symbolic executor. This will open up libFuzzer support, and concrete execution of solved-for test case inputs. Removed all stuff related to sections. Made tests get registered via initializers. Working on exposing the API functions to be hooked by Manticore via a special system call with addres 0x41414141. Split the Angr version out into the mctest-angr binary, and going to try to make the mctest binary use Manticore.
2017-10-28 19:13:59 -04:00
Peter Goodman
0d336bd4d6
Fixed build errors for c++ test basics. Added a ForAll thingy to abstract around making symbols. Shortened section name lengths. Added a simple arithmetic properties test case.
2017-10-28 01:11:59 -04:00
Peter Goodman
76585f095b
Improvements. Now hooking fewer functions, and instead making on big array symbolic. This will make it easier to run the inputs concretely (by eventually filling in the array with the concrete bytes), and will also make possible fuzzer integration (where the fuzzer mutates the bytes of the array) possible.
2017-10-28 00:09:33 -04:00
Peter Goodman
6249ec6208
Initial commit.
2017-10-27 16:34:58 -04:00
