SPA: Systematic Protocol Analysis

Poster.png: 10817x14423, 7432k (May 01, 2015, at 02:40 AM)
SPA Poster @ NSDI'15

Systems developers and operators ask tough questions like:

  • Is this client compatible with this server?
  • If I swap out this server stack with another, will the system still work in the same way?
  • Does adding this proxy modify the system behavior?
  • How many messages can it take for this distributed transaction to converge?
  • Does this system recover from message loss?

The current best-practice to answer such questions involves extensive manual testing, which is both labor intensive and provides limited assurance.

Continuing the line of research behind the PIC project, SPA creates a general framework for systematic analysis of protocol implementations. The system provides a toolkit of operations that can be combined to systematically explore the protocol code and map out the message spaces that result from these what-if scenarios. One can then combine the results to determine such properties as:

  • Equivalence: comparing outcomes for equivalent inputs with differing scenarios.
  • Validity: checking whether assertions and sanity checks hold for all inputs.
  • Complexity: determining the depth of protocol interactions.

The project is still in a prototype stage, however the following analyses are operational in small-scale demonstrations:

  • Interoperability: a straightforward port of the PIC project, this analysis automates the search for test cases that breakdown interoperability between protocol participants. The analysis is also further augmented to support the following variants:
    • Client-Server Interoperability: the original analysis between a single sender and a single receiver.
    • Client-Proxy-Server Interoperability: further checking if adding a proxy between the two end-points adds (or fixes) interoperability issues.
  • Manipulation Attacks: a straightforward porting of the static analysis in MAX, this analysis finds ways to trick a receiver into favoring the sender.
  • Equivalence: this compares message spaces from different scenarios, namely:
    • Client Equivalence: checks whether two different clients generate the same messages for the same inputs.
    • Server Equivalence: checks whether two different servers respond in the same way to all messages.
    • Client-Server Equivalence: checks whether two different servers respond in the same way to the messages sent by a particular client (as opposed to every possible message).
    • Proxy Equivalence: checks whether adding a proxy between a client and server changes the response as seen by the client

Further Reading

Luis Pedrosa; Systematic Analysis of Network Protocol Implementations. PhD Thesis, University of Southern California. 2016
Open Website Download PDF Document More Information
Luis Pedrosa, Ari Fogel, Nupur Kothari, Ratul Mahajan, Todd Millstein, and Ramesh Govindan; SPA: A General Framework for Systematic Protocol Analysis. Presented at The 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15), Oakland, CA, USA. 2015
Open Website Download PDF Document More Information
Luis Pedrosa, Ari Fogel, Nupur Kothari, Ratul Mahajan, Todd Millstein, and Ramesh Govindan; Toward systematic analysis of networked systems. Presented at The NeTS Early Career Workshop 2015, Arlington, VA, USA. 2015
Open Website Download PDF Document More Information

Getting the Source

The SPA 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)