A formally-verified migration protocol for mobile, multi-homed hosts

Matvey Arye, Erik Nordström, Robert Kiefer, Jennifer L. Rexford, Michael Joseph Freedman

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

Abstract

Modern consumer devices, like smartphones and tablets, have multiple interfaces (e.g., WiFi and 4G) that attach to new access points as users move. These mobile, multi-homed computers are a poor match with an Internet architecture that binds connections to fixed endpoints with topology-dependent addresses. As a result, hosts typically cannot spread a connection over multiple interfaces or paths, or change locations without breaking existing connections. In this paper, we create an end-to-end connection control protocol (ECCP) that allows hosts to communicate over multiple interfaces with dynamically-changing IP addresses and works with multiple data-delivery protocols (i.e., reliable or unreliable transport). Each ECCP connection consists of one or more flows, each associated with an interface or path. Through end-to-end signaling, a host can move an existing flow from one interface to another, or change its IP address, without any support from the underlying network. We develop formal models to verify that ECCP works correctly in the presence of packet loss, out-of-order delivery, and frequent mobility, and to identify bugs and design limitations in earlier mobility protocols.

Original languageEnglish (US)
Title of host publication2012 20th IEEE International Conference on Network Protocols, ICNP 2012
DOIs
StatePublished - Dec 1 2012
Event2012 20th IEEE International Conference on Network Protocols, ICNP 2012 - Austin, TX, United States
Duration: Oct 30 2012Nov 2 2012

Publication series

NameProceedings - International Conference on Network Protocols, ICNP
ISSN (Print)1092-1648

Other

Other2012 20th IEEE International Conference on Network Protocols, ICNP 2012
CountryUnited States
CityAustin, TX
Period10/30/1211/2/12

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Software

Keywords

  • end-to-end signaling
  • formal methods
  • migration
  • mobile devices
  • network architecture

Fingerprint Dive into the research topics of 'A formally-verified migration protocol for mobile, multi-homed hosts'. Together they form a unique fingerprint.

  • Cite this

    Arye, M., Nordström, E., Kiefer, R., Rexford, J. L., & Freedman, M. J. (2012). A formally-verified migration protocol for mobile, multi-homed hosts. In 2012 20th IEEE International Conference on Network Protocols, ICNP 2012 [6459961] (Proceedings - International Conference on Network Protocols, ICNP). https://doi.org/10.1109/ICNP.2012.6459961