Skip to main content

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

Author(s): Arye, Matvey; Nordström, Erik; Kiefer, Robert; Rexford, Jennifer; Freedman, Michael J

To refer to this page use:
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.
Publication Date: 2012
Citation: Arye, Matvey, Erik Nordström, Robert Kiefer, Jennifer Rexford, and Michael J. Freedman. "A formally-verified migration protocol for mobile, multi-homed hosts." In 2012 20th IEEE International Conference on Network Protocols (ICNP) (2012). doi:10.1109/ICNP.2012.6459961
DOI: 10.1109/ICNP.2012.6459961
ISSN: 1092-1648
Type of Material: Conference Article
Journal/Proceeding Title: 2012 20th IEEE International Conference on Network Protocols (ICNP)
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.