Formally Verifying Undetectability in Hidden Communication Systems with Maude-HCS
|
ABSTRACT A hidden communication system (HCS) embeds hidden messages within ordinary network activity by repurposing existing protocols as subliminal channels. Although prior work provides useful tools for assessing the detectability of the HCS, there is no general and modular framework that both formalizes what it means for an HCS to be undetectable and formally verifies that a concrete implementation satisfies this property. In this talk, we present a formal approach for specifying and analyzing HCS detectability. We model an HCS hunting adversary whose task is to determine whether the network traffic it observes contains hidden communication. Privacy is formalized as a statistical hypothesis-test by requiring that the adversary's view of the protocol be indistinguishable, under appropriate probability measures, from the view it would obtain when no hidden communication is present in the network. To model and analyze the privacy of real-world HCSs, we develop the Maude-HCS toolchain. Maude-HCS is one of the first generalized and modular toolchains for specifying and reasoning about HCSs at real-world scales. The toolchain, comprised of a Domain Specific Language (DSL) and analysis toolkit, enables network designers to explore alternative HCS designs quickly and effectively and provides provable privacy-performance guarantees needed to trust the design—a necessary step for HCS users to ultimately trust the system, especially when operating in high threat environments where detection of illicit communication has dire consequences. Designers formally model the network protocols, the techniques for hiding communications within them, and the HCS-hunting adversary capabilities, and specify the desired privacy, performance, and scalability properties. Maude-HCS computes high confidence measures quantifying performance and scalability properties using statistical model checking. The models directly incorporate adversary observables that enable quantifying the adversary’s detectability advantage. We evaluate the toolchain on two real-world HCS instantiations with increasing complexity, using a novel methodology for validating model guarantees against empirical measures obtained from a real-world testbed. Considering a passive adversary initially, we quantify performance and scalability measures attesting to the predictive power of the models, and we quantify detectability, and evaluate sensitivity of the measures under a wide range of HCS Maude-HCS is under active development, and open sourced at Authors and Affiliations: Dr. Joud Khoury (RTX BBN Technologies) <joud.khoury@rtx.com> DISTRIBUTION STATEMENT A: Approved for public release; distribution is unlimited. |
|
BIO Dr. Khoury is a Senior Principal Fellow in the Non-Kinetic Capabilities and Technologies business unit at RTX BBN Technologies. His broad expertise in networks and systems enables his emphasis on building practical solutions suitable for transition. His current work sits at the intersection of networks and systems, security and privacy, formal methods, and machine learning. He is currently leading two DARPA programs, and has previously led several efforts for DARPA, ONR, IARPA, and the IC that have elevated the performance and security of networks at all layers of the network stack. Dr. Khoury authored a book on “Internet Naming and Discovery”, several book chapters, more than 20 peer-reviewed conference papers. He holds more than a dozen patents. He received his MS and PhD in computer engineering from the University of New Mexico, Albuquerque. |