A Verified Session Protocol for Dynamic Service Chaining

Pamela Zave, Fabricio B. Carvalho, Ronaldo A. Ferreira, Jennifer Rexford, Masaharu Morimoto, Xuan Kelvin Zou

Research output: Contribution to journalArticlepeer-review

Abstract

Middleboxes are crucial for improving network security and performance, but only if the right traffic goes through the right middleboxes at the right time. Existing traffic-steering techniques rely on a central controller to install fine-grained forwarding rules in network elements - at the expense of a large number of rules, a central point of failure, challenges in ensuring all packets of a session traverse the same middleboxes, and difficulties with middleboxes that modify the 'five tuple.' We argue that a session-level protocol is a fundamentally better approach to traffic steering, while naturally supporting host mobility and multihoming in an integrated fashion. In addition, a session-level protocol can enable new capabilities like dynamic service chaining, where the sequence of middleboxes can change during the life of a session, e.g., to remove a load-balancer that is no longer needed, replace a middlebox undergoing maintenance, or add a packet scrubber when traffic looks suspicious. Our Dysco protocol steers the packets of a TCP session through a service chain, and can dynamically reconfigure the chain for an ongoing session. Dysco requires no changes to end-host and middlebox applications, host TCP stacks, or IP routing. Dysco's distributed reconfiguration protocol handles the removal of proxies that terminate TCP connections, middleboxes that change the size of a byte stream, and concurrent requests to reconfigure different parts of a chain. Through formal verification using Spin and experiments with our prototype, we show that Dysco is provably correct, highly scalable, and able to reconfigure service chains across a range of middleboxes.

Original languageEnglish (US)
Article number9264708
Pages (from-to)423-437
Number of pages15
JournalIEEE/ACM Transactions on Networking
Volume29
Issue number1
DOIs
StatePublished - Feb 2021

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Networks and Communications
  • Electrical and Electronic Engineering

Keywords

  • NFV
  • Session protocol
  • middleboxes

Fingerprint Dive into the research topics of 'A Verified Session Protocol for Dynamic Service Chaining'. Together they form a unique fingerprint.

Cite this