Karl Palmskog

Verification of the Session Management Protocol

Abstract

The Session Management Protocol (SMP) is an important part of a session layer for mobile, disconnection- and delay-tolerant communication developed at Ericsson Research. This layer lets applications use sessions instead of sockets to communicate with network endpoints. Such sessions are very persistent, surviving even network outages and changes in network attachment. SMP may run on top of TCP/IP or other network protocols, and handles data integrity and resumption after disconnection and suspension for sessions. It also deals with sending and processing messages related to the communication context.

In this thesis, we formally describe SMP, specify its correctness, and verify several protocol models in the validation language Promela by using the model checker Spin. As a preparation for verification, the protocol is characterized informally in a structured manner. After outlining the modelling and verification approach, we give reports on model checking. In particular, we highlight the detection of an error in data integrity management, and describe how this discovery led to changes in the protocol.

By applying abstraction and separating the concerns of safety and liveness, protocol model complexity was reduced to permit exhaustive verification in Spin. Model checking results prompt the conclusion that SMP reliability has increased through the verification effort.

Verifiering av Session Management Protocol

Sammanfattning

Session Management Protocol (SMP) utgör en viktig del av ett sessionslager för mobil, avbrotts- och fördröjningstolerant kommunikation utvecklat vid Ericsson Research. Lagret låter applikationer använda sessioner istället för sockets för att kommunicera med nätverksändpunkter. Sådana sessioner är anmärkningsvärt persistenta - de överlever nätverksfel och ändringar av nätverksanslutningspunkt. SMP kan användas ovanpå TCP/IP eller andra nätverksprotokoll, och hanterar dataintegritet och återanslutning efter avbrott för sessioner. Protokollet sköter också sändning och mottagning av meddelanden relaterade till kommunikationskontext.

I den här rapporten beskriver vi SMP formellt, specificerar korrekthet och verifierar flera modeller i valideringsspråket Promela med hjälp av model checkern Spin. Som en förberedelse för verifieringen karakteriseras protokollet informellt på ett strukturerat sätt. Efter en beskrivning av angreppssättet till modellering och verifiering, rapporteras om tillämpningen av model checking. Speciellt belyser vi upptäckten av ett fel i mekanismen som ser till att dataintegriteten bibehålls, och beskriver hur denna upptäckt ledde till ändringar i protokollet.

Genom att använda abstraktion och separera safety- och liveness-krav reducerades protokollmodellkomplexiteten, vilket tillät fullständig verifiering i Spin. Resultaten av model checking lämnade utrymme för slutsatsen att tillförlitligheten för SMP ökat efter verifieringsinsatsen.