不正な解析攻撃からソフトウェアを保護する方法として，SMTソルバによるアセンブリ命令列の生成方法を応用したプログラム難読化法について検討する．提案方法は，アセンブリプログラムに含まれる特定の命令（例えば演算命令やデータ転送命令）を，その命令と同様の意味を持つ不明瞭な命令列で置き換えることで，プログラムを難読化する．不明瞭な命令列の生成は，置換対象となる命令の入出力例や，生成される命令列を構成する命令の挙動に関する情報を制約としてSMTソルバに与えることで行う．提案方法によって難読化を行うツールを試作し，難読化されたプログラムの実行結果の正しさやシンボリック実行解析への耐性を実験を通して確認する．