Analyzing protocol implementations for interoperability
Luis D. Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, Todd D. Millstein · 2015
Abstract — We propose PIC, a tool that helps devel-opers search for non-interoperabilities in protocol imple-mentations. We formulate this problem using intersec-tion of the sets of messages that one protocol partici-pant can send but another will reject as non-compliant. PIC leverages symbolic execution to characterize these sets and uses two novel techniques to scale to real-world implementations. First, it uses joint symbolic execution, in which receiver-side program analysis is constrained based on sender-side constraints, dramatically reducing the number of execution paths to consider. Second, it in-corporates a search strategy that steers symbolic execu-tion toward likely non-interoperabilities. We show that PIC is able to find multiple previously unknown non-interoperabilities in large and mature implementations of the SIP and SPDY (v2 through v3.1) protocols, some of which have since been fixed by the respective developers. 1