Updated links

This commit is contained in:
Damian Pfammatter
2024-07-15 07:57:35 +02:00
parent f6fa1306f0
commit 86c4e481af
7 changed files with 166 additions and 187 deletions
+11 -13
View File
@@ -1,22 +1,20 @@
# Exploiting a Stack Buffer Overflow on the NETGEAR R6700v3 (CVE-2022-27646) with the Help of Symbolic Execution
<!--TODO--------------------------------------------------------------------------------------------
- [ ] Add all external references
--------------------------------------------------------------------------------------------------->
## Introduction
This repository is intended to demonstrate some functionalities of
[Morion](https://github.com/pdamian/morion), a proof-of-concept (PoC) tool to experiment with
**symbolic execution** on real-world (ARMv7) binaries. We show some of
[Morion](https://github.com/pdamian/morion)'s capabilities by giving a concrete example, namely, how
it can assist during the process of creating a working **exploit for CVE-2022-27646** - a stack
buffer overflow vulnerability in NETGEAR R6700v3 routers (affected version 1.0.4.120_10.0.91, fixed
in later versions).
[Morion](https://github.com/cyber-defence-campus/morion), a proof-of-concept (PoC) tool to
experiment with **symbolic execution** on real-world (ARMv7) binaries. We show some of
[Morion](https://github.com/cyber-defence-campus/morion)'s capabilities by giving a concrete
example, namely, how it can assist during the process of creating a working
**exploit for CVE-2022-27646** - a stack buffer overflow vulnerability in NETGEAR R6700v3 routers
(affected version 1.0.4.120_10.0.91, fixed in later versions).
The repository contains all **files** (under [firmware](./firmware/), [libcircled](./libcircled/),
[morion](./morion/) and [server](./server/)) needed to follow along (e.g. scripts to emulate the
vulnerable ARMv7 binary) and reproduce the discussed steps of how to use
[Morion](https://github.com/pdamian/morion). The **documentation** (under [docs](./docs/) and
[logs](./logs/)), to demonstrate [Morion](https://github.com/pdamian/morion)'s workings, contains
the following chapters:
[Morion](https://github.com/cyber-defence-campus/morion). The **documentation**
(under [docs](./docs/) and [logs](./logs/)), to demonstrate
[Morion](https://github.com/cyber-defence-campus/morion)'s workings, contains the following
chapters:
1. [Setup](docs/1_setup.md) - Explains how to setup analysis (running *Morion*) and target systems
(running target binary *circled*).
2. [Emulation](docs/2_emulation.md) - Explains how to emulate the vulnerable target binary.
@@ -30,7 +28,7 @@ the following chapters:
crafting an exploit.
## References
- Morion PoC Tool:
- https://github.com/pdamian/morion
- https://github.com/cyber-defence-campus/morion
- Defeating the NETGEAR R6700v3:
- https://www.synacktiv.com/en/publications/pwn2own-austin-2021-defeating-the-netgear-r6700v3.html
- Emulating, Debugging and Exploiting NETGEAR R6700v3 *cicled* Binary:
+5 -6
View File
@@ -8,20 +8,19 @@
4. [Symbolic Execution](./4_symbex.md)
5. [Vulnerability CVE-2022-27646](./5_vulnerability.md)
6. [Exploitation](./6_exploitation.md)
<!--TODO--------------------------------------------------------------------------------------------
--------------------------------------------------------------------------------------------------->
# Setup
This chapter lists instructions on how to set up an **analysis system** (also referred to as the
**host system**), which, on the one hand, hosts a **guest system** emulating the targeted ARMv7
binary and, on the other hand, contains [Morion](https://github.com/pdamian/morion) to collect
execution traces that can then be analyzed symbolically.
binary and, on the other hand, contains [Morion](https://github.com/cyber-defence-campus/morion) to
collect execution traces that can then be analyzed symbolically.
## Analysis / Host System
- Install the following dependencies:
- git
- binwalk (https://github.com/ReFirmLabs/binwalk)
- Clone the project repository:
```
git clone https://github.com/pdamian/netgear_r6700v3_circled.git && cd netgear_r6700v3_circled/
git clone https://github.com/cyber-defence-campus/netgear_r6700v3_circled.git && cd netgear_r6700v3_circled/
```
- Extract the R6700v3 firmware with *binwalk*:
```
binwalk -e -M -C firmware/ firmware/R6700v3-V1.0.4.120_10.0.91.zip
@@ -46,7 +45,7 @@ execution traces that can then be analyzed symbolically.
# Copy circled.driver.sh script (wrapper to emulate binary circled)
cp firmware/circled.driver.sh $ROOTFS/circled.driver.sh
```
- Install [Morion](https://github.com/pdamian/morion#installation).
- Install [Morion](https://github.com/cyber-defence-campus/morion#installation).
## ARMHF Guest System
**Note**: In the following, we assume that the variable `$ROOTFS` points to the firmware's root
filesystem, as set in section [Analysis / Host System](./1_setup.md#analysis--host-system).
-3
View File
@@ -11,9 +11,6 @@
4. [Symbolic Execution](./4_symbex.md)
5. [Vulnerability CVE-2022-27646](./5_vulnerability.md)
6. [Exploitation](./6_exploitation.md)
<!--TODO--------------------------------------------------------------------------------------------
- [ ] DNS and TCP redirection
--------------------------------------------------------------------------------------------------->
# Emulation
In this chapter, we briefly mention a handful of **files** and **scripts** that can be used to
emulate the intended target, the binary *circled* from NETGEAR R6700v3 routers (firmware version
+40 -44
View File
@@ -14,10 +14,6 @@
4. [Symbolic Execution](./4_symbex.md)
5. [Vulnerability CVE-2022-27646](./5_vulnerability.md)
6. [Exploitation](./6_exploitation.md)
<!--TODO--------------------------------------------------------------------------------------------
- [ ] Update section Run so that it makes the Setup chapter
- [ ] Review whether all addresses/values are consistent
--------------------------------------------------------------------------------------------------->
# Tracing
In the following, we document how to collect a **concrete execution trace** of our target, a
known vulnerable ARMv7 binary named _circled_ (see
@@ -41,12 +37,12 @@ Before collecting concrete execution traces of the target binary _circled_, the
to be set up.
### GDB Commands Script
The file [circled.trace.gdb](../morion/circled.trace.gdb) is a _GNU Project Debugger (GDB)_ commands
script. As shown in the Figure 3.1 above, [Morion](https://github.com/pdamian/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](https://github.com/pdamian/morion) (usage:
script. As shown in the Figure 3.1 above, [Morion](https://github.com/cyber-defence-campus/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](https://github.com/cyber-defence-campus/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](./3_tracing.md#yaml-file), the
@@ -81,8 +77,8 @@ that should be hooked (`hooks:`).
#### States
Typically, the [circled.init.yaml](../morion/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](https://github.com/pdamian/morion) - respectively _GDB_ - will set
before collecting the trace (see also
memory values, that [Morion](https://github.com/cyber-defence-campus/morion) - respectively _GDB_ -
will set before collecting the trace (see also
[Loading the Trace File](./3_tracing.md#loading-the-trace-file)).
```
[...]
@@ -102,14 +98,14 @@ In the example of binary _circled_ above, we manually set a format string `%s %s
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](https://github.com/pdamian/morion) does not record all memory locations accessed by it,
which is why we need to add them manually.
[Morion](https://github.com/cyber-defence-campus/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](https://github.com/pdamian/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.
Here and in other places, [Morion](https://github.com/cyber-defence-campus/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:
```
@@ -155,13 +151,13 @@ parameter `mode`. This is only relevant during symbolic execution and will there
in chapter [Symbolic Execution](./4_symbex.md). More details regarding hooking during trace
collection can be found in section [How Hooking Works](./3_tracing.md#how-hooking-works) below.
**Note**: As mentioned before, [Morion](https://github.com/pdamian/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](https://github.com/pdamian/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.
**Note**: As mentioned before, [Morion](https://github.com/cyber-defence-campus/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](https://github.com/cyber-defence-campus/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.
## 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):
@@ -187,7 +183,7 @@ _proof-of-vulnerability (PoV)_ payload (as for instance being identified by a fu
```
## Discussion
In the following, we discuss some aspects of the tracing process as implemented by
[Morion](https://github.com/pdamian/morion).
[Morion](https://github.com/cyber-defence-campus/morion).
### Loading the Trace File
As seen above, the file `circled.yaml` (initially a copy of
[circled.init.yaml](../morion/circled.init.yaml)) may define concrete **register**
@@ -330,13 +326,13 @@ or to abstract away **environmental interactions** (e.g. with 3rd party librarie
communications, Kernel, device drivers, coprocessors, etc.).
Below, we discuss how the hooking of two concrete _libc_ functions looks like, while
[Morion](https://github.com/pdamian/morion) collects a trace.
[Morion](https://github.com/cyber-defence-campus/morion) collects a trace.
#### Abstract Function Hook with Mode Skip (Example libc:fclose)
The [circled.init.yaml](../morion/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](https://github.com/pdamian/morion/blob/main/morion/tracing/gdb/hooking/lib.py)
[morion/tracing/gdb/hooking/lib](https://github.com/cyber-defence-campus/morion/blob/main/morion/tracing/gdb/hooking/lib.py)
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
@@ -344,16 +340,16 @@ return value to the appropriate return register(s) (`r0`/`r1` for ARMv7 architec
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](https://github.com/pdamian/morion)'s debug output
below. Instructions with addresses `0xd040`, `0x1000` - `0x1010` have been injected by
[Morion](https://github.com/pdamian/morion) to set the correct concrete return value(s) of the
function. The last injected instruction at address `0x1010` transfers control back to the
The described behavior can be observed in [Morion](https://github.com/cyber-defence-campus/morion)'s
debug output below. Instructions with addresses `0xd040`, `0x1000` - `0x1010` have been injected by
[Morion](https://github.com/cyber-defence-campus/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](https://github.com/pdamian/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.
**Note**: [Morion](https://github.com/cyber-defence-campus/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-04-11 09:53:35] [DEBG] 0x0000d03c (08 00 a0 e1): mov r0, r8
@@ -389,14 +385,14 @@ One such function, with rather simple to cover side-effects, is _fgets_ from _li
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](../morion/circled.init.yaml), the hook for function `fgets` is
defined under the key `hooks:libc:fgets:`. [Morion](https://github.com/pdamian/morion) will
therefore apply the specific _fgets_ implementation as defined in file
[morion/tracing/gdb/hooking/libc](https://github.com/pdamian/morion/blob/main/morion/tracing/gdb/hooking/libc.py).
defined under the key `hooks:libc:fgets:`. [Morion](https://github.com/cyber-defence-campus/morion)
will therefore apply the specific _fgets_ implementation as defined in file
[morion/tracing/gdb/hooking/libc](https://github.com/cyber-defence-campus/morion/blob/main/morion/tracing/gdb/hooking/libc.py).
As can be seen in the output below, [Morion](https://github.com/pdamian/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.
As can be seen in the output below, [Morion](https://github.com/cyber-defence-campus/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-04-11 09:53:30] [DEBG] 0x0000cfdc (05 00 a0 e1): mov r0, r5
+56 -61
View File
@@ -12,23 +12,17 @@
3. [Analyzing Symbolic State](./4_symbex.md#analyzing-symbolic-state)
5. [Vulnerability CVE-2022-27646](./5_vulnerability.md)
6. [Exploitation](./6_exploitation.md)
<!--TODO--------------------------------------------------------------------------------------------
- [ ] Does ARMv7 really use registers `r0` and `r1` for return values?
- [ ] Change text of links and validate them
- [ ] Refer to a page as chapter (not section)
- [ ] Review whether all addresses/values are consistent
--------------------------------------------------------------------------------------------------->
# Symbolic Execution
Chapter [Tracing](./3_tracing.md) explained how to collect a concrete execution trace of your
target, which in our specific case is the ARMv7 binary _circled_. If you followed along the given
instructions, this trace was stored in the file `circled.yaml`. As we will see below, this trace
file may then be used as input for the different **analysis modules** implemented by
[Morion](https://github.com/pdamian/morion). These analysis modules execute the collected trace
**symbolically**, which then allows for reasoning about the target's behavior by solving constraints
for specified mathematical problems. An example for such a problem might for instance be the
question of whether or not it is possible for the program counter (register `pc`) to become a
certain value, and if so, how this can be achieved (e.g. leading to a control-flow hijacking
condition).
[Morion](https://github.com/cyber-defence-campus/morion). These analysis modules execute the
collected trace **symbolically**, which then allows for reasoning about the target's behavior by
solving constraints for specified mathematical problems. An example for such a problem might for
instance be the question of whether or not it is possible for the program counter (register `pc`) to
become a certain value, and if so, how this can be achieved (e.g. leading to a control-flow
hijacking condition).
<hr>
<figure>
<img src="../images/Morion_Overview.svg" alt="Morion Overview"/>
@@ -40,9 +34,9 @@ condition).
<hr>
## Setup
Before running one of [Morion](https://github.com/pdamian/morion)'s symbolic analysis modules, the
collected trace file `circled.yaml` might optionally be customized. Such **customizations** could
for example be to:
Before running one of [Morion](https://github.com/cyber-defence-campus/morion)'s symbolic analysis
modules, the collected trace file `circled.yaml` might optionally be customized. Such
**customizations** could for example be to:
- Mark (additional) register values or memory locations as being symbolic (in the entry state)
- Modify the parameter `mode` of hooked functions
- Add/remove assembly instructions to/from the trace
@@ -70,10 +64,10 @@ Remember that if you followed along the instructions in chapter [Tracing](./3_tr
was collected while the vulnerable binary processed a sample payload leading to a
**crasher/segfault** (as might have been identified by a fuzzer).
### Analysis Modules
[Morion](https://github.com/pdamian/morion) implements different analysis modules that are based on
symbolic execution. The chosen design attempts to make [Morion](https://github.com/pdamian/morion)
easily **extendable** with new modules. The currently implemented ones are summarized in the table
below:
[Morion](https://github.com/cyber-defence-campus/morion) implements different analysis modules that
are based on symbolic execution. The chosen design attempts to make
[Morion](https://github.com/cyber-defence-campus/morion) easily **extendable** with new modules. The
currently implemented ones are summarized in the table below:
| Module | Description |
|-------------------------|-------------|
@@ -87,18 +81,18 @@ below:
## Discussion
In the following, we discuss some aspects of the symbolic execution process as implemented by
[Morion](https://github.com/pdamian/morion).
[Morion](https://github.com/cyber-defence-campus/morion).
### Loading the Trace File
As explained in section [Tracing: Collecting the Trace](./3_tracing.md#collecting-the-trace), beside
the executed assembly instructions, the initial **concrete values** of all registers and/or memory
locations accessed within the trace are recorded (in our specific example in the file
`circled.yaml`). Before starting the actual symbolic execution, these are used by
[Morion](https://github.com/pdamian/morion) to initialize the corresponding concrete register and/or
memory values within the context of the symbolic execution engine
(which in our case is [Triton](https://triton-library.github.io/)). This assures that the symbolic
execution of the recorded trace uses the correct concrete register and/or memory values. This
initialization of registers and/or memory locations can be observed in
[Morion](https://github.com/pdamian/morion)'s debug output:
[Morion](https://github.com/cyber-defence-campus/morion) to initialize the corresponding concrete
register and/or memory values within the context of the symbolic execution engine (which in our case
is [Triton](https://triton-library.github.io/)). This assures that the symbolic execution of the
recorded trace uses the correct concrete register and/or memory values. This initialization of
registers and/or memory locations can be observed in
[Morion](https://github.com/cyber-defence-campus/morion)'s debug output:
```
[2024-04-11 10:46:19] [INFO] Start loading file 'circled.yaml'...
[2024-04-11 10:46:21] [DEBG] Regs:
@@ -156,10 +150,11 @@ states:
[...]
[...]
```
As can be seen in the excerpt above, [Morion](https://github.com/pdamian/morion) uses the specifier
`$$` for referring to a **symbolic byte**. In the above example, where a symbolic register and a
symbolic memory location were defined, [Morion](https://github.com/pdamian/morion)'s debug output,
while loading the trace file, would look like this:
As can be seen in the excerpt above, [Morion](https://github.com/cyber-defence-campus/morion) uses
the specifier `$$` for referring to a **symbolic byte**. In the above example, where a symbolic
register and a symbolic memory location were defined,
[Morion](https://github.com/cyber-defence-campus/morion)'s debug output, while loading the trace
file, would look like this:
```
[...]
[2024-04-11 10:46:21] [DEBG] r0=0x21ae0
@@ -173,12 +168,12 @@ Note that in our example of binary _circled_, we do not manually mark any regist
location as being symbolic (there are no `$$` specifiers in the entry state of file
[circled.init.yaml](../morion/circled.init.yaml)). Instead, and as will be explained in section
[Symbex: How Hooking Works](./4_symbex.md#how-hooking-works) below, all symbolic variables are
automatically introduced by [Morion](https://github.com/pdamian/morion) and its model for the hooked
`libc` function `fgets`.
automatically introduced by [Morion](https://github.com/cyber-defence-campus/morion) and its model
for the hooked `libc` function `fgets`.
After initializing concrete and/or symbolic values of all necessary registers and/or memory
locations in the context of the symbolic execution engine,
[Morion](https://github.com/pdamian/morion) sets up the defined function **hooks**:
[Morion](https://github.com/cyber-defence-campus/morion) sets up the defined function **hooks**:
```
[...]
[2024-04-11 10:46:21] [DEBG] Hooks:
@@ -208,14 +203,14 @@ In the chapter about tracing (see section
`0xd040` and `0xd044`, respectively. The hook corresponds to a call to function `fclose` (synopsis:
`int fclose(FILE *stream);`) from `libc` (or to be more specific, `uclibc` in case of the binary
_circled_). Due to the hooking, the effective assembly instructions of the function itself have not
been traced. Instead [Morion](https://github.com/pdamian/morion) injected some instructions to
reproduce some of the function's side-effects. Since we used an **abstract function hook**
(`hooks:lib:func_hook:`), the only modelled side-effect corresponds to setting the correct return
value(s). For the ARMv7 architecture that we target, a function's return value is generally stored
in register `r0` (and potentially `r1`). This is exactly what instructions `0x1000` - `0x100c` are
used for. [Morion](https://github.com/pdamian/morion) injected assembly instructions to move the
trace's effective return value of function `fclose` (here `0`, meaning a successful closure of the
corresponding file stream) to the return register(s).
been traced. Instead [Morion](https://github.com/cyber-defence-campus/morion) injected some
instructions to reproduce some of the function's side-effects. Since we used an
**abstract function hook** (`hooks:lib:func_hook:`), the only modelled side-effect corresponds to
setting the correct return value(s). For the ARMv7 architecture that we target, a function's return
value is generally stored in register `r0` (and potentially `r1`). This is exactly what instructions
`0x1000` - `0x100c` are used for. [Morion](https://github.com/cyber-defence-campus/morion) injected
assembly instructions to move the trace's effective return value of function `fclose` (here `0`,
meaning a successful closure of the corresponding file stream) to the return register(s).
```
[...]
[2024-04-11 10:46:22] [DEBG] 0x0000d03c (08 00 a0 e1): mov r0, r8
@@ -233,12 +228,12 @@ corresponding file stream) to the return register(s).
[2024-04-11 10:46:22] [DEBG] 0x0000d044 (04 30 9d e5): ldr r3, [sp, #4]
[...]
```
When running a trace symbolically, [Morion](https://github.com/pdamian/morion) follows along the
recorded instructions (including the ones injected by hooks during tracing) and executes them one by
one using its underlying symbolic execution engine ([Triton](https://triton-library.github.io/) in
our case). For hooks with mode `skip`, no additional modifications of the symbolic state are
performed. As we will see in the next example, this might be different when using a hook with mode
`model`.
When running a trace symbolically, [Morion](https://github.com/cyber-defence-campus/morion) follows
along the recorded instructions (including the ones injected by hooks during tracing) and executes
them one by one using its underlying symbolic execution engine
([Triton](https://triton-library.github.io/) in our case). For hooks with mode `skip`, no additional
modifications of the symbolic state are performed. As we will see in the next example, this might be
different when using a hook with mode `model`.
#### Specific Function Hook with Mode Model (Example libc:fgets)
As mentioned in section [Tracing: How Hooking Works](./3_tracing.md#how-hooking-works), the file
[circled.init.yaml](../morion/circled.init.yaml), beside others, also defines a hook for entry and
@@ -302,9 +297,9 @@ additional function-specific side-effects to the memory and register contexts.
Since we defined a function-specific hook to be used with mode `model`, additional modifications to
the **symbolic state** might be performed. These modifications can happen either at entry or when
leaving the hook. The model implementation of `fgets` (see
[libc.py#L12](https://github.com/pdamian/morion/blob/main/morion/symbex/hooking/libc.py#L12) for
more details), for instance, makes the string `s` symbolic. This means that new symbolic variables
get assigned to each character/byte of the read string.
[libc.py#L12](https://github.com/cyber-defence-campus/morion/blob/main/morion/symbex/hooking/libc.py#L12)
for more details), for instance, makes the string `s` symbolic. This means that new symbolic
variables get assigned to each character/byte of the read string.
But why does one want to make `s` symbolic?
Well, `s` is read in from a resource external to the targeted binary (here a file), which is
@@ -318,20 +313,20 @@ attacker-controllable values, potentially leading to control-flow hijacking atta
**Note**: In case you want to hook invocations of function `fgets` without making the read string
symbolic, define the corresponding hook to use mode `skip`.
**Note**: [Morion](https://github.com/pdamian/morion) is a *proof-of-concept (PoC)* tool intended to be
used for experimenting with symbolic execution on (real-world) (ARMv7) binaries. It currently
implements (only) a handful of hooks for common `libc` functions. These should be extended in future
work (pull requests are welcome).
**Note**: [Morion](https://github.com/cyber-defence-campus/morion) is a *proof-of-concept (PoC)*
tool intended to be used for experimenting with symbolic execution on (real-world) (ARMv7) binaries.
It currently implements (only) a handful of hooks for common `libc` functions. These should be
extended in future work (pull requests are welcome).
### Analyzing Symbolic State
If we symbolize inputs that an attacker can control, symbolic execution not only allows us to see
which parts of a target binary can be influenced, but also how this may happen. At the end of a
symbolic execution run, [Morion](https://github.com/pdamian/morion) for instance analyzes the
**symbolic state** (can be disabled using option `--skip_state_analysis`). This means that an
overview is given about which registers and memory locations are based on symbolic variable(s). In
the example of the collected trace of binary *circled*, one immediately sees that the program
counter (register `pc`) is one of these candidates. Remember that we only marked inputs an attacker
might control as being symbolic, meaning that an attacker can potentially influence the program's
control-flow.
symbolic execution run, [Morion](https://github.com/cyber-defence-campus/morion) for instance
analyzes the **symbolic state** (can be disabled using option `--skip_state_analysis`). This means
that an overview is given about which registers and memory locations are based on symbolic
variable(s). In the example of the collected trace of binary *circled*, one immediately sees that
the program counter (register `pc`) is one of these candidates. Remember that we only marked inputs
an attacker might control as being symbolic, meaning that an attacker can potentially influence the
program's control-flow.
```
[...]
[2024-04-11 10:46:22] [INFO] Start analyzing symbolic state...
+10 -11
View File
@@ -9,13 +9,12 @@
2. [Analysis](./5_vulnerability.md#analysis)
3. [Memory Layout](./5_vulnerability.md#memory-layout)
6. [Exploitation](./6_exploitation.md)
<!--TODO--------------------------------------------------------------------------------------------
--------------------------------------------------------------------------------------------------->
# Vulnerability CVE-2022-27646
Before looking into the details of how [Morion](https://github.com/pdamian/morion) might assist
during [exploit generation](./6_exploitation.md), this chapter provides essential **background
information** necessary for comprehending the targeted vulnerability. For a deeper exploration, we
direct the interested reader to the original writeup by the vulnerability discoverers, available at
Before looking into the details of how [Morion](https://github.com/cyber-defence-campus/morion)
might assist during [exploit generation](./6_exploitation.md), this chapter provides essential
**background information** necessary for comprehending the targeted vulnerability. For a deeper
exploration, we direct the interested reader to the original writeup by the vulnerability
discoverers, available at
[Pwn2own Austin 2021: Defeating the NETGEAR R6700v3](https://www.synacktiv.com/en/publications/pwn2own-austin-2021-defeating-the-netgear-r6700v3.html).
## Description
[CVE-2022-27646](https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2022-27646) corresponds to a
@@ -91,9 +90,9 @@ is encountered).
What registers and memory locations an attacker can influence, and in particular how, is not always
so easy to determine, and typically requires time-consuming reverse engineering and debugging
efforts. As we will see in the next chapter about [Exploitation](./6_exploitation.md), this is where
[Morion](https://github.com/pdamian/morion), respectively **symbolic execution**, might help by
simplifying certain tasks, so that we do not have to understand all subtleties in full detail (e.g.
which bytes we control, are byte values restricted, etc.) to craft a working exploit.
[Morion](https://github.com/cyber-defence-campus/morion), respectively **symbolic execution**, might
help by simplifying certain tasks, so that we do not have to understand all subtleties in full
detail (e.g. which bytes we control, are byte values restricted, etc.) to craft a working exploit.
## Memory Layout
Figure 5.4 below gives an overview of the **memory layout** that results when the file
`circleinfo.txt` contains the content `b'A'*1021 + b' X'` (note that this is exactly the file
@@ -120,8 +119,8 @@ After getting a basic understanding of vulnerability
[CVE-2022-27646](https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2022-27646), it is finally time
for the fun part - the actual **exploitation**! The [next chapter](./6_exploitation.md) tries to
demonstrate that, at least for simple vulnerabilities like the one explained here, and with the help
of a tool like [Morion](https://github.com/pdamian/morion), not even this level of vulnerability
understanding might be necessary to craft a working exploit.
of a tool like [Morion](https://github.com/cyber-defence-campus/morion), not even this level of
vulnerability understanding might be necessary to craft a working exploit.
----------------------------------------------------------------------------------------------------
[Back-to-Top](./5_vulnerability.md#table-of-contents)
+44 -49
View File
@@ -22,19 +22,13 @@
2. [Stage-1 Payload](./6_exploitation.md#stage-1-payload)
3. [Run Final Exploit](./6_exploitation.md#run-final-exploit)
4. [Conclusion](./6_exploitation.md#conclusion)
<!--TODO--------------------------------------------------------------------------------------------
- [ ] Do in all chapters: ``` -> ```shell or ```python
- [ ] Create screencast using morion_pwndbg
- [ ] Remove circled.exploit.md and circled.exploit.py from git repository
- [ ] Recheck links [Symbolic Execution: Analysis Modules](./4_symbex.md#analysis-modules)
- [ ] Morion README: Intended usage - crash triage
--------------------------------------------------------------------------------------------------->
# Exploitation
In this final chapter, we will show the usage of two **analysis modules** provided by
[Morion](https://github.com/pdamian/morion), `morion_control_hijacker` and `morion_rop_generator`
(see also [Symbolic Execution: Analysis Modules](./4_symbex.md#analysis-modules)). We will explain
how they might first help us to build a proof-of-concept (PoC) exploit, which we can then turn into
a powerful exploit, giving us a **reverse shell** on the targeted devices.
[Morion](https://github.com/cyber-defence-campus/morion), `morion_control_hijacker` and
`morion_rop_generator` (see also
[Symbolic Execution: Analysis Modules](./4_symbex.md#analysis-modules)). We will explain how they
might first help us to build a proof-of-concept (PoC) exploit, which we can then turn into a
powerful exploit, giving us a **reverse shell** on the targeted devices.
The first module, `morion_control_hijacker`, allows us to detect situations, where registers that
might influence the control-flow (typically the *pc* register), get a value assigned that relies on
@@ -42,12 +36,12 @@ a symbolic variable. When symbolic variables are assigned to inputs an attacker
helps to identify and reason about **control-flow hijacking** conditions.
Afterwards, we will motivate the usage of a **Return Oriented Programming (ROP)** chain for our
exploit to work. [Morion](https://github.com/pdamian/morion)'s second module mentioned in this
chapter, `morion_rop_generator`, might assist us in building one, given the actual restrictions we
might have. We can give it as inputs a candidate ROP chain (list of ROP gadgets), as well as a list
of preconditions that must be fulfilled (such as `[sp+32] == 0xb8`). The module then determines
whether such a candidate chain is feasible or not, and if so, what the attacker-controllable inputs
must be to trigger it.
exploit to work. [Morion](https://github.com/cyber-defence-campus/morion)'s second module mentioned
in this chapter, `morion_rop_generator`, might assist us in building one, given the actual
restrictions we might have. We can give it as inputs a candidate ROP chain (list of ROP gadgets), as
well as a list of preconditions that must be fulfilled (such as `[sp+32] == 0xb8`). The module then
determines whether such a candidate chain is feasible or not, and if so, what the
attacker-controllable inputs must be to trigger it.
## Analysis Module morion_control_hijacker
In the following, we use and analyze the concrete execution trace we recorded in
[Tracing: Run](./3_tracing.md#run). Remember that the trace was stored to a file named
@@ -55,7 +49,7 @@ In the following, we use and analyze the concrete execution trace we recorded in
`circleinfo.txt`. The file `circleinfo.txt` contained the proof-of-vulnerability (PoV) payload
`"A"*1021 + " X"`.
### Vulnerability Characteristics
Let us start by using [Morion](https://github.com/pdamian/morion)'s analysis module
Let us start by using [Morion](https://github.com/cyber-defence-campus/morion)'s analysis module
`morion_control_hijacker`, with the aforementioned trace as input.
```
$ morion_control_hijacker circled.yaml
@@ -82,13 +76,13 @@ Type quit(), exit() or ctrl-d to leave the interpreter.
In [1]:
```
[Morion](https://github.com/pdamian/morion) stops after the `pop` instruction at address `0xcf24`
and prints the message `Potential control hijack due to unrestricted register 'pc'`. This means that
register *pc* is based on some symbolic variable(s), i.e. in our specific example, is somehow
influenced by contents originating from file `circleinfo.txt`.
[Morion](https://github.com/pdamian/morion) entered an interactive (Python) shell that allows us to
further **investigate** the observed situation. For instance, we can perform a first simple
check to see, whether we can effectively set the *pc* to a different value:
[Morion](https://github.com/cyber-defence-campus/morion) stops after the `pop` instruction at
address `0xcf24` and prints the message `Potential control hijack due to unrestricted register 'pc'`.
This means that register *pc* is based on some symbolic variable(s), i.e. in our specific example,
is somehow influenced by contents originating from file `circleinfo.txt`.
[Morion](https://github.com/cyber-defence-campus/morion) entered an interactive (Python) shell that
allows us to further **investigate** the observed situation. For instance, we can perform a first
simple check to see, whether we can effectively set the *pc* to a different value:
```
In [1]: pc_ast = ctx.getRegisterAst(ctx.registers.pc)
@@ -119,9 +113,9 @@ others, the output of [3] tells us the following:
available [here](https://triton-library.github.io/documentation/doxygen/py_triton_page.html).
We can finish our initial manual investigation by typing `quit` [4]. At the end of the symbolic
trace execution, [Morion](https://github.com/pdamian/morion) lists us a summary about the
**symbolic state**. This gives a quick overview about which registers and memory locations we might
control at the end of the recorded trace.
trace execution, [Morion](https://github.com/cyber-defence-campus/morion) lists us a summary about
the **symbolic state**. This gives a quick overview about which registers and memory locations we
might control at the end of the recorded trace.
```
In [4]: quit
@@ -218,11 +212,11 @@ the address of gadget 1 need to be placed (as we will also see later on). We cho
since it allows to contain a command string of up to 625 characters.
On the one hand, this ROP chain is simple to understand, suitable to demonstrate some features of
[Morion](https://github.com/pdamian/morion), and yet powerful enough to start a reverse shell on the
targeted device (as we will see in a moment). On the other hand, though, it will crash the binary
after function `system` returns, since we do not properly clean up the call stack. For us this is
not a problem, since the binary `circled` restarts after a crash. However, in the more general
sense, a crashing binary might lead to alerts, which threat actors typically want to avoid.
[Morion](https://github.com/cyber-defence-campus/morion), and yet powerful enough to start a reverse
shell on the targeted device (as we will see in a moment). On the other hand, though, it will crash
the binary after function `system` returns, since we do not properly clean up the call stack. For us
this is not a problem, since the binary `circled` restarts after a crash. However, in the more
general sense, a crashing binary might lead to alerts, which threat actors typically want to avoid.
**Note**: Several (open-source) tools (such as [ropper](https://github.com/sashs/Ropper) or
[ROPgadget](https://github.com/JonathanSalwan/ROPgadget)) exist to help find suitable ROP gadgets in
@@ -254,7 +248,7 @@ to defeat ASLR.
Now that we have developed an exploit strategy, let us next create a simple
**proof-of-concept (PoC) exploit**. To do so, we go back to the interactive (Python) shell, as
provided by `morion_control_hijacker`. Instead of manually typing individual commands, we create a
Python script and run it inside of [Morion](https://github.com/pdamian/morion)'s shell
Python script and run it inside of [Morion](https://github.com/cyber-defence-campus/morion)'s shell
(with `run -i <script>`). The first script that we run, is
[circled.rop1.py](../morion/circled.rop1.py#L10) and looks like this:
```python
@@ -276,7 +270,7 @@ We start by modelling **Precondition 0.0**. To do so, we first get the concrete
access the AST representation of the memory location that will be popped to the *pc*. Then we ask
the symbolic execution engine for a solution, such that the *pc* is equal to `0xc9b8`, the address
of gadget 1 as discussed before. We run [circled.rop1.py](../morion/circled.rop1.py) in
[Morion](https://github.com/pdamian/morion)'s shell as shown below:
[Morion](https://github.com/cyber-defence-campus/morion)'s shell as shown below:
```
$ morion_control_hijacker circled.yaml
@@ -327,8 +321,8 @@ We first access the AST representation of register *r6* and require it to be equ
Then we access the AST representation of the memory at this address (here 16 bytes in size) and
require it to match our PoC command string `id>/id;#`. Finally, the symbolic execution engine is
asked to print us a potential solution fulfilling all the specified conditions. We run script
[circled.rop2.py](../morion/circled.rop2.py) in [Morion](https://github.com/pdamian/morion)'s shell
like shown below:
[circled.rop2.py](../morion/circled.rop2.py) in
[Morion](https://github.com/cyber-defence-campus/morion)'s shell like shown below:
```
$ morion_control_hijacker circled.yaml
@@ -366,9 +360,9 @@ In [5]: run -i circled.rop2.py
1434: 15451;;0xbeffc25f;model;fgets@libc(s=0xbeffc0c4,n=1024,stream=0x21ae0);s+411:8 = 0x00
}
```
Like before, [Morion](https://github.com/pdamian/morion) gives us a solution for our problem, i.e.
tells us how to choose the contents of file `circleinfo.txt` to make the exploit work. We
implemented the above solution as a payload that
Like before, [Morion](https://github.com/cyber-defence-campus/morion) gives us a solution for our
problem, i.e. tells us how to choose the contents of file `circleinfo.txt` to make the exploit work.
We implemented the above solution as a payload that
[circled.server.py](../server/circled.server.py#L47) serves when launched with command-line argument
`--payload "poc1"`:
```python
@@ -799,11 +793,11 @@ attaching of the _gdbserver_, i.e. without the flag `--gdb`. You will receive th
once the correct stack address of the system command has been found.
## Conclusion
This repository intended to demonstrate (some of) the current features (and limitations) of the
**PoC tool [Morion](https://github.com/pdamian/morion)** and to enable interested readers to
replicate all listed steps, fostering independent experimentation with the tool. It aimed to show
how **symbolic execution** might assist in understanding the characteristics of a bug, determine its
capabilities to decide whether or not it is exploitable, and if so, support in the process of
crafting an exploit.
**PoC tool [Morion](https://github.com/cyber-defence-campus/morion)** and to enable interested
readers to replicate all listed steps, fostering independent experimentation with the tool. It aimed
to show how **symbolic execution** might assist in understanding the characteristics of a bug,
determine its capabilities to decide whether or not it is exploitable, and if so, support in the
process of crafting an exploit.
We showcased the tool on a real-world vulnerability to proof its **practicability**, however want to
emphasize that the shown vulnerability class, stack-based buffer overflows, are well studied and
@@ -814,10 +808,11 @@ of the listed steps towards a working exploit can of course be done without the
execution. However we believe that symbolic execution is a **powerful technique** that, especially
if used wisely, can support and simplify (at least) certain tasks.
[Morion](https://github.com/pdamian/morion), but also symbolic execution in more general terms,
still have a lot of **limitations** (scalability, modeling interactions with the environment, etc.),
especially when it comes to **real-world binaries**. [Morion](https://github.com/pdamian/morion) is
created with the intention to research and better understand these limits.
[Morion](https://github.com/cyber-defence-campus/morion), but also symbolic execution in more
general terms, still have a lot of **limitations** (scalability, modeling interactions with the
environment, etc.), especially when it comes to **real-world binaries**.
[Morion](https://github.com/cyber-defence-campus/morion) is created with the intention to research
and better understand these limits.
----------------------------------------------------------------------------------------------------
[Back-to-Top](./6_exploitation.md#table-of-contents)