サイト内の現在位置

LLM+シンボリック実行でバイナリ解析

NECセキュリティブログ

2025年6月13日

NECサイバーセキュリティ技術統括部 セキュリティ技術センターの田中です。

セキュリティ強化や脆弱性分析のために、バイナリ解析は現代のデジタル環境において不可欠な技術となっています。しかしながら、バイナリ解析は長年、高い専門スキルと膨大な経験を持った解析者に強く依存する分野として知られており、バイナリ解析を広く普及させる上で障壁となっています。
今回のブログでは、LLMを活用したバイナリのデコンパイルと、シンボリック実行を組み合わせたバイナリ解析について紹介します。

目次

シンボリック実行エンジンKleeについて

シンボリック実行は、解析対象のプログラムを実行する際、具体的な入力ではなく、象徴的な値や制約を用いてプログラムの内部状態をシミュレートします。
シンボリック実行では、解析対象のバイナリコードを実行する際に、変数や関数の名前などの象徴情報を保持したままプロセスを進めます。この手法により、解析者は逆アセンブル結果をより高水準の抽象度で解釈でき、関数呼び出しの追跡、データのフローの把握、脆弱性発見が容易になります。
Kleeは、シンボリック実行を代表する代表的なツールの1つで、特にソフトウェアの検証や脆弱性発見に用いられますnew window[1]。Kleeで解析するには、追跡したい変数を指定したり検出したい条件分岐の分岐先を指定してコンパイルされたバイナリを入力する必要があります。

インストール方法

Kleeは、dockerイメージとLinuxに導入する2パターンで提供されています。今回は、より導入が簡易なdockerイメージでの導入方法を紹介します。より詳細な解説は、公式ドキュメントnew window[2]を参照してください。

$ docker pull klee/klee:2.0
$ docker run --rm -ti --ulimit='stack=-1:-1' klee/klee:2.0

使い方

Kleeの公式ドキュメントのチュートリアルnew window[3]を参考に解説します。公式リポジトリnew window[4]のsample/get_sign.cを見ると、klee_make_symbolic関数を使用しています。この関数は、第1引数の変数を追跡対象の変数として指定する関数です。

#include "klee/klee.h"

int get_sign(int x) {
  if (x == 0)
     return 0;
  if (x < 0)
     return -1;
  else
     return 1;
}

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}

Kleeのコンテナ上でコンパイル、解析を開始します。

コンパイル:

$ clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c

解析実行:

$ klee get_sign.bc

実行終了すると、klee-out-[通し番号]というディレクトリが作成され、中に検出したテストケースファイルが作成されます。テストケースは、ktest-toolコマンドで表示できます。

$ ktest-tool klee-out-0/test000001.ktest
ktest file : 'klee-out-0/test000001.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x00'
object 0: hex : 0x00000000
object 0: int : 0
object 0: uint: 0
object 0: text: ....

このテストケースは、指定した変数(a)に0を入力するケースを示しています。このほかにも、正の値、負の値を入力するケースも出力されました。

