Maude-HCSは、現実世界の規模で隠蔽通信システム（HCS）を形式的に仕様化し、推論するための、最初の汎用的かつモジュラーなツールチェーンの一つです。これにより、ネットワーク設計者は代替HCS設計を迅速かつ効果的に探求でき、設計を信頼するために必要な形式的なプライバシーとパフォーマンスの保証を提供します。
隠蔽通信システム（HCS）は、通常のネットワーク活動内に秘密のメッセージを埋め込み、通信の存在を隠します。実際には、HCSの検出不能性は、通常、アドホックなトラフィック統計や特定の検出器を用いて評価されるため、セキュリティの主張は実験設定や暗黙の敵対的仮定に強く結びついています。
Maude-HCSは、複雑なHCS設計における検出不能性とパフォーマンスのトレードオフを推論するための、原則に基づいた実行可能な基盤を提供する実行可能なモデリングおよび解析フレームワークです。設計者は、プロトコルの動作、敵対者の観測可能量、環境の仮定を形式的に指定し、誘導されたトレース分布からモンテカルロサンプルを生成します。これらは、統計的検定の真陽性率と偽陽性率を推定し、これらの推定値を検出不能性尺度の下限に変換することで、検出不能性の主張を監査するために使用できます。これにより、明示的に述べられたモデリング仮定の下で、検出可能性とそのパフォーマンスとのトレードオフを体系的に評価することが可能になります。
HCSのモデリングと推論に関して支援が必要な場合は、お気軽にお問い合わせください。また、研究の一部として本ツールを使用される場合は、引用をご検討ください。```bibtex @article{khoury2026maude, title={Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems}, author={Khoury, Joud and Kim, Minyoung and Merlin, Christophe and Meseguer, Jos{'e} and Ratliff, Zachary and Talcott, Carolyn}, journal={arXiv preprint arXiv:2603.03369}, year={2026} }
## 要件
Python バージョン `3.12.4` が必要です
お好みの環境を作成し、アクティベートしてください。例えば、
pyenv の場合```bash
pyenv install 3.12.4
pyenv local 3.12.4
conda の場合```bash conda create --name pwnd2 python=3.12.4 conda activate pwnd2
仮想環境用```bash
python -m venv venv
source venv/bin/activate
リポジトリのソースコードは、次のように構成されています。 依存関係（サブモジュール）として dns-formalization-maude をインポートします。 この依存関係のフォークを作成して、 それへの変更を追跡できるようにしました。 スパースチェックアウトを使用して、依存関係のソース全体をチェックアウトする必要を回避します。 依存関係には、多くの無関係なファイル（Testbedなど）が含まれています。```shell git clone [email protected]:raytheonbbn/maude-hcs.git
メインブランチには最新（不安定な可能性あり）のソースがあります。
`pwnd.cp1` などの古いブランチ/タグは、評価中に結果を生成するために使用された安定したスナップショットを指します。
（例：`pwnd.cp1` はチャレンジ問題1に使用され、同様に `pwnd.cp2` も同様です。）
古いスナップショットを使用するには、特定のブランチ（例：`pwnd.cp1`）をチェックアウトしてください。
コードのクローンを使用して dns サブモジュールをセットアップし、元のソースへの変更を追跡できるようにします。スパースチェックアウトを使用して関連するソースのみを保持します。```shell
cd maude-hcs
mkdir -p maude_hcs/deps
git submodule add -b <branch> -f [email protected]:raytheonbbn/dns-formalization-maude.git \
maude_hcs/deps/dns_formalization
cd maude_hcs/deps/dns_formalization
git sparse-checkout init --cone
git sparse-checkout set "Maude/dns" "Maude/common" "Maude/test" "Maude/attack_exploration"
cd ../../../
git reset .gitmodules
git reset maude_hcs/deps/dns_formalization
上記のコマンドで、<branch> を pwnd.43.rb1 に設定するとチャレンジ問題1の結果を再現でき、
または pwnd に設定すると最新バージョンを使用できます。
上記の操作により、sparse-checkout という名前の新しいファイルが
.git/modules/maude_hcs/deps/dns_formalization/info/
の下に作成され、Maude/src などの特定のディレクトリのみを含むように指示されます。
この時点で git status はクリーンな状態を示すはずです。
インストールするには、まず依存関係を dns というパッケージとしてインストールし（Maude.* としてインポート）、
次に maude_hcs を（dns に依存する）パッケージとしてインストールします。```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## ユーザーモデルの自動生成
ユーザーモデルは、ユーザーの行動を表現するためのマルコフモデルです。
これらはJSON形式で提供されます。
最初のステップは、これらを正式なMaude表現に変換することです。
そのためには、以下を指定します。
- プロトコル：dns または mastodon
- 変換したいすべてのJSONモデルを含む入力ディレクトリ
- すべてのJSONモデルのMaude版を含む出力ディレクトリ
例として、```shell
# convert dns tgen user models
maude-hcs --verbose \
--protocol=dns markov \
--json-dir=../pwnd-cp2/src/static/tgen_models/dns/ \
--maude-dir=./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
# convert mastodon tgen models
maude-hcs --verbose \
--protocol=mastodon markov \
--json-dir=../pwnd-cp2/src/static/tgen_models/mastodon \
--maude-dir="./maude_hcs/lib/raceboat/maude/mastodonprofiles/"
./maude_hcs/lib/tgen/maude/dnsprofiles/markov/以下にあるマルコフJSON仕様の例（mastodonについても同様）と、それらから変換されたMaude仕様を参照してください。
generateコマンドを使用して初期設定を生成します。
HCS設定は、HCS設定パラメータを使用してJSONで直接渡すか、Shadow実験設定ファイルを使用するか、YML設定ファイルを使用して渡すことができます。それぞれについては以下で説明します。
maude-hcs json設定ファイルを以下のように渡します。
iodineを使用した確率的DNSモデル設定を生成し、出力ファイル名を指定するには、```shell
maude-hcs --verbose generate
--run-args="./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1-hcsconfig.json"
--model=prob
--filename="cp2_scenario_1"
--output-dir="./use-cases/challenge-problem-2/cp2_scenarios/"
`--model=nondet` を設定して、非決定論的バージョンを生成します。
これにより、出力ディレクトリに実行可能な maude ファイル（および対応する HCS 設定 json）が生成されます。
入力 JSON 設定ファイルは、すぐに理解できるはずです。以下の仕様が含まれています。
* ネットワークトポロジ（リンクとその特性）
* 敵対者（この場合、zeek 検出器プロファイル、移動平均検出器のベースラインデータ、およびそれらの設定）
* チャンネル/プロトコル：各プロトコルは、奇妙なネットワークと基礎となるネットワークプロトコルを含みます。前者は後者にデータを隠蔽/埋め込みます。例えば、Iodine は DNS に埋め込みます（そのためチャンネルは iodine-dns と呼ばれます）、Destini は Mastodon に埋め込みます。
一部のパラメータの説明については、[HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/main/HCSParamsGuide.md) を参照してください。
確率的モデルは、非決定論的パラメータと確率的パラメータ（非決定論的パラメータを上書きする）を組み合わせることに注意してください。
### YML 設定の使用
#### 単一設定
YML 設定には、トンネルと基盤ネットワークの完全な設定が含まれています。
これから直接 HCS 設定を生成できます。```shell
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
CP2のようなバッチ構成の場合、複数のYMLファイルをMaudeシナリオファイルに変換します:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
`scenario_dir`はオプションです（デフォルトは`../pwnd_cp2`）
### Shadow yaml設定を使用する
ネットワーク設定は、HCS設定JSONの代わりにshadowファイルを使用して指定できます。
（詳しいshadow仕様については、[Shadow](https://github.com/shadow/shadow)シミュレーターを参照してください）。
shadowファイルで定義された特性を使用するモデルを生成するには、以下を指定します。```shell
--shadow-filename <path_to_shadow_file.yaml>
shadow yaml ファイルは、ネットワーク、ホスト、プロセス構成を指定します。
shadow ネットワーク設定がディレクトリ ../pwnd-cp1 に配置されていると仮定して、実行```shell
maude-hcs --verbose --protocol=dns generate --shadow-filename=../pwnd-cp1/shadow_files/examples/cp1_sim_config.yaml --model=prob --filename=generated_test_shadow
## HCS設定の実行
### Maudeを使ったスタンドアロン実行
スタンドアロンのMaudeで設定を実行するには、まずお使いのシステムに[standalone maude](https://github.com/maude-lang/Maude)をインストールしてください（バージョン3.5.0以下を推奨します）
単一の設定を実行するには、ファイル名を指定してmaudeを起動します。例えば、`results`内で、```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
Maude プロンプト内で、入力します```shell rew initConfig .
これは、ルールが見つからなくなり、進行ができなくなるまで、すべての書き換えを実行します。
ログの追加により、実行の冗長性が増加します```shell
set print attribute on .
実行は以下のコマンドでステップ実行することもできます（maude マニュアルを参照）```shell rew[1] initConfig . cont 1 .
### Statistical Model Checking
統計的モデル検査は、[QMaude](https://github.com/fadoss/umaudemc) の scheck サブコマンドを利用して行えます:```shell
maude-hcs scheck [-h] [--advise]
[--protocol {dns}] [--file FILE] [--test TEST] [--initial INITIAL] [--query QUERY]
[--assign METHOD] [--alpha ALPHA] [--delta DELTA]
[--seed SEED] [--jobs JOBS] [--format {text,json}]