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.
|