HALへようこそ！

HAL [/hel/]は、包括的なネットリストリバースエンジニアリングおよび操作フレームワークです。

はじめに
ビルド手順
クイックスタートガイド
学術的な文脈

はじめに

HALって一体何？

事実上、利用可能なネットリスト解析の研究はすべて、検査対象のネットリストをグラフベースで表現したものを基に動作しています。 HALはまさにそれを提供します。すなわち、FPGAやASICなど任意のソースからのネットリストをグラフベースのネットリスト表現にパースし、含まれるゲートやネットのトラバーサルおよび解析に必要なビルトインツールを提供するフレームワークです。

私たちのビジョンは、HALがIDAやGhidraのようなツールのハードウェアリバースエンジニアリング版になることです。 HALが研究者やアナリストにとって共通のベースラインとなり、研究結果の再現性を向上させ、ネットリストパースのような反復的な基本タスクを抽象化することを目指しています。

高いパフォーマンス – 最適化されたC++コアによる
柔軟性 – 組み込みのPythonバインディングによる
モジュール性 – C++プラグインシステムによる
安定性 – 豊富なテストスイートで保証

HALは、マックス・プランク・セキュリティ・プライバシー研究所の組み込みセキュリティグループによって活発に開発されています。複数の研究プロジェクトに加え、ルール大学ボーフム（RUB）の大学講義「ハードウェアリバースエンジニアリング入門」でも使用されています。

また、ネットリストリバースエンジニアリング技術の評価のためのモダンな最先端ベンチマーク回路セットを別のリポジトリで提供していることに注意してください。

同梱プラグイン

このリポジトリには、厳選されたプラグインが含まれています：

GUI: 視覚的なネットリスト検査とインタラクティブな解析を可能にする高機能GUI
- HAL PythonバインディングにアクセスできるPythonシェルのネイティブ統合
- 特定のゲートやモジュールを分離してクリーンな検査を実現
- ネットリストのインタラクティブなトラバーサル
- 検査中のネットリストのあらゆる側面に関する情報を提供する詳細なウィジェット
Netlist Simulator: ロードされたネットリストの任意の部分のシミュレータ
Dataflow Analysis: 非構造化ネットリストから高レベルレジスタを復元するデータフロー解析プラグインDANA
Graph Algorithms: igraphとの統合により、グラフ理論の一般的なアルゴリズムへの直接アクセスを提供
Python Shell: HAL PythonバインディングをプリロードしたPythonシェルを起動するコマンドラインプラグイン
VHDL & Verilog パーサ: ネットリスト入力形式としてVHDLおよびVerilogファイルのパースをサポート
Liberty パーサ: 標準のlibertyゲートライブラリ形式の任意のゲートライブラリをサポート
VHDL & Verilog ライター: （変更された）ネットリストを合成可能なVHDLまたはVerilogファイルにシリアライズする機能を提供
Gate Libraries: XILINX UnisimおよびSimprimゲートライブラリをサポート

ドキュメント

HALの機能に関するユーザー視点の包括的なドキュメントは、Wikiで入手できます。さらに、完全なC++ APIおよびPython APIのドキュメントも提供しています。

ビルド手順

HALのビルド手順については、Wikiの専用ページを参照してください。

クイックスタートガイド

HALをインストールまたはビルドし、hal -gでGUIを起動します。すべての利用可能なオプションはhal [--help|-h]で一覧表示できます。 examplesサブディレクトリにいくつかのサンプルプロジェクトを同梱しています。サンプルプロジェクトを始めるには、メインメニューからImport Projectを選択するか、ウェルカム画面のOPEN PROJECTエリアにzipファイルをドロップしてインポートします。これにより、書き込み権限のあるディレクトリを要求するポップアップが表示され、そこにHALがプロジェクトディレクトリを作成してファイルを解凍します。次回プロジェクトを開くときにネットリストとゲートライブラリが見つかるように調整が行われるため、外部ツールで解凍しないでください。

独自のVerilogまたはVHDLネットリストを開きたい場合は、代わりにImport Netlistを実行してください。これは、plugins/gate_libraries/definitionsに一致するゲートライブラリがある場合、または手動でゲートライブラリを提供した場合にのみ機能します。独自のゲートライブラリを作成する手順やその他の便利なチュートリアルについては、wikiを参照してください。

以下のサンプルコードは、fsmサンプルに関するものです。

統合されたPythonシェルまたはPythonスクリプトウィンドウを使用して対話操作を行います。どちらも（制限付きの）オートコンプリート機能を備えています。

すべてのルックアップテーブルをリストし、そのブール関数を表示してみましょう：

