SMTソルバによる命令列生成を用いたアセンブリプログラムの難読化

摘要

プログラムコードの解析技術の発展にともない，ソフトウェアに対するMan-At-The-End 攻撃（エンドユーザによる実行可能コードの解析・改ざh行為）の手段が多様になっている．特に近年では，シンボリック実行による自動解析を用いた攻撃が報告されており[1]，その攻撃に対する保護方法が求められる．本研究では，このような自動解析を用いた攻撃からソフトウェアを保護する一方法として，SMT (Satisfiability ModuloTheories) ソルバによる自動的な命令列生成を用いたプログラムの難読化方法を提案する．提案方法は，アセンブリプログラムに含まれる特定の命令を，その命令と同様の意味を持つ複雑な命令列（2 つ以上の命令の組合せ）で置き換えることで，プログラムを難読化する．複雑な命令列の生成は，置換対象となる命令の入出力例などを制約としてSMT ソルバに与えることで行う．