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 作为依赖（子模块）导入。 我们创建了该依赖的一个分支，以便跟踪对其所做的更改。 我们使用 sparse-checkout 来避免检出依赖的所有源码，其中包含许多无关文件（例如 Testbed）。
要克隆主仓库```shell git clone [email protected]:raytheonbbn/maude-hcs.git
主分支包含最新（可能不稳定）的源代码。
旧的分支/标签如 `pwnd.cp1` 指的是用于评估期间产生结果的稳定快照（例如，`pwnd.cp1` 用于挑战问题1，同理 `pwnd.cp2`）。
要使用旧的快照，请切换到特定分支（例如 `pwnd.cp1`）。
使用我们克隆的代码设置 dns 子模块，以便跟踪对原始源代码所做的更改，使用 sparse-checkout 仅保留相关源文件。```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 以获取最新版本。
上述操作应在路径
.git/modules/maude_hcs/deps/dns_formalization/info/
下创建一个名为 sparse-checkout 的新文件，
并指示它仅包含某些目录，例如 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 表示形式。
为此，请指定
- protocol: 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 检测器配置文件、移动平均检测器的基线数据及其配置）
* 通道/协议：每个协议包含一个 weird 网络和一个底层网络协议。前者将数据隐藏/嵌入到后者中。例如，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 配置
网络配置可以使用 shadow 文件指定，而不是我们的 HCS 配置 JSON
（有关 shadow 规范的更多信息，请参阅 [Shadow](https://github.com/shadow/shadow) 模拟器）。
要生成使用 shadow 文件中定义的特征的模型，请指定：```shell
--shadow-filename <path_to_shadow_file.yaml>
影子 yaml 文件指定了网络、主机和进程配置。
假设影子网络配置文件位于目录 ../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中运行配置，请首先为您的系统安装[独立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 manual）```shell rew[1] initConfig . cont 1 .
### 统计模型检验
通过[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`` 指代一个专门为 dns 协议创建的模型检查文件，位于 ``lib/`` 下。
定量属性（如平均延迟的期望值）可通过 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）或所有查询均以所需的统计显著性得到回答。
在下面的示例中，第二个查询在使用默认值 alpha=0.05 和 delta=0.5 的情况下，经过 30 个样本后得到回答，而第一个查询在使用如上指定的 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
### Test automation
runexp.sh 是一个结合了生成与SMC分析的自动化脚本。它需要两个必需参数：```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，应启动一个或多个工作节点，命令如下：
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
新的 sworker 命令的唯一选项是地址 (-a) 和端口 (-p)。它会持续等待来自控制器的连接。
在控制器端，可以执行普通的 scheck 命令，并附加选项 --distribute 。例如：
$ 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 查询的期望值 (μ)，以及达到该值所需的蒙特卡洛模拟次数。
## Tests
要运行测试，请先在您的环境中安装 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 所使用：