FlexMove: A Protocol for Flexible Addressing on Mobile Devices (MSE thesis)
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.