h5i-dev/h5i

h5i – エージェントネイティブ Web セキュリティワークスペース

概要

• コマンドラインのワークスペースで、AI エージェント を使用して Web アプリの脆弱性を探し、Rust の Web サービスを形式検証することができます。
• 主な 2 つのモードがあります：
  1. レッドチーム（バグ発見） – エージェントがヘッドレスブラウザを操作し、HTTP トラフィックをキャプチャ/変更し、サイトをクロールし、CI/CD でリプレイできます。
  2. 形式検証 – h5i-app Rust フレームワーク（Axum ベース）でアプリを書き、Aeneas を介して Lean 4 にコードを変換し、認可やデータ分離などの特性を証明します。

主要コンポーネント

コンポーネント	役割
h5i CLI	エージェント（ブラウザ、websec、recon、app コマンド）の統一インターフェース。
ブラウザツールキット	ナビゲーション、クリック、フォーム入力などを自動化。
HTTP ツールキット	リクエストをキャプチャ、変更、リプレイし、回帰テストに役立ちます。
Recon クローラー	クローリングと JS 解析により、隠れたエンドポイントやパラメータを発見します。
h5i-app crate	Lean 4 に変換可能なように設計された Axum ベースの Rust フレームワーク。
ダッシュボード（h5i ui）	エージェントセッション、トラフィック、サンドボックスの状態を表示するローカル Web UI。

典型的なワークフロー

1. インストール – ワンライナースクリプトでバイナリとオプションプラグイン（websec、recon、test）を追加します。
2. レッドチーム – 例：

   h5i browser open https://example.com
   h5i browser click @e3
   h5i websec requests            # キャプチャしたトラフィックを表示
   h5i websec replay req_42 --set query.id=456
   h5i recon crawl --max-requests 200
   

   エージェントは設定可能な FS/ネットワーク制限を持つサンドボックス内で実行でき、記録されたフローは CI パイプラインで保存およびリプレイできます。
3. 検証可能なアプリを構築 – 例：

   h5i app new counter && cd counter   # 新しいプロジェクトをスキャフォールド
   h5i app extract                     # Rust コードを Lean 4 に変換
   h5i app prove                       # Lean 証明チェッカーを実行
   h5i app mutate                      # コードを変異させて証明の破綻を確認
   

   Rust crate は依存関係（h5i-app = "0.1.1"）として追加され、HTTP や Postgres などの機能をサポートします。
4. 監視 – h5i ui でローカル UI を起動し、ブラウザセッションとリプレイログを確認します。

重要性

• AI 駆動のセキュリティテスト（迅速なエージェント制御の探索）と 形式手法（数学的保証）を橋渡しし、Web セキュリティツール領域ではまれな組み合わせです。
• エージェント側を軽量（CLI コマンド）に保ちながら、証明可能な安全なサービス向けの Rust ファーストの開発パスを提供します。

はじめに

• 提供されているスクリプトまたは cargo install --path . でインストールします。
• エージェントランタイム用にバイナリを スキル として追加します（npx skills add h5i-dev/h5i）。
• 完全なコマンドリファレンスは MANUAL.md または man h5i を参照してください。

ライセンス – Apache-2.0。

---

すべての詳細は、リポジトリの README から直接取得しています。