トリトン対花王のおもちゃプロジェクト。 良い伝統を続ける

この記事では、SMTソルバーについて説明します。 そのため、このトピックに関する研究資料に良い伝統が登場しました。 すでに何度か、さまざまな研究者がSMTソルバーの亀裂と同じ例を選択しました 。これは、ニックネームkaoの人が発明した亀裂です。 さて、この伝統を続けて、記号計算用の別のツールであるTritonを使用して亀裂を解決してみましょう。

SMTソルバーに関する一言

理論の公式の充足可能性の問題（英語の充足可能性モジュロ理論、SMT）は、それらの基礎となる理論を考慮した論理式の充足可能性の問題です。 このようなSMT式の理論の例は次のとおりです。整数と実数の理論、リストの理論、配列、ビットベクトルなど- ウィキペディア

SMTタスクは、SATタスクの延長です（ブール充足可能性問題または命題充足可能性問題。英語文学ではSATISFIABILITYまたはSAT、ロシア文学ではVypと呼ばれることもあります）。

ウィキペディアからの別の引用：

SATタスクのインスタンスは、変数名、角かっこ、AND、OR、HE演算のみで構成されるブール式です。 タスクは次のとおりです。式で発生するすべての変数に値「false」および「true」を割り当てて、式がtrueになるようにすることは可能ですか。 - ウィキペディア

SMTソルバーはさまざまな理論で機能するため、従来のプロセッサアーキテクチャのアルゴリズムにそれらを使用することが可能になります。 したがって、SMTソルバーは2つの問題を解決できます。

• アルゴリズムの特定の出力値が特定の入力値で可能かどうかという質問に答えます。
• アルゴリズムの結果に出力値が与えられる入力値を決定します。

SMTソルバーは、科学技術のさまざまな分野で応用されています。 Z3 、 miniSAT 、 CVC4などのSMT式を解くための個別のツール、およびBAP 、 radare2またはangrなどのSMT式の構文で機械語でアルゴリズムを表すための個別のツールがあります 。 ツールは絶えず改善されており、APIはより強力になり、数回クリックするだけでリバースエンジニアリングの問題でSMT数学装置全体を使用できます。

また、シンボリックパフォーマンスにはいくつかのタイプがあることに注意してください。 静的シンボリック実行（SSE）は、シンボリック変数のみに基づいており、シンボリック式のみを使用します。 動的シンボリック実行（DSE）（コンコリック実行とも呼ばれます）は、プログラム実行中に数値変数の特定の値とともにシンボリック計算を使用します。 このホワイトペーパーでは、静的文字の実行のみを使用します。

花王のトイプロジェクトクラックストーリー

クラック花王のトイプロジェクトは非常にシンプルです。 1つのウィンドウに、特定の16進数のシーケンスが表示され、このシーケンスに有効なキーの入力が求められます。

彼の物語は、次の年代記の形で表現できます。

2012年3月4日- 花王のおもちゃプロジェクトと代数暗号解読 -dcoder、andrewl-代数暗号解読、SAT

このクラック専用の最初の作品は2012年に登場しました。 その中で、ニックネームdcoderを持っている人が代数暗号解読を使用してソリューションを公開し、この作業の共同著者andrewlがSATソルバーを正常に適用しました。

03/06/2012- シンボリック実行による半自動入力クラフティング、自動キージェネレーター生成へのアプリケーション -Rolf Rolles-z3、レコーダー

その後、有名な研究者であるロルフ・ロールズは、最初にSMTソルバーをソリューションに適用しました。 まず、Z3で数式を手動で作成し、次にOCamlでマシンコードの中間表現から数式を自動的に生成するツールを提示しました。 彼が使用した中間言語は自分で開発しました。

BitBlazeとBAPで使用されているものと非常によく似たIRを使用していますが、VEXを使用するのではなく、独自のIRトランスレーターを作成しました。 私の実装は最初から書かれており、オープンソースのフレームワークとコードを共有しません。 -openrce.org

11.2013- ソフトウェアセキュリティ用のSMTソルバー -Georgy Nosenko-BAP、z3

その後、同僚のジョージ・ノセンコの研究が始まりました。そこでは、BAPフレームワークと同じZ3ソルバーが既に式の生成に使用されていました。

2015.2015- OpenREILおよびZ3を使用した自動代数暗号解析 -Cr4sh-OpenREIL、z3

