about summary refs log tree commit diff stats
Commit message (Collapse)AuthorAgeFilesLines
* Add support for editable miasm builds ta/uv-migrateTheofilos Augoustis2025-08-271-1/+10
|
* Support using custom miasm fork directly in flakeTheofilos Augoustis2025-08-273-26/+12
|
* Update to new miasm version with pyproject supportTheofilos Augoustis2025-08-271-0/+0
|
* Remove unused submodulesTheofilos Augoustis2025-08-271-6/+0
|
* Add miasm as a dependencyTheofilos Augoustis2025-08-272-0/+4
|
* Make default develop shell editableTheofilos Augoustis2025-08-271-3/+54
|
* Update pyproject.toml to support a custom development version of miasmTheofilos Augoustis2025-06-202-6/+8
|
* Add cpuid dependency on fork of cpuid that supports pyproject.tomlTheofilos Augoustis2025-06-205-39/+28
|
* Add support for getting a glibc environmentTheofilos Augoustis2025-06-171-0/+9
|
* Lookup gdb in PATH in verify qemu scriptTheofilos Augoustis2025-06-171-1/+1
|
* Add new pyproject.toml that includes dev environmentTheofilos Augoustis2025-06-172-0/+175
|
* Update flake to expose better developer shellsTheofilos Augoustis2025-06-171-8/+7
|
* Include reproducer for 508 (and generalize gitignore)Theofilos Augoustis2025-06-122-2/+15
|
* Remove nix.shell (switching completely to flakes)Theofilos Augoustis2025-06-121-12/+0
|
* Update flake to include gccTheofilos Augoustis2025-06-121-2/+2
|
* Update flake to include support for muslTheofilos Augoustis2025-06-111-0/+13
|
* Add flake support for known-buggy QEMU versionTheofilos Augoustis2025-06-112-6/+36
|
* Update flake to include QEMU versionTheofilos Augoustis2025-06-101-0/+10
|
* Add multi-system support to flake;Theofilos Augoustis2025-06-102-8/+43
|
* Rename tests directoryTheofilos Augoustis2025-06-102-0/+0
|
* Update gitignore to hide Nix result filesTheofilos Augoustis2025-06-101-0/+4
|
* Migrate project to use flakesTheofilos Augoustis2025-06-102-0/+193
|
* Migrate project to standard structure with uvTheofilos Augoustis2025-06-1023-2/+117
|
* Merge branch 'ta/develop'Theofilos Augoustis2025-02-2531-588/+3730
|\
| * Implement online verification of symbolic backend ta/developTheofilos Augoustis2024-10-147-106/+412
| | | | | | | | | | Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
| * Read instructions directly from program memoryTheofilos Augoustis2024-10-132-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.
| * Enable Focaccia's logging in capture_transforms.pyTheofilos Augoustis2024-07-282-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.
| * Add support for aarch64Theofilos Augoustis2024-07-1210-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>
| * Rework Focaccia's command line interfaceTheofilos Augoustis2024-02-222-64/+132
| |
| * Make symbolic equations more symbolicTheofilos Augoustis2024-02-1910-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.
| * Add hostname argument to `verify_qemu.py`Theofilos Augoustis2024-02-151-6/+6
| |
| * Rewrite symbolic tracing algorithmTheofilos Augoustis2024-02-143-191/+139
| | | | | | | | | | Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
| * Store instructions in SymbolicTransformationTheofilos Augoustis2024-02-086-59/+151
| |
| * Basic reproducer generator setupTheofilos Augoustis2024-02-029-21/+257
| | | | | | | | | | Co-authored-by: Alp Berkman <alp.berkman@no-reply.com> Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com>
| * Extract matching algorithms into a moduleTheofilos Augoustis2024-02-073-39/+108
| | | | | | | | | | | | | | | | We have: - Trace folding: Resolve mismatches in snapshot granularity - Trace matching: Resolve mismatches in program flow
| * 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>
| * Add ReadableProgramState interfaceTheofilos Augoustis2024-02-024-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.
| * Refactor comparison and user-facing logicTheofilos Augoustis2024-01-245-102/+55
| | | | | | | | | | 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-225-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>
| * Refactor symbolic transformation handlingTheofilos Augoustis2024-01-179-209/+464
| |
| * Refactor project structureTheofilos Augoustis2023-12-3117-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.
| * Verify QEMU by converting logs to internal data formatTheofilos Augoustis2023-12-264-1/+274
| | | | | | | | | | Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
| * Extend error reporting systemTheofilos Augoustis2023-12-274-92/+169
| | | | | | | | | | Add error severities and the ability to filter for them. Include more information in comparison error messages.
| * Refactor parser.py (for gdb integration)Theofilos Augoustis2023-12-261-25/+56
| | | | | | | | | | Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
| * Improve SparseMemory.write_memory performanceTheofilos Augoustis2023-12-262-8/+13
| | | | | | | | Reduce overhead of handling sparse memory
| * Implement symbolic comparison and match traces via MiasmTheofilos Augoustis2023-12-1410-293/+511
| | | | | | | | | | Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
| * Adapt symbolic compare to new transform interfaceTheofilos Augoustis2023-12-0818-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>
| * Replace symbolic execution tools with MiasmTheofilos Augoustis2023-12-074-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.
| * Record symbolic transform for single instructionsTheofilos Augoustis2023-11-284-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>
| * Add memory storage capabilities to `ProgramState`Theofilos Augoustis2023-11-274-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`.