25 KiB
Table of Contents
Tracing
In the following, we document how to collect a concrete execution trace of our target, a known vulnerable ARMv7 binary named circled (see Vulnerability CVE-2022-27646). The trace is collected in a cross-platform remote setup, i.e. despite our host system being x86-based, the target runs on an (emulated) ARMv7-based device (see Emulation). The collected trace may later be used for different symbolic execution runs/analyses (see Symbolic Execution), which can be done offline, for instance on a more powerful machine.
Note: In case you are not interested in how to collect a concrete execution trace yourself and
directly want to jump into Morion's symbolic
execution capabilities, the file circled.trace.yaml can be used.
Rename it to circled.yaml (i.e. cp circled.trace.yaml circled.yaml) and follow along the
discussions in chapter Symbolic Execution.
Setup
Before collecting concrete execution traces of the target binary circled, the following files need to be set up.
GDB Commands Script
The file circled.trace.gdb is a GNU Project Debugger (GDB) commands
script. As shown in the Figure 3.1 above, Morion
uses GDB to interact with its target during the process of tracing. The script contains GDB commands
that bring the target to the point from which tracing should start (e.g. to follow along and break
the relevant thread when dealing with multi-threaded binaries, as it is the case with circled). As
show below, the trace can then be collected with the command morion_trace, a custom GDB command
implemented by Morion (usage:
morion_trace [debug] <trace_file_yaml:str> <stop_addr:int> [<stop_addr:int> [...]]).
Alongside some stop addresses, morion_trace expects as argument a YAML file, into which the trace
will be stored. As explained below in section YAML File, the
inputted YAML file can hold additional information that steers how the trace will be collected (e.g.
by hooking certain functions).
[...]
# Addresses
[...]
set $before_vulnerability = 0xcfc0
[...]
# Break before vulnerability
break *$before_vulnerability
continue
# Trace till return of function updating_database (address 0xf1a4)
morion_trace debug circled.yaml 0xf1a4
[...]
As can be seen in the code excerpt above, the trace we intend to collect should start/stop at
addresses 0xcfc0 and 0xf1a4, respectively. Start and stop addresses of the trace need to be
selected adequately for the intended purpose. In our specific case where we intend to generate an
exploit for CVE-2022-27646 (see also Exploitation), this means that the
trace should include both the points where attacker-controllable inputs are introduced and where
these inputs lead to a potential vulnerability (e.g. the point the binary is crashing due to a
memory violation condition - as for instance found by a fuzzing campaign).
DEMO Tracing/Setup/GDB_Commands_Script - Click the image below to watch on YouTube:
YAML File
Next, the file circled.init.yaml needs to be defined. It typically
includes information about the trace's entry state (states:entry:), as well as about functions
that should be hooked (hooks:).
States
Typically, the circled.init.yaml file first defines information about
the trace's entry state (states:entry:). More specifically, we define concrete register and/or
memory values, that Morion - respectively GDB -
will set before collecting the trace (see also
Loading the Trace File).
[...]
states:
entry:
regs:
mems:
'0x000120f8': ['0x25'] # '%'
'0x000120f9': ['0x73'] # 's'
'0x000120fa': ['0x20'] # ' '
'0x000120fb': ['0x25'] # '%'
'0x000120fc': ['0x73'] # 's'
'0x000120fd': ['0x00'] #
[...]
In the example of binary circled above, we manually set a format string %s %s. Within the trace
that we are about to collect, this format string is solely used by the function sscanf - a
function that we hook (see next section on Hooks) and in consequence, do not trace all of its
assembly instructions. Due to skipping the function's instructions,
Morion does not record all memory locations
accessed by it, which is why we need to add them manually.
Here and in other places, Morion is designed with
the intention to give an analyst extensive configuration flexibilities, so that cases can be handled
where the tool does not (yet) implement full automation. In the example of sscanf, a future
hooking implementation could improve on this, so that the format string is automatically added to
the accessed memory pool.
The general format to configure the entry state looks like this:
states:
entry:
regs:
'r0': ['0x00', '$$$$$$$$']
mems:
'0x00000000': ['0x00', '$$']
Beside setting concrete values, like 0x00 in the example above, we might also mark certain
registers and/or memory bytes as being symbolic (indicated by the specifier $$). The symbolic
values have not yet any effect during tracing, but will be central during symbolic execution (see
Symbolic Execution).
Hooks
Next, the circled.init.yaml file typically defines information about
hooks (hooks:). A hook is a sequence of consecutive assembly instructions (from an entry to
a leave address) that will not be recorded in the trace. As a consequence, these instructions will
later not be executed by the symbolic execution engine, which takes the recorded trace as input.
Most of the time, hooks will correspond to function calls (such as
0x0000d040 (73 f1 ff eb): bl #0x9614 <fclose@plt>), where the effective symbolic execution of all
included assembly instructions does either not scale, is irrelevant for the intended purpose (e.g.
exploit generation) or the function has well-known semantics that can be mimicked by a semantic
function model.
[...]
hooks:
lib:
func_hook:
- {entry: '0xd040', leave: '0xd044', mode: 'skip'} # fclose@plt
[...]
- {entry: '0xc9c4', leave: '0xc9c8', mode: 'skip'} # free@plt
libc:
fgets:
- {entry: '0xcfe0', leave: '0xcfe4', mode: 'model'} # fgets@plt
- {entry: '0xd094', leave: '0xd098', mode: 'model'} # fgets@plt
sscanf:
- {entry: '0xcffc', leave: '0xd000', mode: 'model'} # sscanf@plt
[...]
As can be seen in the code excerpt above, hooks include - beside entry and leave addresses - a
parameter mode. This is only relevant during symbolic execution and will therefore be explained
in chapter Symbolic Execution. More details regarding hooking during trace
collection can be found in section How Hooking Works below.
Note: As mentioned before, Morion generally
intends to favor configuration flexibility over full automation. Therefore, leave addresses of
hooks (currently) need to be configured manually, since in general, the return address of a function
is hard to determine (e.g. tail calls). And more importantly,
Morion's hooking feature intends not to be limited
to function calls, but be applicable in more generic cases, i.e. for any sequence of subsequent
assembly instructions.
DEMO Tracing/Setup/YAML_File - Click the image below to watch on YouTube:
Run
Use the following steps to create a trace of the binary circled, while it is targeted with a proof-of-vulnerability (PoV) payload (as for instance being identified by a fuzzer):
- Start a HTTP server, delivering the PoV payload:
- System: ARMHF Guest
- Command:
python3 ./server/circled.server.py --payload "pov"
- Emulate the binary circled with GDB attached (and therefore not using ASRL):
- System: ARMHF Guest (chroot)
- Command:
/circled.driver.sh --gdb
- Collect an execution trace of the binary circled:
- System: Analysis / Host (morion)
- Command:
cd morion/ # Ensure to be within the correct directory cp circled.init.yaml circled.yaml # Start with a fresh circled.yaml file gdb-multiarch -q -x circled.trace.gdb # Use GDB for cross-platform remote trace collection
DEMO Tracing/Run - Click the image below to watch on YouTube:
Discussion
In the following, we discuss some aspects of the tracing process as implemented by Morion.
Loading the Trace File
As seen above, the file circled.yaml (initially a copy of
circled.init.yaml) may define concrete register
(states:entry:regs:) and/or memory (states:entry:mems:) values, which are set (using GDB)
before starting the actual tracing process:
[...]
[2024-08-20 14:16:07] [INFO] Start loading trace file 'circled.yaml'...
[2024-08-20 14:16:07] [DEBG] Regs:
[2024-08-20 14:16:07] [DEBG] Mems:
[2024-08-20 14:16:07] [DEBG] 0x000120f8 = 0x25 %
[2024-08-20 14:16:07] [DEBG] 0x000120f9 = 0x73 s
[2024-08-20 14:16:07] [DEBG] 0x000120fa = 0x20
[2024-08-20 14:16:07] [DEBG] 0x000120fb = 0x25 %
[2024-08-20 14:16:07] [DEBG] 0x000120fc = 0x73 s
[2024-08-20 14:16:07] [DEBG] 0x000120fd = 0x00
[...]
Also, the hooks defined in circled.yaml are applied (using GDB), so that they take effect
(see also How Hooking Works) when collecting the concrete
execution trace:
[...]
[2024-08-20 14:16:07] [DEBG] Hooks:
[2024-08-20 14:16:07] [DEBG] 0x0000d040 'lib:func_hook (on=entry, mode=skip)'
[2024-08-20 14:16:07] [DEBG] 0x0000d044 'lib:func_hook (on=leave, mode=skip)'
[...]
[2024-08-20 14:16:07] [DEBG] 0x0000c9c4 'lib:func_hook (on=entry, mode=skip)'
[2024-08-20 14:16:07] [DEBG] 0x0000c9c8 'lib:func_hook (on=leave, mode=skip)'
[2024-08-20 14:16:07] [DEBG] 0x0000cfe0 'libc:fgets (on=entry, mode=model)'
[2024-08-20 14:16:07] [DEBG] 0x0000cfe4 'libc:fgets (on=leave, mode=model)'
[2024-08-20 14:16:07] [DEBG] 0x0000d094 'libc:fgets (on=entry, mode=model)'
[2024-08-20 14:16:07] [DEBG] 0x0000d098 'libc:fgets (on=leave, mode=model)'
[2024-08-20 14:16:07] [DEBG] 0x0000cffc 'libc:sscanf (on=entry, mode=model)'
[2024-08-20 14:16:07] [DEBG] 0x0000d000 'libc:sscanf (on=leave, mode=model)'
[...]
[2024-08-20 14:16:07] [INFO] ... finished loading trace file 'circled.yaml'.
[...]
Once this is done, the actual tracing can start.
Collecting the Trace
Collecting a trace includes the recording of the following pieces of information:
- Executed assembly instructions (e.g.
0x0000cfc0 (64 37 65 e5): strb r3, [r5, #-0x764]!) - Initial values of all accessed registers and memory locations (e.g.
r3 = 0x0,r5 = 0xbeffd078or0xbeffc914 = 0x00)
[...]
[2024-08-20 14:16:07] [INFO] Start tracing...
[2024-08-20 14:16:07] [DEBG] 0x0000cfc0 (64 37 65 e5): strb r3, [r5, #-0x764]! # store 1st assembly instruction
[2024-08-20 14:16:07] [DEBG] Regs:
[2024-08-20 14:16:07] [DEBG] r3 = 0x0 # store value of accessed register r3 (initial access)
[2024-08-20 14:16:07] [DEBG] r5 = 0xbeffd078 # store value of accessed register r5 (initial access)
[2024-08-20 14:16:07] [DEBG] Mems:
[2024-08-20 14:16:07] [DEBG] 0xbeffc914 = 0x00 # store value of memory 0xbeffc914 (initial access)
[2024-08-20 14:16:07] [DEBG] 0x0000cfc4 (64 32 9f e5): ldr r3, [pc, #0x264] # store 2nd assembly instruction
[2024-08-20 14:16:07] [DEBG] Regs: # ignore value of accessed register r3 (stored before)
[2024-08-20 14:16:07] [DEBG] Mems:
[2024-08-20 14:16:07] [DEBG] 0x0000d230 = 0xbc # store value of memory 0x0000d230 (initial access)
[2024-08-20 14:16:07] [DEBG] 0x0000d231 = 0x6a j # store value of memory 0x0000d231 (initial access)
[2024-08-20 14:16:07] [DEBG] 0x0000d232 = 0xff # store value of memory 0x0000d232 (initial access)
[2024-08-20 14:16:07] [DEBG] 0x0000d233 = 0xff # store value of memory 0x0000d233 (initial access)
[...]
The initial values of register (states:entry:regs:) and memory locations (states:entry:mems:)
are stored, so that they can later be set in the symbolic context. This is needed so that the
symbolic execution engine uses the correct concrete values.
The collected information (instructions and initial values) is stored in the file circled.yaml,
i.e. the file is updated as shown in the next code excerpt. The file circled.yaml serves as input
for subsequent symbolic execution runs (see also Symbolic Execution).
[...]
trace:
instructions:
- ['0x0000cfc0', 64 37 65 e5, 'strb r3, [r5, #-0x764]!', '']
- ['0x0000cfc4', 64 32 9f e5, 'ldr r3, [pc, #0x264]', '']
[...]
- ['0x0000cf20', 03 db 8d e2, 'add sp, sp, #0xc00', '']
- ['0x0000cf24', f0 8f bd e8, 'pop {r4, r5, r6, r7, r8, sb, sl, fp, pc}', '']
states:
entry:
addr: '0x0000cfc0'
regs:
[...]
r3: ['0x00000000']
[...]
r5: ['0xbeffd078']
[...]
mems:
'0x0000d230': ['0xbc']
'0x0000d231': ['0x6a']
'0x0000d232': ['0xff']
'0x0000d233': ['0xff']
[...]
'0x000120f8': ['0x25'] # '%'
'0x000120f9': ['0x73'] # 's'
'0x000120fa': ['0x20'] # ' '
'0x000120fb': ['0x25'] # '%'
'0x000120fc': ['0x73'] # 's'
'0x000120fd': ['0x00'] #
[...]
'0xbeffc914': ['0x00']
[...]
[...]
If we look at the end of the tracing process's debug output, we can observe that the trace did not
end at our configured stop address 0xf1a4, but at address 0xcf24:
[...]
[2024-08-20 14:16:18] [DEBG] 0x0000cf20 (03 db 8d e2): add sp, sp, #0xc00
[2024-08-20 14:16:18] [DEBG] Regs:
[2024-08-20 14:16:18] [DEBG] Mems:
[2024-08-20 14:16:18] [DEBG] 0x0000cf24 (f0 8f bd e8): pop {r4, r5, r6, r7, r8, sb, sl, fp, pc}
[2024-08-20 14:16:18] [DEBG] Regs:
[2024-08-20 14:16:18] [DEBG] Mems:
[2024-08-20 14:16:18] [DEBG] 0xbeffd094 = 0x41 A
[2024-08-20 14:16:18] [DEBG] 0xbeffd095 = 0x41 A
[...]
[2024-08-20 14:16:18] [DEBG] 0xbeffd082 = 0x41 A
[2024-08-20 14:16:18] [DEBG] 0xbeffd083 = 0x41 A
[2024-08-20 14:16:18] [ERRO] Failed to execute instruction at address 0x0000cf24: 'Remote connection closed'
[2024-08-20 14:16:18] [INFO] ... finished tracing (pc=0x0000cf24).
[2024-08-20 14:16:18] [INFO] Start storing trace file 'circled.yaml'...
[2024-08-20 14:16:21] [INFO] ... finished storing trace file 'circled.yaml'.
This is due to the fact, that our target binary crashed before reaching the intended stop address.
More specifically, and as we will see in greater detail later on, the instruction
0x0000cf24 (f0 8f bd e8): pop {r4, r5, r6, r7, r8, sb, sl, fp, pc} tried to pop a value from the
stack that led to an invalid program counter (pc register), and in consequence, resulted in a
segmentation fault (segfault). We will learn later on how symbolic execution
can help us to decide whether this situation is exploitable or not, and if
so, how we can do it.
DEMO Tracing/Discussion/Collecting_the_Trace - Click the image below to watch on YouTube:
How Hooking Works
As mentioned before, hooking allows a specified sequence of assembly instructions (e.g. corresponding to a called function) not to be added to the trace. In consequence, these instructions will later on not be executed by the symbolic execution engine and have therefore no effect on the symbolic state. Typically, this is required to address scalability issues of symbolic execution or to abstract away environmental interactions (e.g. with 3rd party libraries, inter-process communications, Kernel, device drivers, coprocessors, etc.).
Below, we discuss how the hooking of two concrete libc functions looks like, while Morion collects a trace.
Abstract Function Hook with Mode Skip (Example libc:fclose)
The circled.init.yaml file defines a hook for entry and leave
addresses 0xd040 and 0xd044, respectively. The corresponding entry is located under the key
hooks:lib:func_hook:, which means that an abstract hooking mechanism for functions should be used
(see
morion/tracing/gdb/hooking/lib
for implementation details), as compared to a specific one, which will be the case in the second
example below. The abstract function hooking mechanism will skip the actual assembly
instructions of the function, and instead inject instructions that move the function's concrete
return value to the appropriate return register(s) (r0/r1 for ARMv7 architectures). This is
needed so that during symbolic execution the return register(s) hold the correct concrete value(s)
and the symbolic execution proceeds in synchronization with the concrete one.
The described behavior can be observed in Morion's
debug output below. Instructions with addresses 0xd040, 0x1000 - 0x1010 have been injected by
Morion to set the correct concrete return value(s)
of the function. The last injected instruction at address 0x1010 transfers control back to the
instruction at the leave address (0x0000d044 (04 30 9d e5): ldr r3, [sp, #4]).
Note: Morion also implements the concept of
hooking arbitrary sequences of assembly instructions ("hooks:lib:inst_hook:"), not necessarily
belonging to function calls. These are similar to the ones regarding functions, but do not inject
any instructions for setting return values.
[...]
[2024-08-20 14:16:13] [DEBG] 0x0000d03c (08 00 a0 e1): mov r0, r8
[2024-08-20 14:16:13] [DEBG] Regs:
[2024-08-20 14:16:13] [DEBG] Mems:
[2024-08-20 14:16:13] [INFO] --> Hook: 'lib:func_hook (on=entry, mode=skip)'
[2024-08-20 14:16:13] [INFO] 'func_hook'
[2024-08-20 14:16:13] [DEBG] 0x0000d040 (ee cf ff ea): b #-0xc040 # // Hook: lib:func_hook (on=entry, mode=skip)
[2024-08-20 14:16:13] [INFO] ---
[2024-08-20 14:16:13] [DEBG] 0x00001000 (00 00 a0 e3): mov r0, #0x0 # // Hook: lib:func_hook (on=leave, mode=skip)
[2024-08-20 14:16:13] [DEBG] 0x00001004 (00 00 40 e3): movt r0, #0x0 # // Hook: lib:func_hook (on=leave, mode=skip)
[2024-08-20 14:16:13] [DEBG] 0x00001008 (01 10 a0 e3): mov r1, #0x1 # // Hook: lib:func_hook (on=leave, mode=skip)
[2024-08-20 14:16:13] [DEBG] 0x0000100c (00 10 40 e3): movt r1, #0x0 # // Hook: lib:func_hook (on=leave, mode=skip)
[2024-08-20 14:16:13] [DEBG] 0x00001010 (0b 30 00 ea): b #0xc034 # // Hook: lib:func_hook (on=leave, mode=skip)
[2024-08-20 14:16:13] [INFO] <-- Hook: 'lib:func_hook (on=leave, mode=skip)'
[2024-08-20 14:16:13] [DEBG] 0x0000d044 (04 30 9d e5): ldr r3, [sp, #4]
[2024-08-20 14:16:13] [DEBG] Regs:
[2024-08-20 14:16:13] [DEBG] Mems:
[2024-08-20 14:16:13] [DEBG] 0xbeffc084 = 0x06
[2024-08-20 14:16:13] [DEBG] 0xbeffc085 = 0x00
[2024-08-20 14:16:13] [DEBG] 0xbeffc086 = 0x00
[2024-08-20 14:16:13] [DEBG] 0xbeffc087 = 0x00
[...]
Specific Function Hook with Mode Model (Example libc:fgets)
In general, not only function return values (as discussed in the previous section), but all side-effects with respect to registers and/or memory locations need to be covered, in order for the symbolic execution to be correct. This is why more specific function hook implementations might be needed.
One such function, with rather simple to cover side-effects, is fgets from libc
(synopsis: char *fgets(char *s, int n, FILE *stream)). The function reads a maximum of n-1 bytes
from a file stream to an address given by s (newline or end-of-file conditions can make the
function read less bytes).
In the file circled.init.yaml, the hook for function fgets is
defined under the key hooks:libc:fgets:. Morion
will therefore apply the specific fgets implementation as defined in file
morion/tracing/gdb/hooking/libc.
As can be seen in the output below, Morion
injected instructions (addresses 0xcfe0, 0x1000 - 0x6008) that move the concrete string read
by fgets (which actually corresponds to the PoV payload served by the HTTP server) to the
appropriate memory addresses.
[...]
[2024-08-20 14:16:08] [DEBG] 0x0000cfdc (05 00 a0 e1): mov r0, r5
[2024-08-20 14:16:08] [DEBG] Regs:
[2024-08-20 14:16:08] [DEBG] r0 = 0x21a90
[2024-08-20 14:16:08] [DEBG] Mems:
[2024-08-20 14:16:08] [INFO] --> Hook: 'libc:fgets (on=entry, mode=model)'
[2024-08-20 14:16:08] [INFO] 'char *fgets(char *restrict s, int n, FILE *restrict stream);'
[2024-08-20 14:16:08] [INFO] s = 0xbeffc914
[2024-08-20 14:16:08] [INFO] n = 1024
[2024-08-20 14:16:08] [INFO] stream = 0x00021a90
[2024-08-20 14:16:08] [DEBG] 0x0000cfe0 (06 d0 ff ea): b #-0xbfe0 # // Hook: libc:fgets (on=entry, mode=model)
[2024-08-20 14:16:08] [INFO] ---
[2024-08-20 14:16:08] [INFO] s = 0xbeffc914
[2024-08-20 14:16:08] [INFO] *s = 'AAA[...]AAA X'
[2024-08-20 14:16:09] [DEBG] 0x00001000 (14 09 0c e3): mov r0, #0xc914 # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00001004 (ff 0e 4b e3): movt r0, #0xbeff # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00001008 (41 10 a0 e3): mov r1, #0x41 # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x0000100c (00 10 40 e3): movt r1, #0x0 # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00001010 (00 10 c0 e5): strb r1, [r0] # // Hook: libc:fgets (on=leave, mode=model)
[...]
[2024-08-20 14:16:09] [DEBG] 0x00005fec (13 0d 0c e3): mov r0, #0xcd13 # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00005ff0 (ff 0e 4b e3): movt r0, #0xbeff # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00005ff4 (00 10 a0 e3): mov r1, #0x0 # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00005ff8 (00 10 40 e3): movt r1, #0x0 # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00005ffc (00 10 c0 e5): strb r1, [r0] # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00006000 (14 09 0c e3): mov r0, #0xc914 # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00006004 (ff 0e 4b e3): movt r0, #0xbeff # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [DEBG] 0x00006008 (f5 1b 00 ea): b #0x6fdc # // Hook: libc:fgets (on=leave, mode=model)
[2024-08-20 14:16:09] [INFO] <-- Hook: 'libc:fgets (on=leave, mode=model)'
[2024-08-20 14:16:09] [DEBG] 0x0000cfe4 (00 00 50 e3): cmp r0, #0
[...]
The implementation of all a function's side-effects might not always be so simple as in the example
of fgets. In consequence, simplifications/abstractions might sometimes be needed, which as a
drawback might introduce inconsistencies between the effective concrete and symbolic execution.
Depending on the intended task that you intend to solve with symbolic execution, this might or might
not be acceptable.