PIC: Protocol Interoperability Checker

Poster.png: 3072x3840, 1699k (December 02, 2013, at 10:57 PM)
PIC Poster @ SOSP'13

Interoperability among different implementations of a protocol is essential for correct and reliable operation of networked systems. Today, protocol interoperability testing is largely a manual process in which developers devise and check interesting test cases manually, typically at large vendor gatherings known as bake-offs. Consequently, many issues go undiscovered in testing and reveal themselves after the implementations have been deployed.

PIC is a tool that analyzes real protocol implementations and automates the search for potential interoperability problems, while requiring little developer input. PIC uses program analysis techniques to map out the sets of messages a sender can generate for a given protocol interaction, as well as the set of messages that a receiver will reject as invalid. These two sets are then combined and an SMT solver is employed to generate concrete test-cases that exercise the interoperability issues therein.

Project Contributions

The project's main contributions are:

  • Automated search for interoperability issues: PIC uses program analysis to systematically explore protocol code and automatically generate test-cases that demonstrate a sender in a protocol interaction sending a message that a receiver subsequently considers invalid.
  • Scaling to real-world protocol code: to get PIC to operate on real-world protocol code, several techniques had to be developed to leverage domain knowledge of how protocol code is built to guide and prune the enormous search-space into something more manageable.
  • Finding real interoperability issues: PIC was used to analyze two implementations each of the SPDY protocol and the Session Initiation Protocol (SIP). A total of 22 interoperability issues were discovered and reported. Many have since been fixed.

Future Work

Continuing with the lessons learnt with PIC, we are now developing a more general analysis framework as a part of the Systematic Protocol Analysis (SPA) project.


PIC Talk @ NSDI'15

Further Reading

Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, and Todd Millstein; Analyzing Protocol Implementations for Interoperability. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15). 2015
Open Website Download PDF Document More Information
Luis Pedrosa, Ari Fogel, Nupur Kothari, Ratul Mahajan, Todd Millstein, and Ramesh Govindan; Analyzing Protocol Implementations for Interoperability. Presented at The 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15), Oakland, CA, USA. 2015
Open Website Download PDF Document Download MPEG-4 Video More Information
Luis Pedrosa, Ari Fogel, Nupur Kothari, Ratul Mahajan, Todd Millstein, and Ramesh Govindan; Toward Automated Interoperability Testing of Protocol Implementations. Presented at The 24th ACM Symposium on Operating Systems Principles (SOSP'13), Farmington, PA, USA. 2013
Open Website Download PDF Document More Information

Getting the Source

The PIC source code is hosted on the NSL GitHub project website. To create a local copy of the repository run:

git clone https://github.com/USC-NSL/SPA.git

People

  • Luis Pedrosa (USC)
  • Ari Fogel (UCLA)
  • Nupur Kothari (USC)
  • Ratul Mahajan (Microsoft Research)
  • Todd Millstein (UCLA)
  • Ramesh Govindan (USC)