z3_and_angr_binary_analysis_workshop

Z3およびAngrを使用したバイナリ分析の紹介

もともとSamecon and Hack.lu 2018でSam Brownによって配信されたこれは、バイナリ分析のためにZ3とANGRを使用する参加者を紹介する3時間のワークショップでした。このワークショップは、SMTソルバー、Z3 SMTソルバーとそのPythonライブラリとAngrg binary Analysisフレームワークの紹介を提供しました。

セキュリティ研究者がリバースエンジニアリングと脆弱性の研究を実施するのを支援するために、テクノロジーの潜在的なアプリケーションを実証することを目的としたワークショップエクササイズが提供されました。

スライドは、コンテンツとエクササイズを試すための順序の大まかなガイドを提供します。

例と運動

Z3

名前	タイプ	説明
n女王	例	「n女王をNXNチェスボードの上に置いて、2人がお互いに攻撃しないようにすることができますか？」 Z3を使用して、n * nチェスボードのソリューションを生成します
ハックベント15	例	解決策とZ3でハックベント15 CTFチャレンジを解くために歩いてください
数独	エクササイズ	Z3を使用してSudokuを解決してみてください
RNG	エクササイズ	オプションのエクササイズ - Z3を使用して非暗号化された乱数発電機シード値を見つける
x86	50/50	半分の例、ハーフDIY- Z3を使用してX86命令の同様のバージョンを実装する
不透明な述語	エクササイズ	以前に実装された指示を使用して、アセンブリの指示の小さなシーケンスで不透明な述語を識別します
同等のチェック	例	以前に実装された命令を使用して、一連の命令シーケンスを識別します

angr

名前	タイプ	説明
Opaque_predicates	例	ANGRを使用して、作業がはるかに少ない不透明な述語を識別します:)
ioctls	例	Angrを使用してWindows Driver IOCTLコードを識別します
こんにちは世界	50/50	Angrを使用して、単純な「ライセンスキーバリーター」の有効な引数を生成するための運動とウォークスルー
爆弾ラボ	エクササイズ	「爆弾ラボ」を解決するためにangrを使用したDIYエクササイズ

設定

すべてのコードはPython3であるため、Angrgrivary分析フレームワークをインストールする必要があります。

 mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr