about summary refs log tree commit diff stats
path: root/tools/capture_transforms.py (unfollow)
Commit message (Collapse)AuthorFilesLines
2025-08-27Support using custom miasm fork directly in flakeTheofilos Augoustis3-26/+12
2025-08-27Update to new miasm version with pyproject supportTheofilos Augoustis1-0/+0
2025-08-27Remove unused submodulesTheofilos Augoustis1-6/+0
2025-08-27Add miasm as a dependencyTheofilos Augoustis2-0/+4
2025-08-27Make default develop shell editableTheofilos Augoustis1-3/+54
2025-06-20Update pyproject.toml to support a custom development version of miasmTheofilos Augoustis2-6/+8
2025-06-20Add cpuid dependency on fork of cpuid that supports pyproject.tomlTheofilos Augoustis5-39/+28
2025-06-17Add support for getting a glibc environmentTheofilos Augoustis1-0/+9
2025-06-17Lookup gdb in PATH in verify qemu scriptTheofilos Augoustis1-1/+1
2025-06-17Add new pyproject.toml that includes dev environmentTheofilos Augoustis2-0/+175
2025-06-17Update flake to expose better developer shellsTheofilos Augoustis1-8/+7
2025-06-12Include reproducer for 508 (and generalize gitignore)Theofilos Augoustis2-2/+15
2025-06-12Remove nix.shell (switching completely to flakes)Theofilos Augoustis1-12/+0
2025-06-12Update flake to include gccTheofilos Augoustis1-2/+2
2025-06-11Update flake to include support for muslTheofilos Augoustis1-0/+13
2025-06-11Add flake support for known-buggy QEMU versionTheofilos Augoustis2-6/+36
2025-06-10Update flake to include QEMU versionTheofilos Augoustis1-0/+10
2025-06-10Add multi-system support to flake;Theofilos Augoustis2-8/+43
2025-06-10Rename tests directoryTheofilos Augoustis2-0/+0
2025-06-10Update gitignore to hide Nix result filesTheofilos Augoustis1-0/+4
2025-06-10Migrate project to use flakesTheofilos Augoustis2-0/+193
2025-06-10Migrate project to standard structure with uvTheofilos Augoustis23-2/+117
2024-10-14Implement online verification of symbolic backend ta/developTheofilos Augoustis7-106/+412
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
2024-10-13Read instructions directly from program memoryTheofilos Augoustis2-19/+32
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.
2024-07-28Enable Focaccia's logging in capture_transforms.pyTheofilos Augoustis2-11/+10
Disable Miasm's disassembly logger by default. Enable Focaccia's symbolic execution logger. Also refactor envp construction to use the `utils.get_envp` function.
2024-07-12Add support for aarch64Theofilos Augoustis10-88/+293
- 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>
2024-02-22Rework Focaccia's command line interfaceTheofilos Augoustis2-64/+132
2024-02-19Make symbolic equations more symbolicTheofilos Augoustis10-198/+413
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.
2024-02-15Add hostname argument to `verify_qemu.py`Theofilos Augoustis1-6/+6
2024-02-14Rewrite symbolic tracing algorithmTheofilos Augoustis3-191/+139
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
2024-02-08Store instructions in SymbolicTransformationTheofilos Augoustis6-59/+151
2024-02-02Basic reproducer generator setupTheofilos Augoustis9-21/+257
Co-authored-by: Alp Berkman <alp.berkman@no-reply.com> Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
2024-02-07Extract matching algorithms into a moduleTheofilos Augoustis3-39/+108
We have: - Trace folding: Resolve mismatches in snapshot granularity - Trace matching: Resolve mismatches in program flow
2024-01-30Verify QEMU by abstracting over inconsistencies in trace logs via matching ↵Theofilos Augoustis3-135/+288
algorithm Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
2024-02-02Add ReadableProgramState interfaceTheofilos Augoustis4-71/+97
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.
2024-01-24Refactor comparison and user-facing logicTheofilos Augoustis5-102/+55
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
2024-01-22Use symbolic execution to speed up QEMU testingTheofilos Augoustis5-169/+231
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>
2024-01-17Refactor symbolic transformation handlingTheofilos Augoustis9-209/+464
2023-12-31Refactor project structureTheofilos Augoustis17-121/+102
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.
2023-12-26Verify QEMU by converting logs to internal data formatTheofilos Augoustis4-1/+274
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
2023-12-27Extend error reporting systemTheofilos Augoustis4-92/+169
Add error severities and the ability to filter for them. Include more information in comparison error messages.
2023-12-26Refactor parser.py (for gdb integration)Theofilos Augoustis1-25/+56
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
2023-12-26Improve SparseMemory.write_memory performanceTheofilos Augoustis2-8/+13
Reduce overhead of handling sparse memory
2023-12-14Implement symbolic comparison and match traces via MiasmTheofilos Augoustis10-293/+511
Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
2023-12-08Adapt symbolic compare to new transform interfaceTheofilos Augoustis18-614/+278
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>
2023-12-07Replace symbolic execution tools with MiasmTheofilos Augoustis4-400/+317
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.
2023-11-28Record symbolic transform for single instructionsTheofilos Augoustis4-78/+178
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>
2023-11-27Add memory storage capabilities to `ProgramState`Theofilos Augoustis4-156/+229
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`.
2023-11-27Implement symbolic state comparison algorithmTheofilos Augoustis8-191/+210
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>
2023-11-26Standardize X86 register namesTheofilos Augoustis6-122/+142
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>