使用後解放バグ（use-after-free bugs）は、メモリ破壊の一種であり、静的解析で検出するのが難しい。 この投稿では、Binary NinjaのMLILを使用して、メモリ割り当ての相互作用を追跡するデータフロー グラフを作成する方法を探索する。 グラフは、メモリ領域をノードとして、ポインタの保存をエッジとして表現し、追跡された割り当て、スタックフレーム、動的メモリ、グローバルメモリノードを使用する。 SSA変数はノードにマッピングされ、オフセットはポインタ演算を表すために保存される。 メモリの保存と読み込み操作は、関数のスコープ外の読み込みについては事前に初期化されていると仮定して、グラフのエッジを作成する。 情報は、SSA変数の割り当てとポインタ演算時のオフセット計算に基づいてグラフを通じて伝播する。 引数にマッピングがあるか、スタックオフセットが特定の条件を満たす場合、関数呼び出しは分析され、無限ループを防ぐために再帰が管理される。 グラフの生成後、追跡された割り当てノードに依存する命令はログに記録される。 この分析により、コンテキスト非依存の到達可能性を通じて、潜在的なUAF脆弱性を特定することができる。 このアプローチは、静的解析における固有の分類エラーを認識しているが、他の脆弱性に対する適応可能なプリミティブを強調している。