silab-nitkc/hibari-gas

An experimental obfuscator for software protection using the SMT-based code generation

hibari

hibari is an experimental obfuscator for the assembly language, which aims to protect software against Man-at-the-end attacks. Hibari takes an assembly program (in the GNU assembler format) as input, and returns an obfuscated assembly program as output. In hibari, some code fragments included in the target program are replaced with obscure fragments, preserving their semantics. The obscure fragments are generated using an SMT solver Z3.

Requirements

• Python 3.9 (or higher)
• z3py
• lark-python

Usage

usage: obfuscator.py [-h] [-o O] [-n N] [-l L] src

positional arguments:
  src         Path of input file.

optional arguments:
  -h, --help  show this help message and exit
  -o O        Path of output file.
  -n N        Maximum number of lines to obfuscate at once.
  -l L        Number of instructions used for obfuscation.

Example

python3.9 obfuscator.py target.s -o out.s

Reference

光本智洋，神崎雄一郎，“SMTソルバによる命令列生成を用いたアセンブリプログラムの難読化，” 情報処理学会 第83回全国大会講演論文集 (講演番号2K-04)，2021年3月．

hibari-gas's Issues

GASとSMTの処理を分離する

libs/GAS/とlibs/SMT/の処理を完全に独立させる．

• libs/GAS/で入出力例を生成し，libs/SMT/に渡して命令列を生成
• libs/SMT/で命令列を生成し，libs/GAS/に渡して実行可能コードを生成

色付け処理のリファクタリング

ターミナルのエスケープシーケンスをライブラリ化して分離する

難読化の前後でゼロフラグの値が保証されない

addl $3, %eax
jz hoge

のaddlが難読化されて

addl $3, %eax
subl $3, R0+1*8(%rip)

jz hoge

などとなってしまうケースが発生していた．
（上の例では%eaxの値に基づいていたはずのゼロフラグが，R0+1*8の値で更新されてしまう）