alternatingcontrolflowreconstruction's Introduction

ACFR

Overview

ACFR stands for Alternating Control Flow Reconstruction and is a project whose goal is to reconstruct precise control flow of x86 binaries using under and over-approximation alternatingly. The over-approximation is done with the static analysis tool Jakstab and the under-approximation with the symbolic execution engine of Manticore.

Installation

The tool does currently only support debian-based operating systems and has only been tested on Ubuntu 18.04.

Dependencies:

Python 3.6+
Java
Manticore
z3
nasm

Note that the dependencies can be installed automatically by executing the installDependencies.sh script.

Installation instructions

To install the program, cd into the root directory. Then simply execute the setup and compile script:

./setup.sh
./compile.sh

Usage

Open two terminals. In one, cd into the symbolicExecution folder and execute:

python manticoreServer.py [port]

where [port] is a free port.

Then, use the other terminal to run jakstab. This can be done by executing:

jak -m [binary] [options] --dse [port]

where [binary] is the binary to analyze, [options] are optional options to pass to jakstab and [port] is the port specified for the manticore server. Note that the version of Jakstab in this repository contains options for configuring how dse is used in addition to the original options.

Documentation

For people who desire to modify the tool, a large portion of the code has been documented using comments. Futhermore, jakstab includes a brief description of all the options available which is printed to stdout when the binary is executed without any options. For information concerning the theorethical aspects of the tool, we recommend consulting the Master Thesis of Thomas Peterson.

Questions

Send an email to [email protected] or create an issue using the issue board.

alternatingcontrolflowreconstruction's People

Contributors

Stargazers

Watchers

alternatingcontrolflowreconstruction's Issues

Off by one error when checking which section an address belongs to

Describe the bug
When checking which section an address belongs to there is an off-by-one error for ELF binaries. Thus, if an address corresponds to the first bytes of a section. Jakstab claims that it belongs to the section before the one it actually belongs to.

To Reproduce
Find a binary which jumps to the first byte of the .text section. Jakstab will stop the analysis, claiming that there was a jump outside the text section.

Expected behavior
Jakstab should have continued the analysis when execution flowed to the first bytes of the .text section.

Update:
Screenshots
Fix:

Pure symbolic execution

Currently, only STDIN and argv are symbolic. It would be good to look into how argv, files and sockets could be included into the symbolic execution.

The way the lessOrEqual operator is implemented for the interval domain is incorrect

Describe the bug
When the lessOrEqual operator is applied to two strided interval, it will sometimes erroneously return false. Consequently, the CPA algorithm will think it never reaches a fixpoint and thus jakstab will never finish its execution.

To Reproduce
(This example contains the exact values I used to trigger the bug)
Create an interval domain state which has an interval I1= {ret=5[134512741,2147483646]}and another interval I2 = {ret=0[134512746]}
Now, check if the interval I2 is lessOrEqual to I1. The function will erroneously return false.

Expected behavior
The lessOrEqual function should return true when checking if a zero-strided interval is part of a larger interval which it is indeed part of.

Screenshots
This is the erroneous lessOrEqual function of the strided interval domain(It does not capture all cases correctly):

Exported jakstab path might be infeasible

Currently, each instruction has a prev pointer. However, there are special cases when conditional jumps are used, where this doesn't work.

A solution could be to set a prev pointer to each abstract state.

Recommend Projects

tpetersonkth / alternatingcontrolflowreconstruction Goto Github PK