Cr4shとしても知られるDmitry Oleksyukは、彼の研究で、中間言語OpenREILへの変換と、その後のZ3での式の生成を使用しました。

04.2016- シンボリック実行とangrによる花王のおもちゃプロジェクトの解決-Extreme Codersブログ-angr

そして最後に、2016年に別の作品が登場し、angrフレームワークを使用したソリューションについて説明しています。 Angrは、シンボリック実行にVEX中間言語とclaripyライブラリを使用します。

別のプレイヤーがSMTアリーナに登場しました-Triton。この作品では、有名なクラックを解決するためにそれを使用します。

トリトン

TritonはQuarkslabによって作成されました。Quarkslabは 、リバースエンジニアリングのための多くの興味深いツールを作成しました。

まず、Tritonの仕組みについて少し説明します。 彼の仕事の過程で、彼は次のアクションを実行します。

1. バイナリコードの実行パスを解析し、機械語命令のすべての副作用を考慮した抽象構文コードツリーを生成します。
2. 抽象構文ツリーをバイパスして、SMT-LIB形式のSMT式を生成します。
3. ソルバーz3を使用して数式を解きます。

抽象構文ツリーを構築する場合、Tritonは（bapやangrとは異なり）マシンコードの中間表現を使用せず、現在はx86およびx86-64アーキテクチャでの作業のみをサポートしています。

Tritonは2つのモードのいずれかで動作します。 最初のオンラインモード-実行トレースは、Tritonの一部であり、 ピンDBIフレームワークを使用する特別なトレーサーを使用して記録されます 。 2番目-オフラインモード-トラックは外部手段によって記録されます。 ルートには、一連の命令とそのオペコードが含まれている必要があります。 2番目のケースでは、初期コンテキストを独立して作成する必要があります。つまり、レジスタと使用メモリの値を決定します。

Tritonが提供するAPIは非常に豊富で、非常に不安定です。 APIの登場以来、後方互換性を維持することなく、もちろん4回変更されています。 このため、Tritonを使用する古いツールのコードは、新しいバージョンで実行するように書き直す必要があります。 良い点は、APIにPythonのバインディングがあることです。 リポジトリには、C ++およびPythonでのAPIの使用方法を示すいくつかの例があり、それらを理解するのは非常に簡単です。

それでは、解決策に取り掛かりましょう。

解決策

まず、入力されたキーをチェックするアルゴリズムを見つける必要があります。 コードをざっと見てみると、生成されたシーケンスは実際には8つの32ビット整数であり、リトルエンディアンビューではメモリ内に連続して存在し、ウィンドウではビッグエンディアンとして表示されています。 キーの形式がXXXXXXXX-XXXXXXXXであることがわかります。Xは16進数です。 キーがこの形式で入力された場合、検証手順が呼び出されます。 これは、IDA Pro逆アセンブラーの外観です。

検証手順では、入力が最初に初期化されます：cipherはリトルエンディアンビューの32バイトのソースシーケンス、String1は変換後の出力シーケンスのバッファー、edxおよびebxレジスターは32ビット整数として表されるキーの半分です。 次に、変換アルゴリズム自体（xorおよびrol操作を使用した32サイクル）が続き、String1バッファーからの結果の文字列が文字列「0how4zdy81jpe5xfu92kar6cgiq3lst7」と比較されます。 それらが同一である場合、キーは有効と見なされます。

したがって、次のタスクがSMTソルバーに対して生成されます。アルゴリズムが実行された後、edxおよびebxレジスタのどの入力値が特定の16進数シーケンスを登録するかを文字列「0how4zdy81jpe5xfu92kar6cgiq3lst7」に変換します。

クラックのあるWindows用に作成されているため、TritonトレーサーはLinux用にコンパイルされているため動作しません。 もちろん、Windows用に自分でコンパイルすることもできますが、これらはまだ冒険です。 したがって、PythonにはオフラインモードとTritonバインディングを使用します。

まず、必要な定数を紹介します。

ADDR_CIPHER = 0x4093A8 ADDR_TEXT = 0x409185 ADDR_EBP = 0x18f980 TEXT = "0how4zdy81jpe5xfu92kar6cgiq3lst7" cipher = None
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

