本研究では，プログラムに含まれる演算の表現を，SMTソルバを用いて難読化する方法について検討する．提案方法は，アセンブリのレベルにおいて，演算命令（例えばADD命令）を，命令の意味を保ったまま複雑な表現を持つコード（命令の組み合わせ）に変換することで，演算の表現を不明瞭にする．変換対象となる命令と同じ意味を持つコードは，変換対象となる命令の処理内容や変換後のコードを構成する候補となる命令群の振舞いに関する条件をSMTソルバに与えることで生成する．提案方法に基づいて難読化されたプログラムについて，シンボリック実行を用いた解析に要する時間などを用いた評価を行い，提案方法の有効性を議論する．