文件列表:

Makefile (1623, 2022-12-16)
datasets/ (0, 2022-12-16)
datasets/b2 (42451, 2022-12-16)
datasets/complex_handlers/ (0, 2022-12-16)
datasets/complex_handlers/bp1 (726, 2022-12-16)
datasets/complex_handlers/bp2 (1298, 2022-12-16)
datasets/complex_handlers/bp3 (8308, 2022-12-16)
datasets/if_the_else/ (0, 2022-12-16)
datasets/if_the_else/merged1 (600, 2022-12-16)
datasets/if_the_else/merged2 (1080, 2022-12-16)
datasets/if_the_else/merged3 (1560, 2022-12-16)
datasets/if_the_else/merged4 (2040, 2022-12-16)
datasets/if_the_else/merged5 (2520, 2022-12-16)
datasets/syntia/ (0, 2022-12-16)
datasets/syntia/b1 (7321, 2022-12-16)
dune-project (662, 2022-12-16)
examples/ (0, 2022-12-16)
examples/bin/ (0, 2022-12-16)
examples/bin/Makefile (64, 2022-12-16)
examples/bin/add.c (91, 2022-12-16)
examples/samples/ (0, 2022-12-16)
examples/samples/example.json (4630, 2022-12-16)
examples/samples/example_8_and_16bits.json (1079, 2022-12-16)
examples/samples/example_8bits.json (789, 2022-12-16)
requirements.txt (99, 2022-12-16)
scripts/ (0, 2022-12-16)
scripts/bench/ (0, 2022-12-16)
scripts/bench/bench.py (8644, 2022-12-16)
scripts/bench/grammars/ (0, 2022-12-16)
scripts/bench/grammars/grammar.lark (498, 2022-12-16)
scripts/bench/sample.py (8818, 2022-12-16)
scripts/utils/ (0, 2022-12-16)
scripts/utils/all_from_trace.sh (5211, 2022-12-16)
scripts/utils/binsec/ (0, 2022-12-16)
scripts/utils/binsec/check_equiv.py (4325, 2022-12-16)
scripts/utils/binsec/extract.ini (58, 2022-12-16)
scripts/utils/binsec/sample.py (13859, 2022-12-16)
scripts/utils/gdbscript.txt (85, 2022-12-16)
... ...

# Table of Contents 1. [Requirements](https://github.com/binsec/xyntia/blob/master/#requirements) 2. [Installation](https://github.com/binsec/xyntia/blob/master/#installation) 3. [Usage](https://github.com/binsec/xyntia/blob/master/#usage) 1. [Synthesizing functions from fun.ml predefined functions](https://github.com/binsec/xyntia/blob/master/#synthesizing-functions-from-funml-predefined-functions) 2. [Synthesizing functions from sampling files](https://github.com/binsec/xyntia/blob/master/#synthesizing-functions-from-sampling-files) 3. [Grammar abbreviations](https://github.com/binsec/xyntia/blob/master/#grammar-abbreviations) 4. [Heuristic abbreviations](https://github.com/binsec/xyntia/blob/master/#heuristic-abbreviations) 4. [Experiments](https://github.com/binsec/xyntia/blob/master/#experiments) 5. [Synthesize all blocks from a execution trace](https://github.com/binsec/xyntia/blob/master/#synthesize-all-blocks-from-a-execution-trace) 6. [Synthesize a specific output](https://github.com/binsec/xyntia/blob/master/#synthesize-a-specific-output) 7. [References](https://github.com/binsec/xyntia/blob/master/#references) # Requirements ## System requirements On debian like systems, run the following command: ``` sudo apt install libgmp3-dev gcc-multilib gdb python3 python3-pip python3-tqdm z3 ``` ## OCaml requirements - [OCaml](https://github.com/binsec/xyntia/blob/master/https://ocaml.org/docs/install.fr.html) (>= 4.09) - [Dune](https://github.com/binsec/xyntia/blob/master/https://github.com/ocaml/dune) (>= 1.11.4) - [Zarith](https://github.com/binsec/xyntia/blob/master/https://github.com/ocaml/Zarith) - [Yojson](https://github.com/binsec/xyntia/blob/master/https://github.com/ocaml-community/yojson) (>= 1.7.0) - [Qcheck](https://github.com/binsec/xyntia/blob/master/https://github.com/c-cube/qcheck/) (>= 0.20) You can install all the packages above with [opam](https://github.com/binsec/xyntia/blob/master/https://opam.ocaml.org/). ## Symbolic execution engine Xyntia is a standalone tool which takes I/O example as input and synthesize a corresponding expression. Still, in practice, you do not want to give these I/O examples by hand. Thus we give scripts to automatically sample them from a given binary. It relies on the Binsec symbolic execution engine: - [Binsec](https://github.com/binsec/xyntia/blob/master/https://binsec.github.io/) (version >= 0.6.3) # Installation First, if you do not have a opam switch for an ocaml version >= 4.09 do: ``` $ opam switch create . 4.09 # or any version >= 4.09 $ eval $(opam env) ``` Then you can install ocaml dependencies presented previously using `opam install `. Finally, to install Xyntia, execute: ``` $ make $ make install ``` # Usage The help of Xyntia is available through `xyntia -help`. In the following we will explain the two ways for using Xyntia. ## Synthesizing functions from fun.ml predefined functions The module Fun from src/fun.ml contains a list of sample functions that can be used to test Xyntia without the need of processing a sampling file. To run Xyntia on one of the functions in Fun, run the following command: ``` $ xyntia [-ops ] [-time ] [-heur ] -nosamp ``` where *grammar* is the abbreviation of the grammar used to define the search space (see below), *time* is the time budget of the synthesis in seconds, *heur* is the abbreviation for the search heuristic to be used (see below), *id* is the index of the function in the list, and *nargs* is the number of arguments that the function takes as input. ## Synthesizing functions from sampling files To synthesize a function from a sampling file, execute the following command: ``` $ xyntia [-ops ] [-time ] [-heur ] ``` where *grammar* is the abbreviation of the grammar used to define the search space (see below), *heur* is the abbreviation for the search heuristic to be used (see below), *time* is the time budget of the synthesis in seconds, and *file* is the path of the sampling file. The sampling file should be in the format produced by Syntia's random sampling module. The file `examples/samples/example.json` is an example of a sampling file. ## Grammar abbreviations

