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/HEAD/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}]
options:
--help, -h Show help message and exit
--advise Do not suppress debug messages from Maude
--protocol PR The protocol module being analyzed e.g., dns, which points to an smc file specific to that protocol.
--file FILE Maude source file specifying the model-checking problem. If --protocol is specified, this parameter becomes optional, and if specified overrides the protocol smc file.
--test TEST Test generated from maude-hcs, default=results/generated_test.maude
--initial INITIAL Initial term, default=initConfig
--query QUERY QuaTEx query, default=smc/query.quatex
--assign METHOD Assign probabilities to the successors according to the given method, default=pmaude
--alpha ALPHA, -a ALPHA Required significance level for the confidence interval, default=0.05
--delta DELTA, -d DELTA Maximum admissible radius for the confidence interval around the mean, default=0.5
--seed SEED, -s SEED Random seed
--jobs JOBS, -j JOBS Number of parallel simulation threads, default=1, -j 0 will start as many jobs as CPU units
--format {text,json} Output format for the simulation results, default=text
--distribute WORKERS Distribute the computation across multiple machines, specified as a list of workers for the simulation.
--dump OUTPUTFILE Dump query evaluations into the given file. Currently, it only works with the sequential version (-j 1).
For each simulation, a line is written with the result of all queries separated by space.
-D D Define a constant to be used in QuaTEx expressions.
上記のコマンドで生成されたファイルのSMC実行例は以下の通りです：```shell maude-hcs scheck --test ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude --query ./smc/cp2_eval_cp2_scenario_1.quatex -j 0 -n 30-120
確率的モデルとその初期設定は、Maudeで指定し、``--test TEST`` オプション（デフォルト: ``results/generated_test.maude``）を介して提供する必要があります。
Maudeの実行は、``--initail INITIAL`` オプション（デフォルト: ``TEST`` で指定された ``initConfig``）を介して提供された初期項から開始し、最終構成まで書き換えます。
最終構成から、オブザーバブルは、モデル検査問題用のMaudeソースファイル（``--file FILE`` オプションで提供）または ``--protocol PR`` オプションで指定されたモニターと敵対者アクターを使用して抽出されます。
例えば ``--protocol dns`` は、`lib/` の下でdnsプロトコル専用に作成されたモデル検査ファイルを参照します。
平均レイテンシの期待値などの量的特性は、QuaTEx式を使用して指定し、``--query QUERY`` オプション（デフォルト: ``smc/query.quatex``）を介して提供できます。
流出ファイルの観点でのレイテンシおよびスケーラビリティ指標の例は、``smc/latency.quatex`` および ``smc/scalability_cp2_scenario_1.quatex`` で定義され、``smc/cp2_eval_cp2_scenario_1.quatex`` にインポートされ、次の形式のQuaTEx式で表現できます。```shell
Latency() = s.rval("getLatency(getMonitor(C))");
eval E[Latency()] with delta = 2;
ExfilFilesC2() =
if (s.rval("getToDCumulativeNQueryPostNAT(C,416)") == 0.0) then
discard
else
s.rval("getExfilFiles(getMonitor(C), getToDCumulativeNQueryPostNAT(C,416))")
fi;
eval E[ExfilFilesC2()];
式 Latency() は、モニターからレイテンシ値を抽出し、delta = 2 でその期待値を評価します。
式 ExfilFilesC2() は、流出したファイルの数を条件付きで評価します。
NAT後のDNSクエリの累積数に基づく検出時間がゼロの場合（つまり、累積クエリ数がしきい値（上記の例では416など）を超えないために検出が発生しないことを意味します）、サンプルは破棄されます。それ以外の場合は、検出時点までの流出ファイル数が評価されます。
サンプリングは、指定されたサンプル数（すなわち、-n min-max オプション、例：-n 30-300）に達するか、すべてのクエリが所望の統計的有意性で回答されるまで続行されます。
以下の例では、2番目のクエリはデフォルト値のalpha=0.05およびdelta=0.5を使用して30サンプル後に回答され、一方、1番目のクエリは上記で指定された with delta = 2 を使用して270サンプル後に回答されます。
出力には以下が含まれます：
上記のQuaTExの式のしきい値を500に変更すると、一部のサンプルが破棄されます。
結果は破棄されたサンプル数とともに報告され、統計的保証は以下のように残りのサンプルを使用して計算されます。```shell
Number of simulations = 270
Query 1 (./smc/readme.quatex:7:1)
μ = 191.80187664851906 σ = 16.429217228790975 r = 1.9685272804723886
Query 2 (./smc/readme.quatex:8:1) (39 simulations)
μ = 9.76923076923077 σ = 0.48458003855418535 r = 0.1570826767676969
where 21 executions out of 60 (35.0%) have been discarded
同じ並列化設定（つまり、-j の同じ値）で同じ実験を再現するには、同じ乱数シードを指定して --seed オプションを使用します。デフォルトまたは ‑1 を渡すと、現在時刻がシードとして使用されます。```shell
Number of simulations = 30 μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
Number of simulations = 30 μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
Number of simulations = 30 μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
Number of simulations = 30 μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
### テスト自動化
runexp.shは、生成とSMC分析を組み合わせた自動化スクリプトです。必須の引数を2つ取ります:```shell
runexp.sh CONFIG_FILENAME METRIC
where
CONFIG_FILENAME is the name of the .yaml shadow file defining the experiment
METRIC is the quatex property and can be latency, throughput, goodput, or all
SMCは、マシン上のすべてのコアを使用して高度に並列化可能であり、前述の-j 0オプションを使用することでモンテカルロサンプリングにおいてほぼ線形の速度向上が得られます。
QMaudeは、分散SMCを使用することでマシン間でのさらに高い並列性を可能にします（この機能は現在も活発にテスト中です）。
分散SMCを実行するには、以下のようにして1つ以上のワーカーを起動する必要があります。
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
新しいsworkerコマンドの唯一のオプションは、アドレス（-a）とポート（-p）です。コントローラからの接続を待機し続けます。
コントローラ側では、通常のscheckコマンドに追加オプション--distribute <file>を付けて実行できます。例えば、
$ maude-hcs scheck --distribute workers.json
workers.jsonファイル（TOMLまたはYAMLも可能）は、シミュレーションのワーカーリストを指定します。このファイルは、workersキーを持つ辞書で、その値は{ "workers": [ {"address": "127.0.0.1", "port": 1234} ] }という形式のリスト、または単に{ "workers": [ "127.0.0.1:1234" ] }という形式でなければなりません。それ以外の点では、オプションと出力は通常のscheckコマンドと同じです。
scheckコマンドはリモートワーカーに接続し、必要な情報をすべて渡してアクティベートし、規定の信頼水準に達するまで結果を処理します。ワーカーが動作する各マシンに手動でファイルをコピーする代わりに、ファイルは接続を通じて送信されます。Maudeのインクルードは解決され、フラット化されたバージョンのMaudeソースが送信されます。
QMaudeは、同一形式のモデルに対する統計的モデル検査（SMC）を提供します。
latency.quatexとsmc.maudeを実験ディレクトリにコピーしてください（resultsにそのままでも構いません）。
前者を修正して、対象の（確率的）実験を読み込ませてください。
実行```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
QMaudeは、quatexクエリ(μ)の期待値を返し、その値に達するまでに要したモンテカルロシミュレーションの回数を返します。
## テスト
テストを実行するには、まず環境にpytestをインストールしてください。```
pip install -e .[test]
次に、単体テストを実行します。``` python -m pytest
## その他のユーティリティ
実験で使用するjsonメタデータファイルに画像のディレクトリを変換するには、
例えば、mastodon tgenクライアントで使用される画像を生成する場合（同様にdestiniのカバー画像）```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
plotfinal.py を引数 smc_directory, tne_directory, quatex_directory とともに使用します。```shell
python scripts/plotfinal.py use-cases/challenge-problem-2/results-aligned/ use-cases/challenge-problem-2/cp2_scenarios_tne/cp2_te_results/ smc/
同じスクリプトがCDFプロットを生成します。```shell
python scripts/gather\_samples.py use-cases/challenge-problem-2/results-aligned/samples/ use-cases/challenge-problem-2/results-aligned/cdfs use-cases/challenge-problem-2/cp2_scenarios_tne/cp2_te_results/
以下のプロジェクトはMaude-HCSで直接使用されています。