for gate in netlist.get_gates():
    if "LUT" in gate.type.name:
        print("{} (id {}, type {})".format(gate.name, gate.id, gate.type.name))
        print("  {}-to-{} LUT".format(len(gate.type.input_pins), len(gate.type.output_pins)))
        boolean_functions = gate.boolean_functions
        for name in boolean_functions:
            print("  {}: {}".format(name, boolean_functions[name]))
        print("")

サンプルネットリストfsm.vhdでは、次のように出力されます：

FSM_sequential_STATE_REG_0_i_3_inst (id 4, type LUT6)
  6-to-1 LUT
  O: (!I1 & !I2 & I3 & !I4 & I5) | (I0 & !I2) | (I0 & I1) | (I0 & I3) | (I0 & I4) | (I0 & I5)

FSM_sequential_STATE_REG_0_i_2_inst (id 3, type LUT6)
  6-to-1 LUT
  O: (I2 & I3 & I4 & !I5) | (I1 & !I5) | (I1 & !I4) | (I1 & !I3) | (I0 & I1) | (I1 & I2)

FSM_sequential_STATE_REG_1_i_3_inst (id 6, type LUT6)
  6-to-1 LUT
  O: (!I1 & I4 & !I5) | (!I1 & !I3 & I4) | (I0 & I4 & !I5) | (I0 & !I3 & I4) | (!I1 & I2 & I4) | (I0 & I2 & I4) | (!I2 & !I5) | (!I2 & !I4) | (!I2 & !I3) | (!I0 & !I4) | (!I0 & !I2) | (!I0 & !I1) | (I1 & !I4) | (I1 & !I2) | (I0 & I1) | (I3 & !I5) | (I3 & !I4) | (!I0 & I3) | (I1 & I3) | (I2 & I3) | (!I4 & I5) | (!I3 & I5) | (!I0 & I5) | (I1 & I5) | (I2 & I5)

FSM_sequential_STATE_REG_1_i_2_inst (id 5, type LUT6)
  6-to-1 LUT
  O: (!I0 & I1 & !I2 & I3 & I4 & !I5) | (I0 & !I2 & I3 & I4 & I5)

OUTPUT_BUF_0_inst_i_1_inst (id 18, type LUT1)
  1-to-1 LUT
  O: !I0

OUTPUT_BUF_1_inst_i_1_inst (id 20, type LUT2)
  2-to-1 LUT
  O: (I0 & !I1) | (!I0 & I1)

コントリビューション

HALの開発への貢献を歓迎します。GitHub経由で新しいプルリクエストを自由に提出してください。その前に、静的チェックとclang formatを実行することを検討してください。これらのチェックをコミット前にgitフックとしてインストールすることもできます。

静的チェックとclang formatをローカルで実行

clang-formatフックをインストールするには、git-hooksをインストールし、次を実行します：

git hooks --install

Dockerビルドを開始するには： docker-compose run --rm hal-build

チェンジログの生成

git log $(git describe --tags --abbrev=0)..HEAD --pretty=format:"%s" --no-merges

学術的な文脈

学術的な文脈でHALを使用する場合は、以下の参考文献を使用してフレームワークを引用してください：

@misc{hal,
    author = {{Embedded Security Group}},
    publisher = {{Max Planck Institute for Security and Privacy}},
    title = {{HAL - The Hardware Analyzer}},
    year = {2019},
    howpublished = {\url{https://github.com/emsec/hal}},
}

元の論文を含めていただいても構いません。ただし、HALは論文で説明された元のプロトタイプから大幅に変更されていることに注意してください。したがって、上記のエントリを引用することを推奨します。

@article{2018:Fyrbiak:HAL,
    author = {Marc Fyrbiak and Sebastian Wallat and Pawel Swierczynski and Max Hoffmann and Sebastian Hoppach and Matthias Wilhelm and Tobias Weidlich and Russell Tessier and Christof Paar},
    title = {{HAL-} The Missing Piece of the Puzzle for Hardware Reverse Engineering, Trojan Detection and Insertion},
    journal = {IEEE Transactions on Dependable and Secure Computing},
    year = {2018},
    publisher = {IEEE},
    howpublished = {\url{https://github.com/emsec/hal}}
}

HALで解決しようとしている課題の概要については、36C3でのトークをご覧ください。

ライセンス

HALは、他の研究グループとの協力や産業界からの貢献を促進するためにMITライセンスで提供されています。詳細については、ライセンスファイルを参照してください。

免責事項

HALは最高でもアルファ品質のソフトウェアです。自己責任で使用してください。本ツールキットの悪意のある使用を推奨するものではありません。

hal

人気