Conversation-Based Governance for Distributed Systems by Multiparty Session Types

软件越来越多地以分布式通信过程为中心进行组织。在大型分布式计算平台中尤其如此，例如流行的基于网络的服务的后端，以及用于电子医疗和电子科学的公共部门平台，这些平台往往提供社会生命线。应用程序被组织为分布式组件的动态集合。该框架基于交互过程，它扩展了传统的功能和对象范例，并允许对软件组件进行更多用途和可扩展的组织。确保此类分布式系统的安全性是一个至关重要的社会问题：许多平台寿命长，提供社会关键服务，并收集安全敏感数据；安全违规行为，包括安全漏洞，可能会产生广泛的后果，从临时服务中断到信息泄露，再到犯罪组织利用安全漏洞。然而，现有的保证方法是基于对象和功能的：对于分布式系统，还没有公认的良好的正式保证方法。大规模的分布式计算基础设施就像是成千上万人使用的摩天大楼，对于这些摩天大楼，人们使用成熟的结构工程原理作为安全工程的基础。我们能为构建对现代社会至关重要的软件摩天大楼建立相应的工程原则吗？在这种背景下，本项目的中心目标是为分布式系统建立一种通用的、基于形式的安全保证方法，我们称之为基于会话的治理。基于会话的治理始于捕获会话的高级类型，称为多方会话类型(MPST)，最近由PI引入并被研究人员广泛研究。基于最新的理论成果和PIS与项目合作伙伴的持续合作，我们介绍了基于MPST的新的开发和保证框架。该方法的核心是一种高级的、与编程语言无关的基于MPST的声明性协议描述语言。该框架中的安全保证是通过根据该协议语言的形式规范对分布式组件进行静态(在开发时)或动态(在运行时)执行的验证来实现的，其中我们强调后者：由于组件的异构性，大规模分布式系统很少作为一个整体服从静态验证，因此只有动态验证和执行才能提供全面的安全保证。正是由于这种对会话的运行时策略的强调，我们将提议的保证框架称为基于会话的治理。该项目将通过以下任务建立这一新的方法：(1)开发一种与编程语言无关的协议描述语言，称为Scribble，及其开源工具链、编程接口(API)和运行时，并以MPST的统一类型理论为后盾。(2)开发一种用于指定和验证作为协议精细化的安全属性的断言语言，以及与断言语言链接的策略语言。(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.