about summary refs log tree commit diff stats
path: root/tools/qemu_tool.py (unfollow)
Commit message (Collapse)AuthorFilesLines
2025-11-04Plugin validationReimersS8-6/+455
2025-11-03Add fsub operationChristian Krinitsin2-1/+31
2025-10-30Fix incorrect cross-validation flag specificationTheofilos Augoustis1-0/+1
2025-10-27Add BMI reproducerChristian Krinitsin5-0/+23
2025-10-24Refactor flake handling of box64Theofilos Augoustis1-47/+32
2025-10-23Add Box64 validation steps to READMEckrinitsin1-0/+13
2025-10-23Add Box64 build with erroneous CMPXCHG instructionChristian Krinitsin2-1/+107
2025-10-23Add Box64 parserChristian Krinitsin2-0/+32
2025-10-23Update TraceEnvironment parametersChristian Krinitsin1-1/+1
2025-10-21Update flake to check for missing git submodulesTheofilos Augoustis1-0/+16
2025-10-16Fix incorrect docstring for write_register ta/docsTheofilos Augoustis1-1/+1
2025-10-16Update README to include information about running helper toolsTheofilos Augoustis1-1/+12
2025-10-14Simplify issue 2248 reproducer ta/arm64Theofilos Augoustis1-4/+12
2025-10-14Update to new Miasm version with support for ldsmaxbTheofilos Augoustis3-5/+8
2025-10-14Add better diagnostic for incorrect symbolic expressionsTheofilos Augoustis1-3/+6
2025-10-14Add indentation to any and all Focaccia dunmps to make the human-inspectableTheofilos Augoustis1-1/+1
2025-10-10Dump Focaccia symbolic equations with indentation (to help debugging)Theofilos Augoustis1-1/+1
2025-10-09More alternatives for accessing aarch64 vectorsTheofilos Augoustis1-1/+4
2025-10-09Update QEMU validator to manually pass executable (necessary for cases where ↵Theofilos Augoustis2-12/+36
GDB cannot determine the executable on its own, e.g. when we specify -march)
2025-10-07Improve handling of vector reads when validating QEMUTheofilos Augoustis1-6/+17
2025-10-07Add basic indentation to the TraceEnvironment dumps to improve readabilityTheofilos Augoustis1-1/+1
2025-10-07Enable reading DCZID properlyTheofilos Augoustis1-1/+9
2025-10-07Add support for reading DCZID host-sideTheofilos Augoustis7-3/+65
2025-10-07Properly support TPIDR registerTheofilos Augoustis2-3/+4
2025-10-07Add correct handling for Q<num> registers by converting them to the ↵Theofilos Augoustis2-34/+75
(standard) V<num> form
2025-10-07Make cross-validation of results with native execution optionalTheofilos Augoustis3-21/+34
2025-09-29Add basic reproducer for issue 2248 with Focaccia (hacked, does not work yet)Theofilos Augoustis4-1/+28
2025-09-29Disable hardening to enable compiling non-PIE binaries on aarch64Theofilos Augoustis1-0/+2
2025-09-10Add correct cross-compilation architecture for musl developer environmentTheofilos Augoustis1-1/+1
2025-09-10Add support for running tests with flake checkTheofilos Augoustis5-83/+164
2025-09-10Add descriptions to apps declared by flakeTheofilos Augoustis1-0/+15
2025-09-01Fix handling of Focaccia dependenciesTheofilos Augoustis3-26/+44
2025-08-28Refactor tool handling to match flake systemTheofilos Augoustis7-22/+73
2025-08-28Migrate to LLDB from pylldbTheofilos Augoustis3-73/+96
2025-08-27Migrate to nix flakes, uv and pyproject toml for buildsTheofilos Augoustis30-19/+663
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>