1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
# Focaccia
This repository contains initial code for comprehensive testing of binary
translators.
## Requirements
For Python dependencies, see the `requirements.txt`. We also require at least LLDB version 17 for `fs_base`/`gs_base`
register support.
I had to compile LLDB myself; these are the steps I had to take (you also need swig version >= 4):
```
git clone https://github.com/llvm/llvm-project <llvm-path>
cd <llvm-path>
cmake -S llvm -B build -DCMAKE_BUILD_TYPE=Release -DLLVM_ENABLE_PROJECTS="clang;lldb" -DLLDB_ENABLE_PYTHON=TRUE -DLLDB_ENABLE_SWIG=TRUE
cmake --build build/ --parallel $(nproc)
# Add the built LLDB python bindings to your PYTHONPATH:
PYTHONPATH="$PYTHONPATH:$(./build/bin/lldb -P)"
```
It will take a while to compile.
## How To Use
`focaccia` is the main executable. Invoke `focaccia --help` to see what you can do with it.
### QEMU
A number of additional tools are included to simplify use when validating QEMU:
`capture-transforms`, `convert-log`, `validate-qemu`. They enable the following workflow.
```bash
capture-transforms -o oracle.trace bug.out
qemu-x86_64 -g 12345 bug.out &
validate-qemu --symb-trace oracle.trace localhost 12345
```
Using this workflow, Focaccia can determine whether a mistranslation occured in that particular QEMU run.
### Box64
For validating Box64, we create the oracle and test traces and compare them
using the main executable.
```bash
capture-transforms -o oracle.trace bug.out
BOX64_TRACE_FILE=test.trace box64 bug.out
focaccia -o oracle.trace --symbolic -t test.trace --test-trace-type box64 --error-level error
```
## Tools
The `tools/` directory contains additional utility scripts to work with focaccia.
- `convert.py`: Convert logs from QEMU or Arancini to focaccia's snapshot log format.
## Project Overview (for developers)
### Snapshots and comparison
The following files belong to a rough framework for the snapshot comparison engine:
- `focaccia/snapshot.py`: Structures used to work with snapshots. The `ProgramState` class is our primary
representation of program snapshots.
- `focaccia/compare.py`: The central algorithms that work on snapshots.
- `focaccia/arch/`: Abstractions over different processor architectures. Currently we have x86 and aarch64.
### Concolic execution
The following files belong to a prototype of a data-dependency generator based on symbolic
execution:
- `focaccia/symbolic.py`: Algorithms and data structures to compute and manipulate symbolic program transformations.
This handles the symbolic part of "concolic" execution.
- `focaccia/lldb_target.py`: Tools for executing a program concretely and tracking its execution using
[LLDB](https://lldb.llvm.org/). This handles the concrete part of "concolic" execution.
- `focaccia/miasm_util.py`: Tools to evaluate Miasm's symbolic expressions based on a concrete state. Ties the symbolic
and concrete parts together into "concolic" execution.
### Helpers
- `focaccia/parser.py`: Utilities for parsing logs from Arancini and QEMU, as well as serializing/deserializing to/from
our own log format.
- `focaccia/match.py`: Algorithms for trace matching.
### Supporting new architectures
To add support for an architecture <arch>, do the following:
- Add a file `focaccia/arch/<arch>.py`. This module declares the architecture's description, such as register names and
an architecture class. The convention is to declare state flags (e.g. flags in RFLAGS for x86) as separate registers.
- Add the class to the `supported_architectures` dict in `focaccia/arch/__init__.py`.
- Depending on Miasm's support for <arch>, add register name aliases to the `MiasmSymbolResolver.miasm_flag_aliases`
dict in `focaccia/miasm_util.py`.
- Depending on the existence of a flags register in <arch>, implement conversion from the flags register's value to
values of single logical flags (e.g. implement the operation `RFLAGS['OF']`) in the respective concrete targets (LLDB,
GDB, ...).
|