//正の値を入力するケース
$ ktest-tool test000002.ktest
ktest file : 'test000002.ktest'
args       : ['test-sym.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x01\x01\x01\x01'
object 0: hex : 0x01010101
object 0: int : 16843009
object 0: uint: 16843009
object 0: text: ....

//負の値のケース
$ ktest-tool test000003.ktest
ktest file : 'test000003.ktest'
args       : ['test-sym.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

LLM4Decompileについて

LLM4Decompileは、gccのO0からO3までの最適化レベルのLinux x86_64バイナリを、人間が読めるようにデコンパイルすることに特化した大規模言語モデルですnew window[5]。LLMは、テキストで学習するため、バイナリデータを直接処理できません。一度objdumpなどでアセンブリにするか、Ghidranew window[6]などでデコンパイルして入力する必要があります。
2025年現在、1.3b、6.7b、9b、22bのモデルが提供されています。今回は、GPUのないCPU環境で動作させるため、最も軽量な1.3bのモデルを使用します。

インストール方法

LLM4Decompileのgithubリポジトリをクローンし、依存関係をインストールします。

$ git clone https://github.com/albertan017/LLM4Decompile
$ cd LLM4Decompile
$ pip install -r requirements.txt

使い方

今回は、Ghidraでデコンパイルした結果を使用します。LLM4Decompileには、簡単に試すことができるサンプルコードのdemo.pyが含まれています。demo.pyは、C言語のソースコードをコンパイルし、Ghidraでデコンパイルし、デコンパイルコードをLLMに渡します。
実行するには、モデルの設定とGhidraや実行ファイルのパスを適切に設定する必要があります。CPU環境で動作させるため、demo.pyの下記コードからcuda()を削除します。

model = AutoModelForCausalLM.from_pretrained(model_path, torch_dtype=torch.bfloat16).cuda()

下記コマンドで実行します。

$ cd LLM4Decompile/ghidra
$ python demo.py

LLMには、下記プロンプトが渡されます。

# This is the assembly code:
undefined8 func0(float param_1,long param_2,int param_3)
{
  int local_10;
  int local_c;

  local_10 = 0;
  do {
    local_c = local_10;
    if (param_3 <= local_10) {
      return 0;
    }
    while (local_c = local_c + 1, local_c < param_3) {
      if ((float)(DAT_001020d0 &
                 (uint)(*(float *)(param_2 + (long)local_10 * 4) -
                       *(float *)(param_2 + (long)local_c * 4))) < param_1) {
        return 1;
      }
    }
    local_10 = local_10 + 1;
  } while( true );
}# What is the source code?

実行すると、よりC言語のソースコードに近いデコンパイルコードが出力されます。

refined function:
int func0(float *a, int n, float eps)
{
    int i, j;
    for (i = 0; i < n; i++)
    {
        for (j = i + 1; j < n; j++)
        {
            if (fabs(a[i] - a[j]) < eps)
            {
                return 1;
            }
        }
    }
    return 0;
}

satodaNote CTF - Passcode2

今回は、satodaNote CTFのRev問題であるPasscode2をLLM4DecompileとGhidraとKleeを組み合わせて解いてみますnew window[7]。この問題は、標準入力を受け取り、特定の値と一致するとフラグを出力します。

$ ./passcode2
Enter the passcode: aaaaaaaaaaa
Invalid passcode. Nice try.

LLM4Decompile+Ghidraでデコンパイル

今回はバイナリを入力するため、前に使用したdemo.pyのままでは使用できません。バイナリを入力とするコードはAppendix-1に載せていますのでご参照ください。
Passcode2のバイナリは、stripされているため関数名が残っていませんが、Ghidraでデコンパイルすると、entry関数からFUN_00101175がメイン関数であることが分かります。

void processEntry entry(undefined8 param_1,undefined8 param_2){
  undefined1 auStack_8 [8];

  __libc_start_main(FUN_00101175,param_2,&stack0x00000008,FUN_001014b0,FUN_00101510,param_1,auStack_8);
  do {
                    /* WARNING: Do nothing block with infinite loop */
  } while( true );
}

FUN_00101175をデコンパイル対象に設定して実行すると、下記プロンプトがLLMに渡されます。

# This is the assembly code:
undefined8 FUN_00101175(void)

{
 //変数の宣言は省略
  local_124[0] = 0x18;
  local_124[1] = 0x1f;
  local_124[2] = 4;
  local_124[3] = 0x79;
  local_124[4] = 0x4f;
  local_124[5] = 0x5a;
  local_124[6] = 4;
  local_124[7] = 0x18;
  local_124[8] = 0x1a;
  local_124[9] = 0x1b;
  local_124[10] = 0x1e;
  local_124[0xb] = 0;
  printf("Enter the passcode: ");
  iVar1 = __isoc99_scanf("%255[^\n]%*[^\n]",&local_118);
  if (iVar1 == -1) {
    uVar2 = 1;
  }
  else {
    __isoc99_scanf(&DAT_0010202c);
    if ((char)local_118 == '\0') {
      printf("Invalid passcode.");
    }
    else {
      sVar3 = strlen((char *)&local_118);
      if (sVar3 < 0xb) {
        printf("Invalid passcode. Too short.");
      }
      else {
        sVar3 = strlen((char *)&local_118);
        if (sVar3 < 0xc) {
          sVar3 = strlen((char *)&local_118);
          if (sVar3 == 0xb) {
            local_10 = 0;
            while ((sVar3 = strlen((char *)local_124), local_10 < sVar3 &&
                   (*(byte *)((long)&local_118 + local_10) == (local_124[local_10] ^ 0x2a)))) {
              local_10 = local_10 + 1;
            }
            sVar3 = strlen((char *)local_124);
            if (local_10 == sVar3) {
              puts("The passcode has been verified.\n");
              printf("Flag is : flag{%s}",&local_118);
            }
            else {
              printf("Invalid passcode. Nice try.");
            }
          }
          else {
            printf("Invalid passcode.");
          }
        }
        else {
          printf("Invalid passcode. Too long.");
        }
      }
    }
    putchar(10);
    uVar2 = 0;
  }
  return uVar2;
}
# What is the source code?

LLMにより、下記が返ってきます。

int FUN_00101175()
{
    char passcode[256] = {0};
    char key[11] = {0x18, 0x1F, 0x04, 0x79, 0x4F, 0x5A, 0x04, 0x18, 0x1A, 0x1B, 0x1E, 0x00};
    size_t i;

    printf("Enter the passcode: ");
    if (__isoc99_scanf("%255[^\n]%*[^\n]", passcode) == -1)
        return 1;

    __isoc99_scanf("\n");

    if (passcode[0] == '\0')
    {
        printf("Invalid passcode.");
        goto end;
    }

    if (strlen(passcode) < 11)
    {
        printf("Invalid passcode. Too short.");
        goto end;
    }

    if (strlen(passcode) > 12)
    {
        printf("Invalid passcode. Too long.");
        goto end;
    }

    if (strlen(passcode) != 11)
    {
        printf("Invalid passcode.");
        goto end;
    }

    for (i = 0; i < strlen(passcode); i++)
    {
        if (passcode[i] != (key[i] ^ 0x2A))
            break;
    }

    if (i == strlen(key))
    {
        printf("The passcode has been verified.\n\n");
        printf("Flag is : flag{%s}", passcode);
    }
    else
    {
        printf("Invalid passcode. Nice try.");
    }

end:
    printf("\n");
    return 0;
}

だいぶC言語らしくなりましたが、このままではまだコンパイルできません。どうしても復元できない部分やデコンパイル精度不足な部分があるため、汎用LLMに修正させます。今回はGPT-4.1を使用しましたnew window[8]。プロンプトは、上記コードに「このコードをgccコンパイラでコンパイルできるように、インクルードヘッダーの追加等修正してください。」を加えて実行しました。生成されたコードを下記に示します。

#include <stdio.h>
#include <string.h>
#include <stddef.h>

int FUN_00101175()
{
    char passcode[256] = {0};
    char key[12] = {0x18, 0x1F, 0x04, 0x79, 0x4F, 0x5A, 0x04, 0x18, 0x1A, 0x1B, 0x1E, 0x00};
    size_t i;

    printf("Enter the passcode: ");
    if (__isoc99_scanf("%255[^\n]%*[^\n]", passcode) != 1)
        return 1;

    __isoc99_scanf("%*c");

    if (passcode[0] == '\0')
    {
        printf("Invalid passcode.");
        goto end;
    }

    if (strlen(passcode) < 11)
    {
        printf("Invalid passcode. Too short.");
        goto end;
    }

    if (strlen(passcode) > 12)
    {
        printf("Invalid passcode. Too long.");
        goto end;
    }

    if (strlen(passcode) != 11)
    {
        printf("Invalid passcode.");
        goto end;
    }

    for (i = 0; i < strlen(passcode); i++)
    {
        if ((unsigned char)passcode[i] != ((unsigned char)key[i] ^ 0x2A))
            break;
    }

    if (i == 11)
    {
        printf("The passcode has been verified.\n\n");
        printf("Flag is : flag{%s}", passcode);
    }
    else
    {
        printf("Invalid passcode. Nice try.");
    }

end:
    printf("\n");
    return 0;
}

int main(void) {
    return FUN_00101175();
}

下記が汎用LLMによる主な修正点です。

  1. インクルードヘッダーを追加
    (ア) <stdio.h>: printf, scanf 用
    (イ) <string.h>: strlen 用
    (ウ) <stddef.h>: size_t 用
  2. メイン関数を追加
  3. scanfの書式指定子を修正

次に、Kleeで実行するために、下記を設定します。

  1. 外部入力を受け取る変数のpasscodeをKleeの追跡対象に設定。
  2. passcodeに格納されるデータを、11文字の記号英数字として設定。
  3. フラグを出力する処理を含むパスを、検出したい処理として設定。

修正したコードを下記に示します。

#include <stdio.h>
#include <string.h>
#include <stddef.h>
#include <klee/klee.h>

int FUN_00101175()
{
    char passcode[256] = {0};
    char key[12] = {0x18, 0x1F, 0x04, 0x79, 0x4F, 0x5A, 0x04, 0x18, 0x1A, 0x1B, 0x1E, 0x00};
    size_t i;

    printf("Enter the passcode: ");

    // if (__isoc99_scanf("%255[^\n]%*[^\n]", passcode) != 1)
    //     return 1;
    klee_make_symbolic(passcode, 256, "passcode");
    for(i=0; i<11; i++){
        klee_assume(passcode[i]>=0x21); klee_assume(passcode[i]<=0x7e);
    }

    // __isoc99_scanf("%*c");

    if (passcode[0] == '\0')
    {
        printf("Invalid passcode.");
        goto end;
    }

    if (strlen(passcode) < 11)
    {
        printf("Invalid passcode. Too short.");
        goto end;
    }

    if (strlen(passcode) > 12)
    {
        printf("Invalid passcode. Too long.");
        goto end;
    }

    if (strlen(passcode) != 11)
    {
        printf("Invalid passcode.");
        goto end;
    }

    for (i = 0; i < strlen(passcode); i++)
    {
        if ((unsigned char)passcode[i] != ((unsigned char)key[i] ^ 0x2A))
            break;
    }

    if (i == 11)
    {
        printf("The passcode has been verified.\n\n");
        printf("Flag is : flag{%s}", passcode);
        klee_assert(0);
    }
    else
    {
        printf("Invalid passcode. Nice try.");
    }

end:
    printf("\n");
    return 0;
}

int main(void) {
    return FUN_00101175();
}

Kleeでシンボリック実行

Kleeコンテナ上でコンパイルします。klee_assert関数で警告が出ますが無視して問題ありません。

$ clang -I klee_src/include -emit-llvm -c -g passcode2.c

Kleeを実行します。

$ klee --libc=uclibc --posix-runtime passcode2.bc
KLEE: NOTE: Using POSIX model: /tmp/klee_build130stp_z3/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: NOTE: Using klee-uclibc : /tmp/klee_build130stp_z3/runtime/lib/klee-uclibc.bca
KLEE: output directory is "/home/klee/klee-out-0"
(snip)
Invalid passcode. Too long.
Invalid passcode. Too long.

KLEE: done: total instructions = 344486
KLEE: done: completed paths = 255
KLEE: done: partially completed paths = 2
KLEE: done: generated tests = 257

出力された結果のディレクトリを確認すると、拡張子が”.assert.err”のファイルがあります。このファイル名の番号が、フラグを出力する処理を含むパスに到達したテストケースの番号です。同じ番号の”.ktest”ファイルを見ると、”25.Sep.2014”を入力するとフラグを出力する処理に到達できることが分かります。

$ ktest-tool test000033.ktest
ktest file : 'test000033.ktest'
args       : ['passcode2.bc']
num objects: 1
object 0: name: 'passcode'
object 0: size: 256
object 0: data: b'25.Sep.2014\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
object 0: hex : 0x32352e5365702e323031340000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
object 0: text: 25.Sep.2014.....................................................................................................................................................................................................................................................

実際にpasscode2を実行してパスコードを入力するとフラグが取れました。

$ ./passcode2
Enter the passcode: 25.Sep.2014
The passcode has been verified.

Flag is : flag{25.Sep.2014}

まとめ

本ブログではLLMを利用し、C言語に近い形式でのデコンパイルとシンボリック実行を組み合わせてCTFのReversing問題を解きました。LLMを利用することでほぼ再コンパイル可能な形でデコンパイルできました。一方で、一部そのままでは再コンパイルできない点があり、修正をさらにGPTなどの汎用LLMに任せることで再コンパイル可能になりました。今回は、CPU環境という制約上小さいモデルを使用しましたが、より大きなモデルを使用することでさらに高精度に自動でデコンパイルできると考えます。これにより、従来の高度なスキルが要求されるバイナリ解析の簡易化ができると考えます。

Appendix-1

今回作成した、バイナリからGhidraでデコンパイルし、LLM4DecompileでよりC言語に近い形に変換するコードです。

import os
import tempfile
import subprocess
import torch
from transformers import AutoTokenizer, AutoModelForCausalLM

# 設定関連
GHIDRA_HEADLESS_PATH = "../../ghidra_11.3.2_PUBLIC/support/analyzeHeadless"
GHIDRA_POST_SCRIPT = "./decompile.py"
GHIDRA_PROJECT_NAME = "tmp_ghidra_proj"
BINARY_FILE_NAME = "passcode2"
BINARY_EXECUTABLE_PATH = "../../blog/passcode2"
DECOMPILE_TARGET_FUNCTION = "FUN_00101175"
MODEL_PATH = 'LLM4Binary/llm4decompile-1.3b-v2'
PROMPT_FILE_SUFFIX = '.pseudo'
MAX_NEW_TOKENS = 2048


def extract_function_c_code(c_source_code: str, function_name: str):
    """
    指定された関数部分のみCコードから抽出し、関係ないヘッダー等を除去する
    """
    function_lines = []
    function_found = False
    for line in c_source_code.splitlines():
        if f"Function: {function_name}" in line:
            function_found = True
            function_lines.append(line)
            continue
        if function_found:
            # 次の関数定義まででストップ
            if '// Function:' in line and len(function_lines) > 1:
                break
            function_lines.append(line)

    if not function_found:
        raise ValueError(f'関数が見つかりません: {function_name}')

    # 関数ヘッダー重複部分の除去
    for idx in range(1, len(function_lines)):
        if function_name in function_lines[idx]:
            function_lines = function_lines[idx:]
            break

    return '\n'.join(function_lines).strip()


def run_ghidra_decompile(temp_dir: str, output_c_path: str) -> None:
    """
    Ghidraのheadless analyzerで指定バイナリをデコンパイルする
    """
    ghidra_command = [
        GHIDRA_HEADLESS_PATH,
        temp_dir,
        GHIDRA_PROJECT_NAME,
        "-import", BINARY_EXECUTABLE_PATH,
        "-postScript", GHIDRA_POST_SCRIPT, output_c_path,
        "-deleteProject"
    ]
    subprocess.run(ghidra_command, text=True, capture_output=True, check=True)


def main():
    with tempfile.TemporaryDirectory() as temp_dir:
        pid = os.getpid()
        output_c_file = os.path.join(temp_dir, f"{pid}_.c")

        # Ghidraでバイナリをデコンパイル
        run_ghidra_decompile(temp_dir, output_c_file)

        # 結果Cファイル読み出し
        with open(output_c_file, "r") as c_file:
            decompiled_c = c_file.read()

        # 指定関数のみ抽出
        target_c_code = extract_function_c_code(decompiled_c, DECOMPILE_TARGET_FUNCTION)

        # プロンプト作成
        prompt_header = "# This is the assembly code:\n"
        prompt_footer = "\n# What is the source code?\n"
        model_prompt = prompt_header + target_c_code + prompt_footer

        # .pseudoファイル保存
        prompt_file_path = BINARY_FILE_NAME + PROMPT_FILE_SUFFIX
        with open(prompt_file_path, "w", encoding="utf-8") as prompt_file:
            prompt_file.write(model_prompt)

    # モデルロード
    tokenizer = AutoTokenizer.from_pretrained(MODEL_PATH)
    model = AutoModelForCausalLM.from_pretrained(MODEL_PATH, torch_dtype=torch.bfloat16)

    # デコンパイル結果読込、トークン化
    with open(prompt_file_path, "r") as prompt_file:
        prompt_content = prompt_file.read()
    input_tokens = tokenizer(prompt_content, return_tensors="pt").to(model.device)

    # デコンパイル内容をLLMによりCに変換
    with torch.no_grad():
        output_tokens = model.generate(**input_tokens, max_new_tokens=MAX_NEW_TOKENS)
    output_c_func = tokenizer.decode(output_tokens[0][len(input_tokens['input_ids'][0]):-1])

    # 結果出力
    print(f'Refined function:\n{output_c_func}')


if __name__ == "__main__":
    main()

参考文献

執筆者プロフィール

田中 大樹(たなか だいき)
担当領域:リスクハンティング
専門分野:ペネトレーションテスト、脆弱性診断、ソフトウェア検査

ソフトウェアの不正機能検査システムの研究開発業務を経て、現在はペネトレーションテスト、脆弱性診断、ソフトウェア検査などに従事。
CISSP Associate

執筆者の他の記事を読む

アクセスランキング