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

TL;DR

Maude-HCS is developed, an executable modeling and analysis framework that provides a principled and executable foundation for reasoning about undetectability-performance tradeoffs in complex HCS designs and 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 such as KL divergence.

Abstract

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. In this work, we formalize undetectability as the statistical indistinguishability of observable execution traces under two deployments: a baseline system without hidden communication and an HCS deployment carrying covert traffic. Undetectability is expressed as a bound on a quantitative measure of distance between the trace distributions induced by these two executions. We develop Maude-HCS, an executable modeling and analysis framework that provides a principled and executable foundation for reasoning about undetectability-performance tradeoffs in complex HCS designs. Maude-HCS allows designers to specify protocol behavior, adversary observables, and environmental assumptions, and to generate Monte Carlo samples from the induced trace distributions. We show that Maude-HCS 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 such as KL divergence. This enables systematic evaluation of detectability and its tradeoffs with performance under explicitly stated modeling assumptions. Finally, we evaluate Maude-HCS on tunneling-based HCS instantiations and validate model predictions against measurements from a physical testbed. For passive adversaries observing timing and traffic statistics, we quantify how undetectability and performance vary with protocol configuration, background traffic, and network loss, and demonstrate strong semantic alignment between model-based guarantees and empirical results.

Figures (7)

• Figure 1: Maude-HCS reduces the burden on the designer while ensuring semantic consistency. Designers build nondeterministic models of the underlying network ①, of the weird transforms ②, and of the application ③ as generalized actor theories. They also provide the actor and system configs ④ which are used to generate the initial HCS configuration. Designers then specify the adversary observables ⑤ (and extend the adversary detection logic as needed), and the performance relevant events to monitor ⑥. Maude-HCS generates executable, timed, and probabilistic specification used for statistical analysis. For analysis, designers specify the quantitative performance and privacy properties of interest and the SMC parameters $\alpha$, $\delta$ (and hosts for distributed SMC) ⑧. These are used to produce performance and privacy guarantees.
• Figure 2: The HCS system and network modeled and instantiated on the testbed, and used for evaluation.
• Figure 3: Privacy–performance tradeoff across Scenarios 1, 4, and 7. Each subplot corresponds to a different network condition (see Table 1). For each scenario, Alice’s mean wait time between posts in the Markov model is varied while all other parameters are fixed. Each point shows the achieved goodput (bytes/sec) and the corresponding certified lower bound on $\mathrm{KL}(\mathsf{View}^{\mathrm{HCS}}{t}|\mathsf{View}^{\mathrm{Ord}}{t})$, derived from SMC estimates of detector TPR and FPR. Across scenarios, decreasing the wait time generally increases goodput and generally increases statistical distinguishability between HCS and ordinary executions, though the magnitude of the KL bound depends on network loss and background traffic.
• Figure 4: We vary the moving average detector threshold multiplier $k$ (section \ref{['sec:quanti-properties']}) and observe the effect on KL divergence bounds (left), on probability of alarm for the moving average detector MA1 (middle), and on operating duration (right). The bar around the alarm datapoints is the radius.
• Figure 5: We vary the mean wait time (sec) in Alice's markov model; longer waits between posts means lower performance. We observe the effect on KL divergence bounds (left), on probability of alarm for the cumulative C8 detector (middle), and on operating duration (right). The bar around the datapoints is the radius. In the KL bounds figure on the left, scenario 1 and 4 datapoints overlap. The threshold $N=80$ for the C.8 detector is fixed.

Theorems & Definitions (1)

• definition 1: $(\mathcal{M}, d)$-Undetectability