FlexMove: A Protocol for Flexible Addressing on Mobile Devices (MSE thesis)
Abstract:
The Internet has been a wildly successful platform for global communication. However, new
technologies are now running into its limitations. Mobile devices are becoming an increasingly
prevalent, yet the network does not support device movement in a streamlined manner. Existing
solutions either use inefficient "triangle routing" or they allow ongoing connections to break when
a device moves and rely on application-level recovery mechanisms. Similarly, virtual machine migration allows servers to change locations but runs into some of the same limitations inherent to
device movement. In addition, network-enabled devices often have more than one interface to the
Internet (e.g., Wifi and 3G) but can only use a single interface per connection. We propose FlexMove, a protocol that operates between the network and transport layer, and that allows devices to
use multiple interface for a single connection and at the same time preserves ongoing connections
across mobility events. To avoid changing the underlying network architecture, FlexMove uses inband signaling to enable communicating hosts to update each others addresses as they move. This allows the network to support device movement while keeping addresses location-dependent. To
verify that this protocol does not exhibit misbehaviours such as livelock and deadlock, FlexMove
has been formally modeled and verified in the SPIN protocol verification tool. This verification
exhaustively verifies protocol correctness for connections with up to five device movement events
and reflects network loss and reordering.