POST: Protocols, Observabilities and Session Types

通信不仅是新兴的大规模分布式应用（如电子商务、电子科学、电子医疗和金融技术）的基本组织原则，也是使用计算资源（如微服务和多核芯片）的有效方式。在这个新范例中，通信和并发性是软件开发中的规范，而不是次要的问题，这使得架构师和程序员能够利用成百上千的并发进程通过“消息传递”进行交互。然而，对于这种范例来说，没有一种行之有效的软件开发方法，可以根据其行为的清晰和精确的数学标准来保证安全性。这就给分布式基础设施构建的正确性留下了不确定性。该奖学金的目的是建立在多方会话类型的一般理论基础上，为通信密集型并发和分布式应用程序的安全执行建立一般和实际的基础。分布式应用程序中的通信通常被组织成多个结构化的会话（协议），其中开发人员或程序员希望强制执行系统行为的“可观察性”，以遵循协议给出的安全和保障标准。这里，系统行为的“可观察性”是指与更复杂的信息（如数据依赖性、安全信息、通信成本和时间）进行的消息交换的可见序列。在多方会话类型中，端点系统适当地执行其职责，以便可观察的系统行为作为一个整体遵守商定的协议。多方会话类型阐明了各自计算范式中的基本动态，因此作为建模、规范、验证、系统测试和认证的基础，并通过监视和逻辑断言等其他方法得到增强。该研究金旨在通过开展实验，发挥多方会议类型作为交流类型的潜力。为实现这一目标，确定了以下技术目标：建立基于行为理论和博弈语义的多方会话类型的统一类型理论，捕获全范围的应用层协议，作为整个方法论的基础。建立依赖和细化型理论的规范和验证；并提出了一种基于自动机理论的可扩展安全性能验证算法。基于（1,2），结合应用程序编程接口（API）和行业工具的开源工具链的开发和发布。一个理论上建立良好的架构，可以有效地监控、跟踪、记录和执行正确的观察行为，以符合(3).5中所写的规范。通过与学术和行业合作伙伴的合作进行实验，实现针对现实世界应用（包括多机器人/无人机、金融和医疗保健系统）先进协议的正式安全和安全保证。在整个研究计划中，理论（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.