Conversation-Based Governance for Distributed Systems by Multiparty Session Types

通过多方会话类型对分布式系统进行基于会话的治理

• 批准号: EP/K011715/1
• 负责人: Nobuko Yoshida
• 金额: $ 191.21万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2013
• 资助国家: 英国
• 起止时间: 2013 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FK011715%2F1
• 关键词: Conversation; Based; Governance; Distributed; Systems

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.

软件越来越有组织地以分布式通信流程为中心。在大规模的分布式计算平台中尤其如此，例如基于Web的流行服务的后端以及用于电子保健和电子科学的公共部门平台，这些平台通常提供社会的生命线。将应用程序组织为分布式组件的动态集合。该框架基于相互作用的过程，该过程扩展了传统的功能和对象范式，并允许软件组件的通用性和可扩展性组织更加广泛，可扩展的组织。在此类分布式系统中，确保安全性是一个至关重要的社会问题：许多平台都是长期以来的寿命，提供社会至关重要的服务，并提供至关重要的服务和收集安全敏感的数据；从临时服务中断到信息泄漏再到犯罪组织对安全脆弱性的开发，包括安全漏洞在内的安全违规行为可能会带来广泛的后果。但是，现有的保证方法基于对象和功能：没有建立正式保证方法以分布式系统而闻名。大规模的分布式计算基础设施就像成千上万人使用的摩天大楼一样，用于建造良好的结构工程原理，用作安全工程的基础。我们能否建立相应的工程原理，以构建对现代社会至关重要的软件摩天大楼？在这种背景下，该项目的核心目的是建立针对分布式系统的一般，正式的安全保证方法，我们称之为基于对话的治理。基于对话的治理始于用于捕获对话的高级类型，称为多方会话类型（MPST），最近由PIS引入并由研究人员进行了广泛的研究。在最新的理论结果和PIS与项目合作伙伴进行的持续合作的基础上，我们介绍了基于MPST的新开发和保证框架。 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整体是由于异质组件，因此只有动态验证和执行才能提供全面的安全保证。这是由于这种强调对话的运行时警务，我们称之为拟议的保证框架，基于对话的治理。该项目将通过以下任务来建立这种新方法：（1）开发编程语言 - 语言协议描述语言，称为cribble及其开源工具链，编程界面（API）和运行时间，并以统一类型的MPST理论进行支持。断言语言。 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以及针对未来IT基础设施和社会至关重要的分布式系统的一般安全保证方法的工具。

项目成果

Multicompatibility for Multiparty-Session Composition

多方会话组合的多重兼容性

• DOI: 10.1145/3610612.3610614
• 发表时间: 2023
• 作者: Barbanera F

Honesty by Typing

打字诚实

• DOI: 10.2168/lmcs-12(4:7)2016
• 发表时间: 2017
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Bartoletti M

Designing Asynchronous Multiparty Protocols with Crash-Stop Failures

设计具有紧急停止故障的异步多方协议

• DOI: 10.48550/arxiv.2305.06238
• 发表时间: 2023
• 作者: Barwell A

Choreographies in the wild

野外编舞

• DOI: 10.1016/j.scico.2014.11.015
• 发表时间: 2015
• 期刊: Science of Computer Programming
• 影响因子: 1.3
• 作者: Bartoletti M

Book review

书评

• DOI: 10.1016/j.artint.2019.103175
• 发表时间: 2019
• 期刊: Artificial Intelligence
• 影响因子: 14.4
• 作者: Halpern, Joseph Y.