POST: Protocols, Observabilities and Session Types

通信不仅是新兴的大规模分布式应用程序的基本组织原则，如电子商务、e-Science、e-Healthcare和金融科技(金融科技)：它也是使用微服务和多核心芯片等计算资源的有效方式。在这个新的范例中，通信和并发是软件开发中的规范，而不是边缘关注点，使架构师和程序员能够利用数百甚至数千个并发进程通过*消息传递*进行交互的能力。然而，对于这种范例，没有一种成熟的软件开发方法，具有基于明确和数学上准确的行为标准的安全和安全保证。这给分布式基础设施的构建的正确性留下了不确定性。该奖学金的目的是为通信密集型并发和分布式应用程序的安全实施建立通用和实用的基础，建立在*多方会话类型*的一般理论基础上。分布式应用程序中的通信通常组织为多个结构化对话(*协议*)，其中开发人员或程序员希望强制执行系统行为的“可观察性”，以遵循协议给出的安全和安全标准。在这里，系统行为的“可观察性”是指具有更复杂信息的可见消息交换序列，例如数据的依赖性、安全信息、通信的成本和时间。在多方会话类型中，端点系统正确地履行其职责，从而使可观测系统的行为作为一个整体遵守商定的协议。多方会话类型清楚地表达了各自计算范例中的基本动态，从而作为建模、规范、验证、系统测试和认证的基础，并通过监视和逻辑断言等其他方法来增强。该奖学金旨在通过开展实验来实现多方会话类型作为通信类型的这一潜力。为了实现这一目标，已经确定了以下技术目标：1.基于行为理论和博弈语义，为捕获所有应用层协议的多方会话类型建立统一的类型理论，作为整个方法学的基础。建立了依赖和精化型的规范和验证理论；并基于自动机理论建立了可扩展的安全和安全属性验证算法。开发和发布基于(1，2)的开源工具链，并结合应用程序编程接口(API)和行业工具。一个理论上有充分依据的架构，可以有效地监控、跟踪、记录和执行正确的观测行为，以符合(3)中所写的规范。通过与学术和行业合作伙伴的合作，实现针对现实世界应用程序(包括多机器人/无人机、金融和医疗系统)的高级协议的正式安全和安保保证。通过研究计划，理论(1，2)和实践(3，4，5)之间的积极和广泛对话将是实现奖学金目标的关键推动因素，最终建立跨学科和共同创建的ICT研究。该项目还将基于会话类型的保证方法与云计算(云本地计算基金会)的标准化以及财务和电子医疗协议文档的公共监管要求联系起来，以满足人们对信息和通信技术核心的目标。

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.