Inference and Analysis of Formal Models of Botnet Command and Control Protocols

We propose a novel approach to infer complete protocol state machines in realistic high-latency network setting, and apply it to the analysis of botnet C&C protocols. Our proposed techniques enable an order of magnitude reduction in the number of queries and time needed to learn a botnet C&C protocol than classic algorithms (from days to hours for inferring MegaD C&C protocol). We also show that the computed complete protocol state machines enable powerful analysis for botnet defense, including finding weakest links in a protocol, uncovering protocol design flaws, inferring the existence of unobservable communication back-channels among botnet servers, and finding deviations of protocol implementations which can be used for fingerprinting. Our experimental results on MegaD demonstrate that our technology offers invaluable novel insights to existing problems on botnet C&C and provides a powerful weapon for botnet defense.