grammar	abbreviation
Mixed Boolean Arithmetic (MBA)	mba
MBA+Division	expr
MBA+Division+Mod+Shift	full
MBA+Shift	mba_shift
MBA+If then else	mba_ite

## Heuristic abbreviations

heuristic	abbreviation
Iterated Local Search	ils
Hill Climbing	hc
Random Walk	rw
Simulated Annealing	sa
Metropolis-Hastings	mh

# Experiments All datasets and scripts are given to reproduce expriments presented in [1]. Especially, it contains the B1 dataset from the [Syntia](https://github.com/binsec/xyntia/blob/master/https://github.com/RUB-SysSec/syntia) paper [2] (Thank you [Tim Blazytko](https://github.com/binsec/xyntia/blob/master/https://synthesis.to/) for sharing it with us), our B2 dataset and the datasets used to evaluate anti-black-box deobfuscation. ## Python dependencies To facilitate installation, we also give the `requirements.txt` to easily install the python dependencies. To create and activate a python environment, execute the following commands (optional): ``` $ python3 -m venv # create a virtual environment for python3 $ source /bin/activate # active the virtual environment ``` Then, install dependencies: ``` $ pip install -r requirements.txt ``` ## Launch expriments Datasets used in [1] can be found in the `./datasets` directory. To launch Xyntia over a dataset (e.g., B2) with a given timeout (e.g., 1s) execute the following commands: ``` $ python3 ./scripts/bench/sample.py --bench ./datasets/b2 --out $ python3 ./scripts/bench/bench.py --bench ./datasets/b2 --timeout 1 --out ``` The option and their meanings can be found through the `--help` option. # Synthesize all blocks from a execution trace We also give `./scripts/utils/all_from_trace.sh` which traces code execution with GDB, extracts each code block executed, samples and synthesizes them. The manual is available through `./scripts/utils/all_from_trace.sh --help` and it can be run as follows: ``` $ ./scripts/utils/all_from_trace.sh --outdir --all -- binary arg1 arg2 ... ``` Here is an example: ``` $ cd examples/bin && make && cd - $ ./scripts/utils/all_from_trace.sh --outdir --all -- ./examples/bin/add ``` # Synthesize a specific output The previous section explained how to synthesize each output of each basic block. However, you may be interested in only one output of one basic block. We explain how to do it for the `add` function of `./examples/bin/add` and the `eax` output. First, you need to trace the code: ``` $ ./scripts/utils/all_from_trace.sh --outdir --gdb -- ./examples/bin/add ``` Then you need to find the basic block of interest in `/add/cfgs`. In our case, this is the file `/add/cfgs/0x56556191.bin`. Now you can sample the `eax` output and run Xyntia over it: ``` $ python3 ./scripts/utils/binsec/sample.py --bin /add/cfgs/0x56556191.bin --reg_out eax --out 0x56556191_eax $ xyntia 0x56556191_eax/out_0.json ``` # References [1] Menguy, G., Bardin, S., Bonichon, R., & Lima, C. D. S. (2021, November). Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (pp. 2513-2525). [2] Blazytko, T., Contag, M., Aschermann, C., & Holz, T. (2017). Syntia: Synthesizing the semantics of obfuscated code. In 26th USENIX Security Symposium (USENIX Security 17) (pp. 643-659).

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：