| Commit message (Collapse) | Author | Files | Lines |
|
Instead of loading an executable file and disassembling instructions
from there, load instructions directly from the concrete execution's
memory. This allows symbolic tracing to work for non-statically compiled
executables as well as JIT-compiled code.
|
|
Disable Miasm's disassembly logger by default. Enable Focaccia's
symbolic execution logger.
Also refactor envp construction to use the `utils.get_envp` function.
|
|
- Implement an architecture description for aarch64
- Add endianness information to the `Arch` class.
- Move conversion from flags register to logical flag values from the
calling code to the concrete targets (LLDB and GDB), which is the
only point where we (have to) deal in flags registers.
- Handle assembly/disassembly errors in serialization of
SymbolicTransform
- Move ProgramState's `arch` attribute into ReadableProgramState.
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
|
|
Reduce the impact of concrete guidance on the process of calculating an
instruction's symbolic equation. The resulting equations will contain
less assumptions about the concrete state and thus be more generic.
|
|
|
|
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
|
|
Co-authored-by: Alp Berkman <alp.berkman@no-reply.com>
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
|
|
We have:
- Trace folding: Resolve mismatches in snapshot granularity
- Trace matching: Resolve mismatches in program flow
|
|
algorithm
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
It often occurs that a function only wants to read values from a
ProgramState, but not write them. The new interface ReadableProgramState
captures this need.
|
|
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
We don't need QEMU's log anymore, so we connect to a GDB server instance
that the user has to start with `$ qemu -g <port> ...`.
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
|
|
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>
|
|
Add error severities and the ability to filter for them. Include more
information in comparison error messages.
|
|
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
Reduce overhead of handling sparse memory
|
|
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.
|
|
Step manually through single instructions instead of full basic blocks.
Record the transformation performed by each instruction as symbolic
equations.
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
The `SparseMemory` class represents a program's memory. While the user
can read from and write to arbitrary memory addresses, it manages its
memory in pages/chunks internally. This is a tradeoff between space
consumption (this solution might have a memory overhead) and lookup
speed of individual memory addresses.
Add two small unit tests for `SparseMemory`.
|
|
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>
|
|
Add some infrastructure for flexible register name matching (i.e. using
'PC' to look up RIP):
- `Arch.to_regname` tries to look up a register's standard name from an
arbitrary string.
- `ArchX86` overrides `to_regname` to resolve alias names for
registers. Currently just 'PC' for 'RIP'.
- `ProgramState.read` and `ProgramState.write` use `to_regname` to make
register access more convenient.
Add all flags with their standard abbreviations to `x86.regnames`.
Implement a full RFLAGS decomposition into its individual flags in
`x86`. Replace the hacks in `run.py` and `miasm_test.py` with this more
complete solution.
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>
|
|
|
|
|
|
|
|
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
- main.py: focaccia user-interface
- snapshot.py: state trace snapshots handling
- compare.py: snapshot comparison algorithms
- run.py: native execution tracer
- arancini.py: Arancini log handling
- arch/: per-architecture abstractions
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
Employ some refactorings to make the parsing code simpler and faster.
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
|
|
|
| |