Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems

1. Problem Statement

Hidden Communication Systems (HCS) embed covert messages within ordinary network traffic to conceal the existence of communication, a capability critical for journalists and military operations in adversarial environments. However, evaluating the security of HCS designs currently faces significant challenges:

• Lack of Formal Frameworks: Existing evaluations rely on ad-hoc traffic statistics, specific detectors, or informal testbed experiments. These methods are rigid, error-prone, and tightly coupled to specific experimental setups, making it difficult to generalize security claims.
• Tradeoff Complexity: HCS designers must balance performance (throughput, latency) against undetectability (risk of detection). Without a formal model, exploring the design space to find optimal configurations is inefficient.
• Absence of Quantitative Guarantees: There is no principled way to formally verify that an HCS design meets specific undetectability thresholds (e.g., "the KL divergence between normal and covert traffic is below $d$") under varying network conditions and adversary capabilities.

2. Methodology

The authors introduce Maude-HCS, an executable modeling and analysis framework based on Rewriting Logic and Statistical Model Checking (SMC).

A. Formal Definition of Undetectability

The paper formalizes undetectability not as a binary property, but as a quantitative condition based on the statistical indistinguishability of observable execution traces.

• Two Worlds: The system is modeled in two states: an Ordinary World (baseline protocol without hidden traffic) and an HCS World (protocol carrying covert traffic).
• Trace Distributions: An adversary observes a sequence of events (packet sizes, timings, directions). These observations induce probability distributions over traces, denoted as $P_t$ (Ordinary) and $Q_t$ (HCS).
• Divergence Metric: Undetectability is defined as a bound on a divergence measure (e.g., Kullback-Leibler (KL) Divergence) between $P_t$ and $Q_t$.
  • $(M, d)$-Undetectability holds if $M(Q_t, P_t) \leq d$ for all adversary strategies.
  • A low KL divergence implies the adversary cannot reliably distinguish the two worlds, limiting their information gain.

B. The Maude-HCS Framework

The toolchain leverages Maude (a high-performance rewriting logic language) and PMaude (probabilistic extension) to create executable models.

1. Modular Modeling: Designers specify the underlying network and protocols as Generalized Actor Rewrite Theories.
2. Weird Network Transformation: A formal pattern transformation converts the baseline network $N$ into a "weird network" $W(N, \vec{p})$ that embeds hidden communication (e.g., tunneling) without altering the original protocol's logic.
3. Probabilistic Execution: Non-deterministic models are transformed into probabilistic models using the $P$-transformation (assigning probability distributions to rules) and $Sim$-transformation (enabling Monte Carlo simulation). This ensures the Absence of Nondeterminism (AND) property required for SMC.
4. Statistical Model Checking (SMC): Using QMaude and QuaTeX (a quantitative probabilistic temporal logic), the framework runs Monte Carlo simulations to estimate:
   • Performance: Latency, goodput, throughput.
   • Detectability: True Positive Rate (TPR) and False Positive Rate (FPR) of specific adversary detectors.

C. Auditing Methodology

Since estimating full trace distributions is computationally infeasible, Maude-HCS audits undetectability via adversarial tests:

1. Sampling: The system generates Monte Carlo samples of traces for both Ordinary and HCS worlds.
2. Detector Evaluation: A specific detector $\phi$ (e.g., a threshold on DNS query counts) is applied to these traces to estimate TPR and FPR.
3. Lower Bound Calculation: Using the Data Processing Inequality, the framework computes a certified lower bound on the KL divergence:
   $$D_{KL}(Q_t \| P_t) \geq D_{KL}(\text{Bern}(TPR) \| \text{Bern}(FPR))$$
   If the calculated lower bound exceeds a claimed privacy parameter $d$, the undetectability claim is falsified under the given assumptions.

3. Key Contributions

1. Formalization of Undetectability: The first formal definition of HCS undetectability as a quantitative bound on the divergence of observable trace distributions, explicitly linking it to adversary information gain.
2. Executable Framework (Maude-HCS): A scalable toolchain that allows designers to specify complex, timed, and probabilistic HCS designs using rewriting logic, automatically transforming them into executable probabilistic models for SMC.
3. Auditing Methodology: A rigorous process to audit undetectability claims by estimating TPR/FPR of detectors and deriving certified lower bounds on KL divergence, enabling systematic exploration of the performance-privacy tradeoff space.
4. Semantic Alignment: Validation of the framework by comparing model predictions against a physical testbed implementation, demonstrating strong alignment between formal guarantees and empirical reality.

4. Results and Evaluation

The authors evaluated Maude-HCS using a Proof-of-Concept (PoC) HCS involving:

• Control Channel: Iodine (DNS tunneling).
• Data Channel: Destini (steganography over Mastodon social media).
• Testbed: A Dockerized network with NAT, synthetic background traffic, and a passive adversary using Zeek with three detectors (DNS query count, HTTPS request count, and moving average DNS rate).

Key Findings:

• Tradeoff Analysis: The framework successfully quantified the tradeoff between goodput (performance) and KL divergence (detectability). Increasing the rate of covert traffic injection (decreasing wait times) increased goodput but also increased the KL divergence, making the system more detectable.
• Parameter Sensitivity: The system's detectability was highly sensitive to network conditions (packet loss) and background traffic volume. For instance, high packet loss altered the statistical signatures, affecting the KL bounds.
• Detector Impact: Varying detector thresholds (e.g., the multiplier $k$ for moving averages) significantly changed the certified lower bounds, proving that undetectability is relative to the specific adversary strategy.
• Semantic Alignment:
  • Latency/Goodput: The model's predictions for latency and goodput closely matched testbed measurements (within ~13.6% for latency and ~17.1% for goodput).
  • Detection Time: The model accurately predicted the "time-to-detect" for most scenarios, with deviations primarily attributed to modeling inaccuracies in background traffic under high loss rather than the HCS logic itself.
  • KL Divergence: The model showed very low KL divergence between its own output distributions and empirical testbed distributions, validating the fidelity of the simulation.

5. Significance

• Shift from Ad-Hoc to Formal: Maude-HCS moves HCS evaluation from informal, simulation-heavy testing to a principled, formal verification approach. This allows for the systematic exploration of design spaces that would be too costly to test physically.
• Trustworthy Design: By providing certified lower bounds on divergence, the tool gives designers concrete evidence of whether a system meets its privacy goals under specific threat models, rather than relying on "it looks safe" heuristics.
• Scalability: By using SMC and rewriting logic, the framework handles the complexity of distributed, concurrent systems with dynamic actors and unbounded data structures, which are difficult to model with traditional automata-based tools (like UPPAAL or PRISM).
• Future Roadmap: The authors propose using this framework to not just audit existing systems, but to design and generate new HCS protocols automatically, potentially leading to "correct-by-construction" implementations that are optimized for both performance and undetectability before a single line of code is written.

In conclusion, Maude-HCS provides a robust, mathematically grounded methodology for analyzing the fundamental tension between hiding communication and maintaining performance, offering a path toward more secure and reliable covert communication systems.