| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
|
|
| |
Read concrete state on demand during concolic exec
During concolic tracing, don't record full program snapshots at each
basic block, but instead read concrete values directly from the concrete
target when they are needed.
|
| |
|
|
|
| |
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Also implement a `MiasmSymbolicTransform.concat` function that
concatenates two transformations. Some minor adaptions to the eval_expr
code was necessary to remove some assumptions that don't work if the
resolver state returns symbols instead of concrete values.
Remove obsolete utilities that were used for angr.
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
| |
|
|
|
|
|
|
|
| |
Refactor SymbolicTransform interface a bit to include transformations of
memory content. Implement it for Miasm as a backend.
Move all symbolic execution things out of the test script
(`miasm_test.py`) and move them to `symbolic.py` to replace the
angr-based algorithms.
|
| |
|
|
|
|
|
|
|
| |
This is the first draft of a `compare` algorithm that uses recorded
symbolic transformations. Is currently based on angr, so it's probably
going to be reworked to work with states generated by Miasm.
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
| |
|
|
|
| |
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
| | |
|
| |
|