Information Technology Reference
In-Depth Information
SPY: Local Verification of Global Protocols
Rumyana Neykova, Nobuko Yoshida, and Raymond Hu
Imperial College London, UK
Abstract.
This paper presents a toolchain for designing deadlock-free
multiparty global protocols, and their run-time verification through au-
tomatically generated, distributed endpoint monitors. Building on the
theory of multiparty session types, our toolchain implementation vali-
dates communication safety properties on the global protocol, but en-
forces them via independent monitoring of each endpoint process. Each
monitor can be internally embedded in or externally deployed alongside
the endpoint runtime, and detects the occurrence of illegal communica-
tion actions and message types that do not conform to the protocol. The
global protocol specifications can be additionally elaborated to express
finer-grained and higher-level requirements, such as logical assertions on
message payloads and security policies, supported by third-party plugins.
Our demonstration use case is the verification of choreographic commu-
nications in a large cyberinfrastructure for oceanography [10].
1 Introduction
The application-level interactions in distributed systems and Web services often
involve complex, high-level communication patterns between multiple parties.
It is common for implementations of each participant to be written separately,
or for a system to be constructed by composing separate services managed by
different administrative domains. Implementations are also commonly based on
informal protocol specifications, and thus informal verification mechanisms, and
can be prone to concurrency errors such as communication mismatch (e.g. the
arrival of an unexpected message or request of an unsupported service opera-
tion) and deadlock (e.g. party A waits to receive a message from B while B is
waiting for a message from A). This is why the need for rigorous description and
verification of protocols has been observed in many different contexts.
The Scribble language [6,12] (foundation of the JBoss Savara project [13])
is a formal protocol description language developed towards tackling this chal-
lenge. The goal of Scribble is to provide an intuitive engineering language and
tools, based on the theory of multiparty session types (MPST) [7], for spec-
ifying and reasoning about message passing protocols and their implementa-
tions. As a verification technique, the previously published implementations
of MPST focus on static type checking of protocol specifications against end-
point processes. Well-typed processes are guaranteed to enjoy properties such
as communication-safety (all processes conform to a globally agreed commu-
nication protocol) and deadlock-freedom. Static session type checking in these
