raytheonbbn/maude-hcs
GitHub: raytheonbbn/maude-hcs
基于 Maude 重写逻辑的隐蔽通信系统形式化建模与统计模型检测框架，用于验证不可检测性与性能的权衡。
Stars: 20 | Forks: 7
# Maude-HCS
Maude-HCS 是首批用于在现实世界规模下形式化规范和推理隐藏通信系统 (HCS) 的通用模块化工具链之一。
它使网络设计者能够快速有效地探索不同的 HCS 设计，
并提供信任该设计所需的形式化隐私-性能保证。
## 简介
隐藏通信系统 (HCS) 将隐蔽消息嵌入到普通网络活动中以隐藏通信的存在。
在实践中，HCS 的不可检测性通常使用临时的流量统计或特定的检测器来评估，
这使得安全性声明与实验设置和隐式的对手假设紧密耦合。
Maude-HCS 是一个可执行的建模和分析框架，为推理复杂 HCS 设计中的不可检测性与性能权衡提供了原则性且可执行的基础。
设计者形式化地规范协议行为、对手可观察量和环境假设，并从诱导的迹分布中生成 Monte Carlo 样本。
这些可用于通过估计统计检验的真阳性率和假阳性率，并将这些估计值转换为不可检测性度量的下界，从而审计不可检测性声明。
这使得能够在明确陈述的建模假设下，系统地评估可检测性及其与性能的权衡。
如果您在建模和推理您的 HCS 时需要帮助，请联系我们。
如果您将其用作研究的一部分，请考虑引用我们的工作。
```
@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
```
pyenv install 3.12.4
pyenv local 3.12.4
```
对于 conda
```
conda create --name pwnd2 python=3.12.4
conda activate pwnd2
```
对于 virtual env
```
python -m venv venv
source venv/bin/activate
```
## 安装：从 git 源码
我们构建了 repo 源代码结构，以便我们将 dns-formalization-maude 作为依赖项（一个 submodule）导入。
我们创建了该依赖项的一个 fork，以便我们可以跟踪对此的更改。
我们使用 sparse-checkout 来避免检出依赖项的所有源代码，其中包含许多不相关的文件（例如 Testbed）。
克隆主 repo
```
git clone git@github.com:raytheonbbn/maude-hcs.git
```
主分支包含最新（可能不稳定）的源代码。
较旧的分支/标签（如 `pwnd.cp1`）是指用于在评估期间生成结果的稳定快照
（例如，`pwnd.cp1` 用于挑战问题 1，类似地 `pwnd.cp2`）。
要使用较旧的快照，请检出特定的分支（例如 `pwnd.cp1`）。
使用我们的代码克隆设置 dns submodule，以便我们可以跟踪对原始源代码的更改，使用 sparse-checkout 仅保留相关源代码
```
cd maude-hcs
mkdir -p maude_hcs/deps
git submodule add -b -f git@github.com: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
```
在上面的命令中，将 `` 设置为 `pwnd.cp1` 以重现挑战问题 1 的结果，
或设置为 `pwnd` 以获取最新版本。
上述操作应在 .git/modules/maude_hcs/deps/dns_formalization/info/ 下创建一个名为 sparse-checkout 的新文件，
并指示它仅包含某些目录，例如 `Maude/src`。
此时 `git status` 应显示一个干净的起始状态。
要安装，首先将依赖项安装为名为 dns 的包，我们将其作为 `Maude.*` 导入
然后将 `maude_hcs` 安装为一个包（依赖于 dns）。
```
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
```
## 自动生成用户模型
用户模型是旨在表示用户行为的 markov 模型。
这些以 JSON 格式给出。
第一步是将这些转换为形式化的 Maude 表示。
为此，请指定
- protocol：dns 或 mastodon
- 包含所有要转换的 JSON 模型的输入目录
- 将包含所有 JSON 模型的 Maude 版本的输出目录
例如，
```
# 转换 dns tgen 用户模型
maude-hcs --verbose \
--protocol=dns markov \
--json-dir=../pwnd-cp2/src/static/tgen_models/dns/ \
--maude-dir=./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
# 转换 mastodon tgen 模型
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/` 下的示例 markov JSON 规范
（mastodon 同理），以及它们转换后的 Maude 规范。
## 自动生成 HCS 配置
我们使用 `generate` 命令生成初始配置。
HCS 配置可以使用 HCS 配置参数直接在 JSON 中传递，
或使用 Shadow 实验配置文件，或使用 YML 配置文件。
接下来将分别描述这些内容。
### 使用 HCS JSON 配置
按如下方式传递 Maude-HCS JSON 配置文件，
要使用 iodine 生成概率 DNS 模型配置并指定输出文件名，
```
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 检测器配置文件、用于移动平均检测器的基线数据及其配置）
* channels/protocols：每个协议包含一个 weird network 和一个底层网络协议。前者将数据隐藏/嵌入到后者中。例如，Iodine 嵌入在 DNS 中（因此通道称为 iodine-dns），而 Destini 嵌入在 Mastodon 中
有关某些参数的说明，请参阅 [HCSParamsGuide](./HCSParamsGuide.md)。
请注意，概率模型将结合非确定性参数以及概率参数（后者会覆盖非确定性参数）。
### 使用 YML 配置
#### 单个配置
YML 配置包含隧道和底层网络的完整配置。
我们可以直接从中生成 HCS 配置。
```
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
```
#### CP2 的批量配置
对于像 CP2 中那样的批量配置，将多个 YML 文件转换为 Maude 场景文件：
```
./scripts/generate_cp2_maude.sh [scenario_dir]
```
其中 `scenario_dir` 是可选的（默认为 `../pwnd_cp2`）
### 使用 Shadow YAML 配置
可以使用 Shadow 文件代替我们的 HCS 配置 JSON 来指定网络配置
（有关 Shadow 规范的更多信息，请参阅 [Shadow](https://github.com/shadow/shadow) 模拟器）。
要生成使用 Shadow 文件中定义的特征的模型，请指定：
```
--shadow-filename
```
Shadow YAML 文件指定了网络、主机和进程配置。
假设 Shadow 网络配置位于目录 `../pwnd-cp1` 中，运行
```
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` 中，
```
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
```
在 Maude 提示符内，输入
```
rew initConfig .
```
这将执行所有重写，直到找不到更多规则且无法取得进展。
添加日志记录将通过以下方式增加执行的详细程度
```
set print attribute on .
```
也可以使用以下命令单步执行（请参阅 Maude 手册）
```
rew[1] initConfig .
cont 1 .
```
### 统计模型检测
统计模型检测可通过 [QMaude](https://github.com/fadoss/umaudemc) 中的 scheck 子命令进行：
```
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 运行如下：
```
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 源文件中为模型检测问题指定的 monitor 和 adversary 参与者提取可观察量，该源文件通过 ``--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 公式表示：
```
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 个样本后回答第一个查询。
输出包括：
- mu：样本均值（期望值）
- sigma：样本标准差
- r（置信半径）：给定 alpha 下 mu 周围的误差范围，即置信度为 (1-alpha) 的 mu ± radius
```
step=30 n=30 30 μ=191.13112908653187 8.066666666666666 σ=20.074331354964382 1.048260737942926 r=7.495878519259243 0.391426992470463
step=60 n=60 30 μ=191.73987197380484 8.066666666666666 σ=18.784008301748255 1.048260737942926 r=4.852423885397848 0.391426992470463
step=90 n=90 30 μ=191.0827655561146 8.066666666666666 σ=17.597893935302075 1.048260737942926 r=3.6858075268606814 0.391426992470463
step=120 n=120 30 μ=191.28516943859958 8.066666666666666 σ=16.712118022094398 1.048260737942926 r=3.0208416995911134 0.391426992470463
step=150 n=150 30 μ=191.81314662826944 8.066666666666666 σ=16.539151183097196 1.048260737942926 r=2.6684398888965446 0.391426992470463
step=180 n=180 30 μ=190.8746803932425 8.066666666666666 σ=16.936122821805657 1.048260737942926 r=2.4909903998666914 0.391426992470463
step=210 n=210 30 μ=191.46358580546917 8.066666666666666 σ=16.52110171477275 1.048260737942926 r=2.24749940416632 0.391426992470463
step=240 n=240 30 μ=191.56944900796088 8.066666666666666 σ=16.513730454991496 1.048260737942926 r=2.0998701423425232 0.391426992470463
step=270 n=270 30 μ=191.8095651355114 8.066666666666666 σ=16.62555049424396 1.048260737942926 r=1.9920516750753852 0.391426992470463
Number of simulations = 270
Query 1 (./smc/readme.quatex:5:1)
μ = 191.8095651355114 σ = 16.62555049424396 r = 1.9920516750753852
Query 2 (./smc/readme.quatex:6:1) (30 simulations)
μ = 8.066666666666666 σ = 1.048260737942926 r = 0.391426992470463
```
如果我们将上述 QuaTEx 公式中的阈值修改为 500，则某些样本会被丢弃。
然后会报告结果以及丢弃的样本数量，并使用剩余样本计算统计保证，如下所示。
```
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 时，使用当前时间作为种子。
```
# maude-hcs scheck --seed 0
Number of simulations = 30
μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
# maude-hcs scheck --seed 0
Number of simulations = 30
μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
# maude-hcs scheck --seed 0 -j 4
Number of simulations = 30
μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
# maude-hcs scheck --seed 0 -j 4
Number of simulations = 30
μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
```
### 测试自动化
runexp.sh 是一个结合了生成和 SMC 分析的自动化脚本。它接受两个必需参数：
```
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
SMC 具有高度可并行性，可以使用机器上的所有核心在 Monte Carlo 采样中获得接近线性的加速，如上所述使用 `-j 0` 选项。
QMaude 允许使用分布式 SMC 跨机器实现更高的并行性（该功能仍在积极测试中）
要运行分布式 SMC，应该有一个或多个使用以下命令启动的 worker：
```
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
```
新的 sworker 命令的唯一选项是地址 和端口。它一直等待来自控制器的连接。
在控制器端，可以使用附加选项 --distribute 执行普通的 scheck 命令。例如，
```
$ maude-hcs scheck --distribute workers.json
```
文件 workers.json（也可以是 TOML 或 YAML）指定了用于模拟的 worker 列表。该文件应该是一个字典，包含一个 workers 键，其值为 ``{ "workers": [ {"address": "127.0.0.1", "port": 1234} ] }`` 或简单地 ``{ "workers": [ "127.0.0.1:1234" ] }`` 形式的列表。除此之外，选项和输出应与常规 scheck 命令相同。
scheck 命令将连接到远程 worker，将它们所需的所有信息传递给它们，激活它们，并处理它们的结果，直到达到规定的置信水平。无需手动将文件复制到每台运行 worker 的机器，文件通过连接发送。Maude 包含内容会被解析，并将 Maude 源代码的扁平化版本发送出去。
### 运行 QMaude 进行独立测试
QMaude 提供了相同形式主义下模型的统计模型检测 (SMC)。
将 `latency.quatex` 和 `smc.maude` 复制到您的实验目录（或将其保留在 `results` 中）。
修改前者以加载目标（概率）实验。
运行
```
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
```
QMaude 返回 quatex 查询的期望值 (μ)，以及达到该值所进行的 Monte Carlo 模拟次数。
## 测试
要运行测试，首先在您的环境中安装 pytest。
```
pip install -e .[test]
```
然后运行单元测试
```
python -m pytest
```
## 其他实用工具
要将图像目录转换为实验中使用的 JSON 元数据文件，
例如生成 mastodon tgen 客户端使用的图像（destino 的封面图像同理）
```
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
```
### 跨场景生成 testbed 和 SMC 之间每个 quatex 查询的比较图
使用 `plotfinal.py`，参数为 smc\_directory、tne\_directory、quatex\_directory
```
python scripts/plotfinal.py use-cases/challenge-problem-2/results-aligned/ use-cases/challenge-problem-2/cp2_scenarios_tne/cp2_te_results/ smc/
```
同一脚本将生成 CDF 图。
```
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 直接使用
* [Maude](https://github.com/maude-lang/Maude)
* [QMaude](https://github.com/fadoss/umaudemc)
* 使用 Maude 的 [DNS 协议形式化](https://gitlab.ethz.ch/netsec/dns-formalization-maude)
* [Actors2PMaude tool](https://zenodo.org/records/7071693)
标签：Google搜索, Homebrew安装, IP 地址批量处理, Maude, Python, 信息隐藏, 入侵检测 evasion, 协议设计, 形式化验证, 性能权衡, 无后门, 模型检测, 私有化部署, 科研工具, 统计分析, 网络安全, 网络安全, 网络隐写, 蒙特卡洛模拟, 逆向工具, 防御规避, 隐私保护, 隐私保护, 隐蔽性分析, 隐蔽通信