raytheonbbn/maude-hcsFormal modeling and analysis framework for hidden communication systems, enabling specification of covert channels, adversary models, and statistical model checking of undetectability-performance tradeoffs.
Maude-HCS is one of the first generalized and modular toolchains for formally specifying and reasoning about Hidden Communication Systems (HCS) at real-world scales. It enables network designers to explore alternative HCS designs quickly and effectively and provides formal privacy-performance guarantees needed to trust the design.
Hidden communication systems (HCS) embed covert messages within ordinary network activity to hide the presence of communication. In practice, the undetectability of an HCS is typically evaluated using ad hoc traffic statistics or specific detectors, making security claims tightly coupled to experimental setups and implicit adversarial assumptions.
Maude-HCS is an executable modeling and analysis framework that provides a principled and executable foundation for reasoning about undetectability–performance tradeoffs in complex HCS designs. Designers formally specify protocol behavior, adversary observables, and environmental assumptions, and generate Monte Carlo samples from the induced trace distributions. These can be used to audit claims of undetectability by estimating the true and false positive rates of a statistical test and converting these estimates into lower bounds on undetectability measures. This enables systematic evaluation of detectability and its tradeoffs with performance under explicitly stated modeling assumptions.
Please reach out to us if you need assistance modeling and reasoning about your HCS. And please consider citing our work if you use it as part of your research.
@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}
}
Requires python version 3.12.4
Create your preferred environment and activate it, for example
For pyenv
pyenv install 3.12.4
pyenv local 3.12.4
For conda
conda create --name pwnd2 python=3.12.4
conda activate pwnd2
For virtual env
python -m venv venv
source venv/bin/activate
We structured the repo source code so that we import dns-formalization-maude as a dependency (a submodule). We created a fork of this dependency so that we can track our changes to it. We use sparse-checkout to avoid needing to checkout all the source of the dependency which includes many irrelevant files (such as Testbed).
To clone the main repo
git clone [email protected]:raytheonbbn/maude-hcs.git
The main branch has the latest (possibly unstable) source.
Older branches/tags such as pwnd.cp1 refer to stable snapshots used to produce results during evaluations
(e.g., pwnd.cp1 used for challenge problem 1, and similarly pwnd.cp2).
To use an older snapshot, checkout the specific branch (eg pwnd.cp1).
Setup the dns submodule using our clone of the code so we can track changes made to the original source, use sparse-checkout to keep only relevant sources
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
In the command above set <branch> either to pwnd.43.rb1 to reproduce challenge problem 1 results,
or to pwnd for the latest version.
The above should create a new file named sparse-checkout under
.git/modules/maude_hcs/deps/dns_formalization/info/
and tell it to only include certain directories such as Maude/src.
At this point git status should show a clean start.
To install, first install the dependency as a package called dns, we import as Maude.*
then install the maude_hcs as a package (with dependency on dns).
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
User models are markov models intended to represent how users behave. These are given in json format. The first step is to convert these to formal maude representations.
To do so, specify the
For example,
# 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/"
See example markov json specifications under ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
(and similarly for mastodon), along with their converted maude specifications.
We generate initial configurations using the generate command.
HCS Configurations can be directly passed in json using HCS configuration parameters,
or using a Shadow experiment configuration file, or using a YML configuration file.
Each of these is described next.
Pass a maude-hcs json configuration file as follows,
To generate a probabilistic DNS model config with iodine and specify the output filename,
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/"
Set --model=nondet to generate a nondeterministic version.
This produces the executable maude file (and the corresponding HCS config json) in the output directory. The input json configuration file should be straightforward to follow. It includes specification of
Refer to HCSParamsGuide for a description of some of the parameters. Note that probabilistic model will combine the nondeterministic params as well as the probabilistic params (which override the nondeterministic ones).
A YML configuration contains the full config of the tunnels and undelying networks. We can generate an HCS config directly from it.
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
For batched configurations like the ones in CP2, convert multiple YML files to Maude scenario files:
./scripts/generate_cp2_maude.sh [scenario_dir]
Where scenario_dir is optional (defaults to ../pwnd_cp2)
The network configuration can be specified using a shadow file instead of our HCS config json (See Shadow simulator for more info on shadow specifications).