The shim6 protocol specifies a layer 3 shim approach and protocol for providing locator agility below the transport protocols, so that multihoming can be provided for IPv6 with failover and load spreading properties, without assuming that a multihomed site will have a provider independent IPv6 address prefix which is announced in the global IPv6 routing table. The hosts in a site which has multiple provider allocated IPv6 address prefixes, will use the shim6 protocol specified in this document to setup state with peer hosts, so that the state can later be used to failover to a different locator pair, should the original one stop working.

»» Read more at the Shim6 website

Formalization and Verification of the protocol

While the draft of the Shim6 protocol was in progress, Matthijs Mekking formalized the description of the protocol and verified its properties. The formal model is made with the model checking tool UPPAAL. After applying formal methods to the protocol, Matthijs tested a Shim6 beta implementation that was developed by Sébastien Barré for the UCL, a large university in Belgium. Both projects were useful in order to improve the Shim6 working group documents.

This resulted in a thesis, which can be downloaded here (abstract). You can also download the complete package with thesis, formal models, test code and wireshark patch.

It was also presented in a poster at the VVSS 2007 symposium, organized by LaQuSo.

Wed Sep 25 2013

© Stichting NLnet Labs

Science Park 400, 1098 XH Amsterdam, The Netherlands, subsidised by NLnet and SIDN.