about summary refs log tree commit diff stats
Commit message (Collapse)AuthorAgeFilesLines
...
| * Add Box64 validation steps to READMEckrinitsin2025-10-231-0/+13
| |
| * Add Box64 build with erroneous CMPXCHG instructionChristian Krinitsin2025-10-232-1/+107
| |
| * Add Box64 parserChristian Krinitsin2025-10-232-0/+32
| |
| * Update TraceEnvironment parametersChristian Krinitsin2025-10-231-1/+1
|/
* Update flake to check for missing git submodulesTheofilos Augoustis2025-10-211-0/+16
|
* Fix incorrect docstring for write_register ta/docsTheofilos Augoustis2025-10-161-1/+1
|
* Update README to include information about running helper toolsTheofilos Augoustis2025-10-161-1/+12
|
* Simplify issue 2248 reproducer ta/arm64Theofilos Augoustis2025-10-141-4/+12
|
* Update to new Miasm version with support for ldsmaxbTheofilos Augoustis2025-10-143-5/+8
|
* Add better diagnostic for incorrect symbolic expressionsTheofilos Augoustis2025-10-141-3/+6
|
* Add indentation to any and all Focaccia dunmps to make the human-inspectableTheofilos Augoustis2025-10-141-1/+1
|
* Dump Focaccia symbolic equations with indentation (to help debugging)Theofilos Augoustis2025-10-101-1/+1
|
* More alternatives for accessing aarch64 vectorsTheofilos Augoustis2025-10-091-1/+4
|
* Update QEMU validator to manually pass executable (necessary for cases where ↵Theofilos Augoustis2025-10-092-12/+36
| | | | GDB cannot determine the executable on its own, e.g. when we specify -march)
* Improve handling of vector reads when validating QEMUTheofilos Augoustis2025-10-071-6/+17
|
* Add basic indentation to the TraceEnvironment dumps to improve readabilityTheofilos Augoustis2025-10-071-1/+1
|
* Enable reading DCZID properlyTheofilos Augoustis2025-10-071-1/+9
|
* Add support for reading DCZID host-sideTheofilos Augoustis2025-10-077-3/+65
|
* Properly support TPIDR registerTheofilos Augoustis2025-10-072-3/+4
|
* Add correct handling for Q<num> registers by converting them to the ↵Theofilos Augoustis2025-10-072-34/+75
| | | | (standard) V<num> form
* Make cross-validation of results with native execution optionalTheofilos Augoustis2025-10-073-21/+34
|
* Add basic reproducer for issue 2248 with Focaccia (hacked, does not work yet)Theofilos Augoustis2025-09-294-1/+28
|
* Disable hardening to enable compiling non-PIE binaries on aarch64Theofilos Augoustis2025-09-291-0/+2
|
* Add correct cross-compilation architecture for musl developer environmentTheofilos Augoustis2025-09-101-1/+1
|
* Add support for running tests with flake checkTheofilos Augoustis2025-09-105-83/+164
|
* Add descriptions to apps declared by flakeTheofilos Augoustis2025-09-101-0/+15
|
* Fix handling of Focaccia dependenciesTheofilos Augoustis2025-09-013-26/+44
|
* Refactor tool handling to match flake systemTheofilos Augoustis2025-08-287-22/+73
|
* Migrate to LLDB from pylldbTheofilos Augoustis2025-08-283-73/+96
|
* Migrate to nix flakes, uv and pyproject toml for buildsTheofilos Augoustis2025-08-2730-19/+663
|
* 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.