about summary refs log tree commit diff stats
path: root/tools (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Implement online verification of symbolic backend ta/developTheofilos Augoustis2024-10-141-1/+6
| | | | | Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
* Enable Focaccia's logging in capture_transforms.pyTheofilos Augoustis2024-07-281-8/+3
| | | | | | | Disable Miasm's disassembly logger by default. Enable Focaccia's symbolic execution logger. Also refactor envp construction to use the `utils.get_envp` function.
* Add support for aarch64Theofilos Augoustis2024-07-121-23/+58
| | | | | | | | | | | | | | | | | | - 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>
* Make symbolic equations more symbolicTheofilos Augoustis2024-02-192-75/+90
| | | | | | 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.
* Add hostname argument to `verify_qemu.py`Theofilos Augoustis2024-02-151-6/+6
|
* Store instructions in SymbolicTransformationTheofilos Augoustis2024-02-081-5/+18
|
* Basic reproducer generator setupTheofilos Augoustis2024-02-023-1/+5
| | | | | Co-authored-by: Alp Berkman <alp.berkman@no-reply.com> Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
* Verify QEMU by abstracting over inconsistencies in trace logs via matching ↵Theofilos Augoustis2024-01-303-135/+288
| | | | | | | algorithm Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
* Use symbolic execution to speed up QEMU testingTheofilos Augoustis2024-01-222-146/+134
| | | | | | | | 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>
* Refactor symbolic transformation handlingTheofilos Augoustis2024-01-171-0/+27
|
* Refactor project structureTheofilos Augoustis2023-12-311-4/+4
| | | | | | | | 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.
* Verify QEMU by converting logs to internal data formatTheofilos Augoustis2023-12-263-0/+261
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>