aerosec / jetset

GNU General Public License v2.0
49 stars 6 forks source link

Running Jetset on additional binaries #4

Closed DNA-Broker closed 1 year ago

DNA-Broker commented 1 year ago

Hi, I am trying to run JetSet on an additional binary, but I am having no luck. I am trying to run it on the GPS tracker binary located at:

https://github.com/fuzzware-fuzzer/fuzzware-experiments/blob/main/02-comparison-with-state-of-the-art/uEmu/uEmu.GPSTracker/uEmu.GPSTracker.elf

I have set up a gps_config.py file with the following contents:

from device.base_device import Simmio
import angr
import cle

peripherals = Simmio( lower=0x40000000,
                 upper=0x5FFFFFFF,
                 name='peripherals')

regions = [peripherals]

def get_project():        
    p = angr.Project("../jetset_public_data/uEmu.GPSTracker.elf", auto_load_libs=False)
    return p

target = 0x0008480f
arch = "arm"
arch_num = 1

I have also added a gps entry to socs.py as well as a run_gps.sh script with the following:

#!/usr/bin/env bash
$( dirname "${BASH_SOURCE[0]}" )/build/arm-softmmu/qemu-system-arm -machine stm32f4 \
  -m 256 \
  -initial_pc 0x837a1 \
  -initial_sp 0x20088000 \
  -kernel $(dirname "${BASH_SOURCE[0]}")/../jetset_public_data/uEmu.GPSTracker.elf \
  -serial stdio \
  -d nochain -singlestep -S -qmp tcp:localhost:$1,server,nowait

In addition I have added the following to the makefile:

run_gps:
    source jetset_env/bin/activate && cd $(ENGINE_BASE) && python $(ENGINE_SCRIPT) --soc=gps -o=gps_device.c --cmdfile ../jetset_qemu/run_gps.sh --useFunctionPrologues

However, when I run it with make run_gps all I get is the follwing in terminal.

image

This just runs forever, but xterm and qemu both open.

Is there something I am missing in order to get this running on additional binaries?

maxwell-bland commented 1 year ago

Hello, thanks for your effort.

One of three things is happening. These are research questions that I wanted to address in the original work but I've been sidetracked breaking redactions, haha.

(1) There are function calls called "TCG helper operations" that also need to be taint-tracked inside QEMU for the symbolic execution to work correctly for some microarch (assembly) instructions and features (e.g. task-switching). No existing work has implemented taint tracking for all of these operations as the work required would be excessive (re-implementing an entire microarch), even some questionable claims to having implemented SE support for QEMU automatically. You may have such an operation on your codepath and it may be important. You can instrument the TCG interpreter in QEMU to find out (see the other issue I opened on this repo).

(2) The search strategy is getting itself stuck into a bad position. In general, finding the correct program path n a binary is hard, but for whatever reason the academic security community doesn't like acknowledging this and I was ... discouraged .... to put it lightly, from being able to address this in the paper. One solution is to record the set of decisions that get made and walk along with them while performing some reverse engineering to figure out where it gets stuck, and implementing a different strategy.

For 1 and 2, I may also be able to get you access to a new project that I think solves these problems (and others), but is a radically different architecture and approach to the problem of firmware rehosting (and you may not want this, since it isn't "published" yet and ... given what I know of the academic process, may never be). Email me and I can send you the code.

(3) There's some bug in the taint tracking. During the process, I argued we should be making unit tests and was made fun of by the coauthors. To track it down, uncomment many of the print statements I made in the TCG interpreter and track down where either (1) a symbolic decision is not being made when it should be or (2) the wrong decision is being made, likely because of some incorrect symbolic constraints.

When/if you do find the solution, please make a pull request! I've wanted to work on Jetset but have not been able to for innumerable reasons.

Maxwell