Conversation-Based Governance for Distributed Systems by Multiparty Session Types

软件越来越多地以分布式通信过程为中心进行组织。在大型分布式计算平台中尤其如此，例如流行的基于web的服务的后端以及电子医疗保健和电子科学的公共部门平台，这些平台通常提供社会的生命线。应用程序被组织为分布式组件的动态集合。该框架基于交互过程，它扩展了传统的函数和对象范例，并允许更通用和可扩展的软件组件组织。确保这种分布式系统的安全是一个重要的社会问题：许多平台是长期存在的，提供对社会至关重要的服务，并收集安全敏感的数据；违反安全规定，包括违反安全规定，可能会产生广泛的后果，从暂时的服务中断到信息泄露，再到犯罪组织利用安全漏洞。然而，现有的保证方法是基于对象和功能的：对于分布式系统来说，还没有建立好的正式保证方法。大规模的分布式计算基础设施就像成千上万人使用的摩天大楼，在建筑中，完善的结构工程原理被用作安全工程的基础。我们能否建立相应的工程原则来建造对现代社会至关重要的软件摩天大楼？在此背景下，该项目的中心目标是为分布式系统建立一个通用的、正式的、基于安全保证的方法，我们称之为基于对话的治理。基于会话的治理从捕获会话的高级类型开始，称为多方会话类型（mpst），最近由pi引入并被研究人员广泛研究。基于最新的理论成果和pi与项目伙伴的持续合作，我们介绍了基于MPSTs的新开发和保证框架。我们方法的核心是一种高级的、与编程语言无关的、基于mpst的声明性协议描述语言。该框架中的安全保证是通过根据该协议语言的正式规范对分布式组件进行验证来实现的，这些验证可以静态地（在开发时）执行，也可以动态地（在运行时）执行，其中我们强调后者：由于诸如异构组件等原因，大规模分布式系统作为一个整体很少适用于静态验证，因此只有动态验证和强制执行才能提供全面的安全保证。正是由于这种对会话的运行时监管的强调，我们将建议的保证框架称为基于会话的治理。该项目将通过以下任务建立这种新的方法论：(1)开发一种与编程语言无关的协议描述语言，称为Scribble，以及它的开源工具链、编程接口（api）和运行时，并以mpst的统一类型理论为支持。(2)开发一种断言语言，用于指定和验证作为协议精细化的精细安全属性，以及与断言语言相关联的策略语言。由pi演算理论支持的分散监控提供了高效、可扩展的运行时验证和执行。(3)通过与项目合作伙伴的协作进行大规模实验，实现对现实世界应用的正式安全保障，包括全球网络基础设施、企业软件和消息中间件。在整个项目中，将进行理论与实践之间的广泛对话，为分布式系统的一般安全保证方法提供真正有效的原则和工具，这对未来的IT基础设施和社会至关重要。

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.