そして、初期化を実行します。

 ctx = TritonContext() ctx.setArchitecture(ARCH.X86) ctx.setConcreteRegisterValue(ctx.registers.ebp, ADDR_EBP) ctx.setConcreteRegisterValue(ctx.registers.esp, 0x18f95b) ctx.setConcreteRegisterValue(ctx.registers.eip, 0x4010ec) ctx.setConcreteMemoryAreaValue(ADDR_CIPHER, cipher) ctx.setConcreteMemoryAreaValue(ADDR_TEXT, list(map(ord, TEXT))) edx = ctx.convertRegisterToSymbolicVariable(ctx.getRegister(REG.X86.EDX)) ebx = ctx.convertRegisterToSymbolicVariable(ctx.getRegister(REG.X86.EBX)) keys = [ctx.convertMemoryToSymbolicVariable(MemoryAccess(ADDR_EBP-0x21, 1)) for i in xrange(32)]
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

初期化中に、コンテキストを作成し、アーキテクチャを確立し、レジスタとメモリを初期化し、もちろんシンボル変数を作成します：edxとebxのレジスタ、および変換されたシーケンスのバッファ。式の制限により値が課されます。

次に、実行トレースを作成します。 オフラインモードでこれを行うには、バイナリコードをダウンロードするだけです。

 code = {0x4010EC: '\x55', # push ebp 0x4010ED: '\x8b\xec', # mov ebp, esp 0x4010EF: '\x83\xc4\xdc', # add esp, -24h 0x4010F2: '\xb9\x20\x00\x00\x00', # mov ecx, 20h 0x4010F7: '\xbe\xa8\x93\x40\x00', # mov esi, offset cipher 0x4010FC: '\x8d\x7d\xdf', # lea edi, [ebp+string1] 0x4010FF: '\x8b\x55\x08', # mov edx, [ebp+arg_0] 0x401102: '\x8b\x5d\x0c', # mov ebx, [ebp+arg_4] # loc_401105: 0x401105: '\xac', # lodsb 0x401106: '\x2a\xc3', # sub al, bl 0x401108: '\x32\xc2', # xor al, dl 0x40110A: '\xaa', # stosb 0x40110B: '\xd1\xc2', # rol edx, 1 0x40110D: '\xd1\xc3', # rol ebx, 1 0x40110F: '\xe2\xf4'} # loop loc_401105
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

命令の処理を開始します。

 ip = 0x4010ec while ip < 0x401111: inst = Instruction() inst.setOpcode(code[ip]) inst.setAddress(ip) ctx.processing(inst) ip = ctx.buildSymbolicRegister(ctx.registers.eip).evaluate()
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

命令の処理中に、Tritonはそれらを記号形式に変換し、受け取った記号命令をコンテキストに追加します。 このコードでは、ipレジスタのシンボリックエミュレーションを使用して、実行順に次の命令を計算します。

この後、変数の値に必要な制限をコンテキストに導入することが残っています。 TEXT定数に配置した文字列「0how4zdy81jpe5xfu92kar6cgiq3lst7」と変換された文字列が等しいかどうかについて、この条件があります。

 for i in xrange(32): r_ast = ast.bv(ord(TEXT[i]), 8) l_id = ctx.getSymbolicMemoryId(ADDR_EBP-0x21 + i) l_ast = ctx.getAstFromId(l_id) ex = ast.equal(l_ast, r_ast) expr.append(ex) expr = ast.land(expr)
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

制約は、抽象構文ツリー（ASD）のノードの形式で設定されます。 ループでは、文字列の1文字のASDノードと、変換されたシーケンスの1つの要素のASDノードが作成されます。 次に、これら2つのノードを比較する操作を含む新しいASDノードが作成されます。 すべての要素の等価条件は同時に満たされる必要があるため、サイクルでそれらを受け取った後、論理AND演算expr = ast.land（expr）の下で1つのASDに結合されます。

すべてが解を計算する準備ができています。 指定されたexpr制約を持つシンボリック式のデータモデルを取得します。

 model = ctx.getModel(expr)
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

keygenスクリプト全体は、ここから完全にダウンロードできます 。

スクリプトを実行すると...何も起こりません。 デバッグは、命令の処理段階で実行ループが発生することを示しており、ループ命令が処理されていないことがすぐに明らかになります。 トリトンはこの命令さえ知らないことが判明した 。 この問題に対処する方法は？ 新しい命令のセマンティクスをTritonソースに追加して再構築できます。 しかし、Windowsでの再構築はかなり骨の折れる作業であると既に述べました。 うーん、すぐに動揺することはありません。コードをやり直してください。 ループを実際の動作と同じ命令セットで置き換えてみてください。例：

 dec ecx jz 0401105h
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

そして、手動でループを展開して、内部にループのあるブロックではなく、ecxレジスタに書き込まれているループ本体（32）だけを処理することができます。コードは次のようになります。

 code = ['\xac', # lodsb '\x2a\xc3', # sub al, bl '\x32\xc2', # xor al, dl '\xaa', # stosb '\xd1\xc2', # rol edx, 1 '\xd1\xc3'] # rol ebx, 1 ctx.setConcreteRegisterValue(ctx.registers.esi, ADDR_CIPHER) ctx.setConcreteRegisterValue(ctx.registers.edi, ADDR_EBP - 0x21) ctx.setConcreteRegisterValue(ctx.registers.eip, 0x401105) ctx.setConcreteMemoryAreaValue(ADDR_CIPHER, cipher) ctx.setConcreteMemoryAreaValue(ADDR_TEXT, list(map(ord, TEXT))) edx = ctx.convertRegisterToSymbolicVariable(ctx.registers.edx) ebx = ctx.convertRegisterToSymbolicVariable(ctx.registers.ebx) ip = 0x401105 for i in xrange(32): for c in code: inst = Instruction() inst.setOpcode(c) inst.setAddress(ip) ctx.processing(inst) ip = ctx.buildSymbolicRegister(ctx.registers.eip).evaluate()
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

そこで、新しいオプションを起動します。 今回は、処理が完全に実行され、予想どおり、しばらくの間、モデルの計算に成功します。 私たちは待っています...待っています...私たちは非常に長い間待っていました。 待たなかった。 今回は、問題はモデルを計算する機能であり、ここでエラーを検出するのはそれほど簡単ではないかもしれません。 結果の式は非常に大きく、その計算には非常に長い時間がかかると想定できます。 これを確認するために、処理が行われるループの反復回数を減らします。 実際、反復回数が少ないと、結果が出力されます。 選択方法を使用すると、実験用ラップトップで計算に見える時間がかかる反復回数の上限は12であることがわかりました。はい、非常に小さく、その増加に伴い、時間が指数関数的に増加します。 32回の反復は12をはるかに超えており、C ++でコードを書き換えたとしても、とにかく、モデルの計算は許容できないほど長くなるようです。

getModel関数で非常に時間がかかるデバッグを調べようとすると、これらはtriton::ast::TritonToZ3Ast::convert



関数の再帰呼び出しであることがtriton::ast::TritonToZ3Ast::convert



ます。

ドキュメントに書かれているように、TritonはカスタムASDツリーを使用します。

抽象構文木（AST）は、文法を木として表現したものです。 Tritonは、式にカスタムASTを使用します。 すべての式は実行時に構築されるため、ASTは各プログラムポイントで使用できます。 -Tritonドキュメント

この関数は、TritonのADSをz3の式に変換します。

TritonのASDを構成する表現を見てみることができます。 モデルを取得する前に、次の行を追加します。

 tsym = ctx.getSymbolicExpressions() for ek in sorted(tsym.keys()): e = tsym[ek].getAst() print str(e)
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

その後、次のTriton式がコンソールに表示されます。

 ref!0 = SymVar_0 ref!1 = SymVar_1 ref!2 = SymVar_33 ; Byte reference ref!3 = (concat ((_ extract 31 8) (_ bv0 32)) (_ bv29 8)) ; LODSB operation ref!4 = (ite (= (_ bv0 1) (_ bv0 1)) (bvadd (_ bv4232104 32) (_ bv1 32)) (bvsub (_ bv4232104 32) (_ bv1 32))) ; Index operation ref!5 = (_ bv4198662 32) ; Program Counter ref!6 = (concat ((_ extract 31 8) ref!3) (bvsub ((_ extract 7 0) ref!3) ((_ extract 7 0) ref!1))) ; SUB operation ref!7 = (ite (= (_ bv16 8) (bvand (_ bv16 8) (bvxor ((_ extract 7 …
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

SMT-LIB構文の式を取得するには、別の呼び出しを追加する必要があります。

 print ctx.unrollAst(e)
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

この場所unrollAst



、Tritonの式からSMT-LIB式への同じ変換が行われますが、ここでもgetModel関数のように完了を待つことはありません。

SMT-LIB構文に精通している人は、Tritonの式がSSA（単一静的割り当て）の形式のみのSMT-LIB式であることに気付くでしょう。 SMT-LIBには変数の割り当て操作はありません-機能的なlet演算子に置き換えられます。 しかし、ASDをデプロイせずにTritonの構文をSMT-LIB構文に独立して変換し、SSAフォームをletステートメントに置き換えてからz3pyにフィードしようとするとどうなりますか？ かなり面倒で冗長に聞こえますが、開発者がTritonを完成させるまでこの状況から抜け出す必要があります。

したがって、結果の式を使用して、次のアクションを実行します。

• SMT-LIB構文で変数を宣言します。
• 割り当て演算子をletステートメントに置き換えます。
• 結果の式は、SMT-LIB言語で共通の式に結合されます。

結果は、Triton構文からSMT-LIB構文への変換関数です。 もちろん、それは普遍的ではありませんが、少なくとも私たちの仕事には役立ちます。

 def convert(ctx, asserts): zsym = "" tsym = ctx.getSymbolicExpressions() for ek in sorted(tsym.keys()): e = tsym[ek].getAst() if e.getKind() == AST_NODE.VARIABLE: zsym += "(declare-fun ref!%d () (_ BitVec %d))\n" % (ek, e.getBitvectorSize()) nodes = [] for ek in sorted(tsym.keys()): e = tsym[ek].getAst() if e.getKind() <> AST_NODE.VARIABLE: nodes.append("let ((ref!%d %s))" % (ek, e)) # print reduce(lambda x, y: "%s (%s)" % (x, y), reversed(nodes)) def fold(x, y): if not isinstance(y, list): raise TypeError if len(y) == 1: return y[0] return "%s\n(%s)" % (x, fold(y[0], y[1:])) nodes = ["assert"] + nodes nodes[-1] += '\n' + str(asserts) zsym = zsym + '(' + fold(nodes[0], nodes[1:]) + ')' return zsym
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

関数の結果は、計算のためにz3pyソルバーに送信する必要があります。

 s = z3.Solver() cs = z3.parse_smt2_string(expr) s.assert_exprs(cs) s.check() m = s.model() edx, ebx = m.decls()
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

現在、edxおよびebx変数には、 z3.z3.FuncDeclRef



クラスのオブジェクトがz3.z3.FuncDeclRef



ます。 それらの数値表現を取得し、亀裂内の変換は互いにけんかした後に実行されるため、それらをけんかさせる必要もあります。

 edx, ebx = m[edx].as_long(), m[ebx].as_long() print "%x-%x" % (edx, edx ^ ebx)
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

2番目のバージョンのコードはgithubから取得することもできます。

そのため、亀裂のあるウィンドウの入力フィールドにコピーするだけの行が得られます。 手のかゆみはすでにそれをしています。

やった！ keygenは正常に動作しています。

ポンセ

Tritonに基づいて、IDA ProのPonceプラグインという別のクールなツールが構築されます。 IDA逆アセンブラーでのシンボリック実行と汚染分析を直接行うことで、非常に魅力的なことができます。 残念ながら、クラック内にループ命令が存在するため、Ponceをチェックできません。 たぶん、Tritonにループを追加したい人がまだいるでしょうか？ :)または、別のオプションがあります。 kao crackedにはアセンブラのソースコードが付属しているため、ループを前述の同様の命令セットに置き換えることができます。 その後、Ponceを使用してその力を感じることが判明します。 興味のある読者にとって、これはクールなタスクになります。

結論

率直に言って、トリトンはタスクに対処しませんでした。 ただし、厳密になりすぎないようにしましょう。ループステートメントは簡単に追加できます。また、アセンブリの履歴から判断すると、開発者は既に反復処理を開始しています 。

最新のリバースエンジニアリングと、シンボリック実行を伴わないソフトウェアの脆弱性の検索は過去のものです。 これは、たとえば、DARPAサイバーグランドチャレンジ中に作成された自動脆弱性検索およびエクスプロイト生成システムによって証明されます。 そのため、Tritonなどのツールは現在大きな需要があります。 それらが発展するにつれて、それらはますます使いやすくなり、その結果、象徴的なパフォーマンスは研究者の仕事において非常に手頃で効果的なツールになります。