Position Paper: A Case for Machine-Checked Verification of Circumvention Systems
Authors: Vitor Pereira (Algoritmo Sapiente, LDA), Ahmed Irfan (SRI), Vinod Yegneswaran (SRI), Nick Feamster (University of Chicago), Prateek Mittal (Princeton University), Vitaly Shmatikov (Cornell Tech)
Year: 2025
Issue: 2
Pages: 46–50
Abstract: We present a case for adopting formal verification as a methodology for evaluating hidden communication systems (HCS), with the goal of supplementing the current ad hoc and informal analysis strategies used in state-of-the-art HCS with a rigorous pathway to the analysis of these systems. Our position is that the core security properties of these systems, like resistance to traffic analysis and detectability, are fundamentally distinguishability problems aligned with the same distinguishability concepts found in cryptography. Thus, we propose the lifting of cryptographic results to the HCS domain and the leverage of the existing formal verification infrastructure available for cryptography to derive concrete security and performance bounds for HCSs. Concretely, we propose the usage of simulation-based cryptography as a rigorous framework to model interactions between users, censors, and network protocols, allowing precise definitions of censorship relevant goals such as unobservability, unblockability, covertness, and performance guarantees. We showcase the utility of this formal approach by presenting VeriWeird, an envisioned tool that bridges the formal gap existing in state-of-the-art HCS and demonstrate our approach through a (preliminary) analysis of meek. Our case study highlights the potential of machine-checked verification to provide strong, systematic assurances of resilience and also identify vulnerabilities in adversarial environments.
Copyright in FOCI articles are held by their authors. This article is published under a Creative Commons Attribution 4.0 license.
