Conversation-Based Governance for Distributed Systems by Multiparty Session Types

Software is increasingly organised centring on distributed communicating processes. This is especially true in large-scale distributed computing platforms such as the backend of popular Web-based services and public sector platforms for e-healthcare and e-science, which often provide lifelines of society. An application is organised as a dynamic collection of distributed components. The framework is based on interacting processes, which extends the traditional paradigm of functions and objects and which allows far more versatile and scalable organisation of software components.

Assuring safety in such distributed systems is a vital societal concern: many platforms are long-lived, offer socially critical services, and collect security-sensitive data; safety violations, including security breaches, can have wide-ranging consequences, from temporary service outage to information leakage to exploitation of security vulnerability by criminal organisations. However, existing assurance methodologies are based on objects and functions: no well-established formal assurance methodologies are known for distributed systems. Large-scale distributed computing infrastructures are like skyscrapers used by hundreds of thousands of people, for building which the well-established structural engineering principles are used as a foundation of safe engineering. Can we establish the corresponding engineering principles for building software skyscrapers vital to modern society?

Against this background, the central aim of this project is to establish a general, formally based safety assurance methodology for distributed systems, which we call conversation-based governance. The conversation-based governance starts from advanced types for capturing conversations, called multiparty session types (MPSTs), recently introduced by the PIs and extensively studied by researchers. Building on the latest theoretical results and on the PIs' ongoing collaborations with the project partners, we introduce the new development and assurance framework based on MPSTs. At the centre of our approach is a high-level, programming-language-agnostic MPST-based declarative protocol description language.

The safety assurance in this framework is realised through verifications of distributed components against formal specifications in this protocol language, performed either statically (at the development time) or dynamically (at runtime), of which we place an emphasis on the latter: large-scale distributed systems are rarely amenable to static verification as a whole due to, for example, heterogeneous components, so that only the dynamic verification and enforcement can offer a comprehensive safety assurance. It is due to this emphasis on runtime policing of conversations that we call the proposed assurance framework, conversation-based governance. The project will establish this new methodology through the following tasks:

(1) The development of a programing-language-agnostic protocol description language, called Scribble, and its open source tool chain, programming interfaces (APIs) and runtimes, backed up by a uniform type theory of MPSTs.

(2) The development of an assertion language for specifying and verifying refined safety properties as elaboration of protocols, together with a policy language linked to the assertion language. Decentralised monitors backed up by a theory of the pi-calculus offer efficient, scalable runtime verification and enforcement.

(3) Large-scale experiments through collaboration with project partners, realising formal safety assurance for real-world applications, including global cyberinfrastructure, enterprise software, and messaging middleware.

Throughout the project, an extensive dialogue between theories and practice will be conducted, leading to truly effective principles and tools for general safety assurance methodologies of distributed systems vital for future IT infrastructures and society.

The project aims to establish a general and effective development, execution and safety assurance framework for distributed systems building on new structuring methods (conversations and protocols), backed up by formal theories. Embodied as concrete software tools, the proposed methodology will be tested extensively in actual distributed computing environments, giving continuous feedback to the theoretical and design-level development. If successful, the impact of the research will permeate many areas of computing and society in long years to come, as well as meeting some of their urgent needs.

(1) Who might benefit from this research?

The immediate beneficiaries are the development partners of this proposal and those in the related application domains, i.e. e-Science and oceanography (WP3-1), distributed enterprise applications (WP3-2), and scalable messaging middleware (WP3-3). Further once the tools and environments become usable, they also become usable by others, accompanied by open source tools and concrete use scenarios: there is an accelerating demand for developing large-scale applications centring on distributed communicating processes, especially in clouds. For these reasons we expect that those working on distributed systems including global enterprises, systems integration, public infrastructure (e.g. e-healthcare and e-Science) and cloud computing are among the likely beneficiaries in near future.

Finally the end-users and society as a whole will benefit from high-level software quality assurance provided by the proposed methodologies, especially users of infrastructural IT services providing lifeline support, quality of life and social welfare. For example, Ocean Observatories Initiative, a partner of this project (WP3-1), is building distributed observatories providing information from oceans, which is vital for climate change research.

(2) How might they benefit from this research?

First, with the development partners of this project, we carry out extensive experiment of the methodologies and tools from WP1/2, offering constant feedback to our development, leading to robust methodologies and tools truly usable by their developers in their environments. Since all partners are considering the usage of the methodologies in long terms much beyond the duration of this project (for example, the OOI CI has an operational time span of more than 30 years), and because the general principles developed in this project are not restricted to specific application domains but intended for all kinds of software based on distributed communicating processes, they can continue to leverage the fruits from the present collaboration and exploit their potential, leading to rapid accumulation of knowledge.

For the adoption of the proposed methodology beyond these partners, it is important that the methodology is built on a few general principles, distilled as theories, so that it is amenable to systematic teaching, training and extensions. Once their value is clear, any enterprise working on distributed computing environments (e.g. IBM, Microsoft, VMware, Red Hat, Google, and SAP) would be able to adopt them, and may even start to contribute to the enhancement of our open source tools or to provide their own counterparts, leading to the creation of a market for new generation of software tools and methodologies.

In the long term, we expect that the impact will reach the general public who use distributed infrastructures, through a wide adoption of the proposed methodology and its ramifications. Pronounced societal benefits will arise from a public standard for comprehensive certification framework on distributed applications based on the proposed methodologies, contributing to the safety guarantee for infrastructures such as financial networks and cyberinfrastructure for E-science (WP3-1), all of which offer critical services and knowledge to our society.