Synthesizing Attacks Against Communication Protocols
Abstract: The internet is composed of communication protocols such as the Transmission Control Protocol (TCP). These protocols should be robust against adversarial attacks (e.g. message replay) and benign malfunction (e.g. packet loss). Given a formal model of a communication protocol that is provably robust against benign malfunction, we automatically synthesize an adversarial program that causes the protocol to malfunction (e.g. deadlock). We apply this technique to TCP, and analyze the synthesized attacks. Finally, we use block-diagrams to formalize threat models, and employ this formalization to define a generalized version of the Attacker Synthesis Problem.
Bio: Max von Hippel graduated from the University of Arizona Honors College with a BS in Math (Comprehensive Option) and Minor in Computer Science. His favorite classes were Math 415B and Math 401B - algebra and logic - and now he studies Formal Methods - the algebra of logic. He previously completed an Honors Senior Thesis on IoT Security with Dr. Ming Li and Dr. Bryden Cais. You can read more about Max's research interests on his homepage, here: https://www.khoury.northeastern.edu/people/max-von-hippel/