POST: Protocols, Observabilities and Session Types

Communication is not only an essential organisation principle for emerging large-scale distributed applications, such as those for e-Commerce, e-Science, e-Healthcare and financial technology (FinTech): it is also an effective way to use computational resources, such as microservices and manycore chips. In this new paradigm, communication and concurrency are the norm in software development rather than a marginal concern, enabling architects and programmers to harness the power of hundreds or even thousands of concurrent processes interacting through *message passing*.

However, for this paradigm there is no well-established methodology for software development with safety and security gurantee based on clear and mathematically accurate criteria on its behaviour. This leaves uncertainty on the correctness of the construction of distributed infrastructure. The aim of this fellowship is to establish general and practical foundations for safety enforcement of communication-intensive concurrent and distributed applications, building on a general theory of *multiparty session types*.

Communications in a distributed application are commonly organised into multiple structured conversations (*protocols*) where a developer or programmer wishes to enforce *observabilities* of system behaviours to follow a safety and security criteria given by a protocol. Here *observability* of systems behaviours means a visible sequence of message exchanges with more complex information such as dependency of data, secure information, cost and timing of communications. In the multiparty session types, an end-point system properly carries out its responsibility, so that observable systems behaviours as a whole obey an agreed-upon protocol.

Multiparty session types articulate the basic dynamics in a respective computing paradigm, thus serving as a foundation for modelling, specification, verification, systematic testing and certification, enhanced with other methods such as monitoring and logical assertions. This fellowship aims to fulfil this potential of multiparty session types as types for communication by carrying out experiments. To achieve this goal, the following technical objectives have been identified:

1. The establishment of a uniform type theory for multiparty session types capturing a full range of application-level protocols based on behavioural theory and game semantics, as a foundation of the whole methodology.

2. The establishment of a dependent and refinement type theory of specifications and verifications; and of a scalable algorithm to verify safety and security properties based on automata theory.

3. The development and release of an open-source toolchain, based on (1,2), combined with Application Programming Interface (API) and with industry tools.

4. A theoretically well-founded architecture which can efficiently monitor, trace, log and enforce correct observational behaviour against specifications written in (3).

5. Experiments through collaboration with academic and industry partners, realising formal safety and security assurance against advanced protocols for real-world applications, including multi robotics/UAVs, financial and healthcare systems.

Throughout the research programme, an active and extensive dialogue between theories (1,2) and practice (3,4,5) will be the key enabler for reaching the goals of the fellowship, ultimately establishing cross-disciplinary and co-created ICT research. The project also links assurance methodologies based on session types to the standardisation for Cloud Computing (Cloud Native Computing Foundation) and to the public regulatory requirements for the documentation of financial and e-Healthcare protocols, meeting the goals of People at the Heart of ICT.

This fellowship aims to establish the safety and security assurance principles for communication-intensive software based on session types. The outcomes, based on mathematically accurate criteria for communications, are likely to have deep and broad impacts on the information technology sector, and hence be of considerable benefit to society.

(1) Who might benefit from this research?

The immediate beneficiaries are the partners of this proposal and the application domains they are engaged in, i.e. micro/web-services, distributed containers, legacy code analysis, e-Science (robotics), e-Healthcare and financial technology. More generally, those engaged in the development of large-scale distributed applications will also benefit, ranging from global enterprise to infrastructure for public sectors (e.g. healthcare).

The second class of beneficiaries are those who build tools and environments for the runtime management of distributed tracing (observabilities of systems behaviours), including the middleware targeted to Cloud Computing. The validation algorithms and monitor/tracing architecture offer a comprehensive framework for (hybrid) static and runtime safety enforcement, with automatic or semi-automatic development-time verification.

The third beneficiaries are end-users and society as a whole, especially users of IT infrastructure developed in this fellowship proposal. Once the usability of the methodology is established, the new assurance methodology will lead to a comprehensive certification framework as a public standard. For example, distributed tracing is being standardised through the OpenTracing standard, a language-agnostic standard for distributed tracing, developed by the industry partner (Red Hat). Collaborations with Red Hat will have a large impact on establishing the link with two major open source projects, OpenTracing and Jaeger, part of the Cloud Native Computing Foundation (CNCF).

(2) How might they benefit from this research?

This fellowship project will produce a toolchain whose comprehensive support for software development and safety assurance will be tested through prominent real large-scale use cases with the project partners. The development and management experience with the partners will make our toolchain usable by professional developers (including architects, designers and programmers).

In the medium term, when associated development methods have reached sufficient maturity, it is possible for application providers who are using OpenTracing or GitOps to contribute to the enhancement of the toolchain or provide their own versions. Similarly the ecosystem of programming languages and APIs for protocols (i.e. Scribble framework developed) will be enriched by those working inside and outside academic institutions.

Finally the end-users will benefit from the use of safer services with a clear guarantee of their behaviour. Applications will enjoy enriched functionalities because more time and cost can be spent on new functions rather than maintenance and informal manual assurance. Such a trend will be accelerated when the competition in the software tools market for the development and assurance of communication-intensive software emerges (through DevOps), and will be further assisted by a public standard for software quality based on the proposed methodologies. This will ensure the safety of large-scale infrastructures such as financial networks, healthcare and robotics/UAVs, all of which offer critical services and knowledge to our society, and influencing the policy and regulator, putting People in the Heart of ICT.