Towards a formalism for understanding properties of hidden communication systems and weird networks

ABSTRACT

Cryptography and steganography have evolved side by side for millennia as means of secrecy. Whereas cryptography has enjoyed mathematical definitions of security, formal methods approaches to proving security (e.g. EasyCrypt/Lean) and steganography (hidden communication systems) have mostly been ad-hoc constructions and arguments of “hidden-ness”. A path towards formalism has been explored by the DARPA Resilient Anonymous Communication for Everyone (RACE) program, and further expanded on in the Provably Weird Network Deployment and Detection (PWND2) program. In this talk, we discuss our experiences in work done as performers on those programs.

We investigated formal notions of anonymity in private communication using rigorous cryptographic frameworks. In particular, we examined sender and receiver anonymity and found that unlinkability between senders and receivers is central to achieving strong sender-receiver anonymity in strong adversarial models where adversaries conduct state-level censorship and surveillance. Specifically, we define sender-receiver anonymity such that an adversary cannot link the sender of a message to its corresponding receiver, even when the adversary knows the set of participating parties and can observe network traffic. Within this cryptographic framework, we developed CARMA (Covert Anonymous and Resilient Messaging App), an anonymous overlay communication network based on leveraging secure multiparty computation to achieve sender-receiver anonymity.

As part of ongoing work, we are currently developing new formal techniques for proving security, privacy, and performance properties of distributed systems built on weird networks. This is a fundamentally difficult problem, since it combines the verification challenges of concurrency and probabilistic behavior – general solutions for either problem, even in isolation, remain elusive. Our solution, the TOPSPIN DSL, is a choreographic language that simplifies verification tasks by modeling a distributed system using a single global specification that can be compiled into separate programs for the participants to run. Unlike prior work, the TOPSPIN DSL is a fully probabilistic choreographic language, which allows it to model complex probabilistic behaviors of weird networks. To verify security, privacy, and performance properties, we have built automated type-based analyses for the TOPSPIN DSL, which we have used in the PWND2 program to model and analyze the program’s challenge problems.

As a final case study, we describe our experiences developing Unidentified Protocol Generation (UPGen), a system that automates the production of novel protocols for encrypted communication that are unfamiliar to a nation-state censor. Rather than rely on a single obfuscation protocol (e.g., obfs4 or Shadowsocks), UPGen provides a “fresh” encrypted obfuscation protocol for each proxy, making wide-scale traffic analysis and fingerprinting attacks ineffective (since fingerprinting a single instance of an UPGen protocol does not enable fingerprinting never-seen UPGen protocols). Given that UPGen can produce about 4×1022 different encrypted protocols, we discuss the challenges of ensuring that UPGen yields only secure, robust, performant, and believable encrypted communication schemes.

BIO

Steve Lu, Ph.D., is the CEO of Stealth Software Technologies, where he leads a world-class team dedicated to protecting highly sensitive data through advanced cryptography. Under his leadership, the company delivers innovative solutions in multiparty computation, zero-knowledge proofs, and distributed consensus, empowering organizations to safely analyze and share encrypted data. An accomplished executive and principal scientist, Dr. Lu has a proven track record of securing and executing advanced research projects for U.S. Federal agencies, including DARPA. Beyond his corporate leadership, he is a recognized voice in the academic community. He is the recipient of several awards for his cryptographic research and actively publishes in and contributes to leading scientific conferences and journals. Dr. Lu earned his Ph.D. in Mathematics (Cryptography) from UCLA and his M.S. in Computer Science (Artificial Intelligence) from Stanford University.