Maude-HCS

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

安装：从 git 源码

我们构建了仓库源码结构，以便将 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 规范。

自动生成 HCS 配置

我们使用 generate 命令生成初始配置。 HCS 配置可以直接通过 HCS 配置参数的 JSON 传入，或者使用 Shadow 实验配置文件，或者使用 YML 配置文件。接下来将分别描述这些方法。

使用 HCS JSON 配置

按如下方式传入 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/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 的批量配置

对于类似 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/`` 下。

maude-hcs

最受欢迎

Maude-HCS

引言

安装：从 git 源码

自动生成 HCS 配置

使用 HCS JSON 配置

CP2 的批量配置