Next Generation Protocols for Heterogeneous Systems

The classical computer security principle of the least common mechanism says that resource sharing creates security problems and should be treated carefully. This talk highlights that programming language runtimes that handle sensitive information at different confidentiality levels are such common mechanisms and, therefore, can inadvertently leak information. We examine runtime aspects such as schedulers and mailboxes and also study mitigating traffic analysis attacks using information flow techniques.

Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only were adopted for session types relatively recently – but exclusively for terminating languages. This talk scales logical relations to general recursive session types. It develops a logical relation for progress-sensitive noninterference (PSNI) for intuitionistic linear logic session types (ILLST), tackling the challenges non-termination and concurrency pose, and shows that logical equivalence is sound and complete with regard to closure of weak bisimilarity under parallel composition, using a biorthogonality argument. A distinguishing feature of the logical relation is its stratification with an observation index (as opposed to a step or unfolding index), a crucial shift to make the logical relation closed under parallel composition in a concurrent setting.

Secure multi-party computation permits evaluation of a function or a program on protected private inputs in such a way that the computation participants have no access to the data in the clear throughout the computation. The security guarantees are such that only the computation outcome becomes disclosed to the designated parties. In this talk, we discussed the setup, security definitions, and their differences from the properties of other definitions used in the programming languages community. The second part of the talk discussed PICCO, a compiler for transforming general-purpose programs intended to be executed on private data into the corresponding secure multi-party computation protocols. We discussed compiler optimizations and mechanisms for making it easier for programmers to develop efficient programs in this framework.

We sketch a novel approach to linear dependent session types based on a Proposition-as-Types foundation of session-based programs, which targets the development of a linear dependent type theory with equality types for session behaviour, allowing properties of linear objects to be expressed.

Noninterference guarantees that an attacker cannot infer secrets by interacting with a program. An information flow control type system asserts noninterference by tracking the level of information learned and disallowing leakage to entities of lesser or unrelated levels. These restrictions cater to scenarios in which the information learned by an entity monotonically increases with program progression but are at odds with control flow constructs, permitting interaction with entities of lower levels in the continuation. Relaxing such restrictions is particularly challenging in a concurrent setting. This paper utilizes session types to track the flow of information and develops an information flow control type system for message-passing concurrent processes that allows downgrading the pc for the next loop iteration upon recursion. To ensure noninterference, the type system relies on regrading policies, ensuring that any confidential information learned during the high-security parts of the loop cannot be rolled forward to the next iteration. To express regrading policies, the type system is complemented with integrity to ensure that entities with different regrading policies can be safely composed. The paper develops the type system and proves progress-sensitive noninterference for well-typed programs, ruling out timing attacks that exploit the relative order of messages. The type system has been implemented in a type checker, which supports security-polymorphic processes using local security theories.

The productivity of developers depends on the quality of the available programming languages: their support for adequate testing, for locating and fixing mistakes, and for maintenance tasks. If a programming language does not support these routine tasks, the developer is forced to resort to labor-intensive and ineffective workarounds. Put differently, it isn’t about the syntax, the types, or the semantics, but about the pragmatics of a programming language. The problem is that the PL research area has so far few tools to evaluate pragmatics.

The Rational Programmer is a new scientific instrument for that purpose. While simulations have a long history in computer science applications, the Rational Programmer method puts them to new use in PL research. The heart of the method is a simulation, namely an algorithmic abstraction of information gathering in a work context. The outcome of a rational programmer simulation is typically a strategy that a developer can employ. It may also point designers and researchers to a problematic aspect of a language. Finally, it can inform instructors how to teach students the effective use of a language. In this talk, I will demonstrate the workings of the Rational Programmer method with examples.

The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks.

Mailbox types are a novel behavioural type system for mailboxes first introduced for a process calculus by de’Liguoro and Padovani in 2018, which capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language design incorporating mailbox types, and describes an algorithmic type system. We make essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. Our algorithmic type system is necessarily co-contextual, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a prototype type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite.

Federated learning (FL) is a machine learning setting where clients keep the training data decentralised and collaboratively train a model either under the coordination of a central server (centralised FL) or in a peer-to-peer network (decentralised FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralised and a decentralised one, using the CSP process calculus and the PAT model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freeness (safety property) and successful termination (liveness property). The CSP models are constructed bottom-up by hand as a faithful representation of the real Python code and is automatically checked top-down by PAT.

Information-flow control is an important information-security–enforcement mechanism. It requires that secret information not be allowed to influence (or be used to compute) public data. This ensures that no private data will be leaked to the outside world. However, enforcing information-flow control in the concurrent world has proven incredibly difficult. The only known versions are incredibly restrictive. In current work, we are adding information-flow control to choreographic programs, where the extra restrictiveness is not necessary. In this talk, I will explain what goes wrong with information-flow control in concurrent settings, and why choreographic programming appears to rescue it.

Binary sessions, specifying bidirectional exchanges of messages between two processes, has widely been used to model idealised reliable communication, where messages are never dropped, duplicated, or arrive out of order. Such sessions allow for sophisticated protocol structures, as evidenced by the ever expanding work on session types, a behavioural type system for specifying the types of individual messages of a sequence of exchanges. However, the expressivity of session types is often restricted to a decidable fragment, which prohibits them from reasoning about functional correctness.

In this tool presentation, I present the ongoing story of Actris tool – a framework for session type-based reasoning in separation logic – and how it can be used to reason about reliable communication. In particular, I demonstrate the full verification of a suite of programs that combine message passing and shared memory concurrency. I additionally briefly cover the various extensions of Actris; notably how it has been applied to the verification of distributed systems and deadlock freedom.

This talk gives an introduction to the “logical approach” to proving type safety. I will first present a simple version, and then scale up to a small session-typed language. I will show that this approach is well-suited for mechanization of challenging type systems in the Coq proof assistant

In this work we formalise an existing system for high-availability industry automation: the constraint that availability must be maximised – even at the cost of strong consistency – poses some interesting challenges. The basis is given by the peer-to-peer, uncoordinated, but causality-preserving event log replication of the Actyx middleware. Our work resulted in well-formedness constraints that ensure that a designed interaction protocol will achieve eventual consensus on the event trace of its execution, without any need for further coordination. This holds even in a dynamic swarm setting, where any role can be replicated any number of times and new participants can join and leave the system at any time.

Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. In this talk we present the first theory of choreographic programming language that incorporates probabilistic aspects for local computation, choreographic choice, and scheduling. We start from an established theory of choreographic programming [1, 2, 3, 4, 5] and integrate various probabilistic features while maintaining the original syntax. We show that the original compilation procedure can still be used and establish its correctness in terms of probabilistic bisimilarity via standard up-to techniques. We discuss how the various probabilistic features impact the design of the semantics and the lessons learned while integrating them.

During this break-out session, the discussion focused on the following points: state of the art in information flow control, quantitative information flow and its connection to secure multi-party computation, modern formulation of noninterference policies using the epistemic (knowledge-based) framework for declassification, and comparison of different noninterference theorem statements.

During the session, we discussed the security definitions employed in the secure multi-party computation literature, properties of the resulting protocols, and their relationship to the definitions and properties achieved in other settings, e.g., in information flow control literature. Because the model provides powerful guarantees at the level of individual operations, it becomes possible to achieve properties which otherwise would be difficult to achieve in other settings. For example, the fact that a computation participant does not see private values implies that the participant is unable to leak secret data. During the discussion we were also seeking connections with other PL concepts and recent developments as a way to build a fruitful collaboration. Topics that came up include concurrency, information flow, and orchestration.

This breakout session gathered people currently employing the advanced proof method of logical relations and people interested in learning more about it. Of particular concern was the recent developments that employ logical relations in a session-typed concurrent setting. As such the session allowed experts to provide an overview of the current state of the art and latest achievements. A significant portion of the discussion focused on recent logical relations for session types that are indexed not only with a single type, but a set of types. These relations are necessitated by program equivalence statements such as noninterference, demanding observations along possibly several channels. The question came up whether such relations would also support proofs of free theorems in a linear setting based on a parametricity argument.

• $\mathrm{■}$

  Why were attendees interested real-world applications?

  • –

    Understanding how behavioural types can help with real-world projects and what is missing

  • –

    Justifying need for research in grant proposals

• $\mathrm{■}$

  Some problems/examples for behavioural types

  • –

    JEDIS bug (Java implementation of REDIS): was still trying to use a socket even though an exception was thrown before

  • –

    tsunami prediction project

• $\mathrm{■}$

  More first-hand experiences

  • –

    Racket contracts that only specify functional correctness and do not capture artificially introduced bugs in code; common issue that model is not expressive enough; need for specifying protocols

  • –

    Erlang typing for gen_server: practically driven, challenges with failures, gradual typing

• $\mathrm{■}$

  Practical problems with evaluation

  • –

    How to set up experiments?

  • –

    What are target measures? How does one show that number of bugs reduce when using behavioural types?

  • –

    Getting companies interested in pilot projects

• $\mathrm{■}$

  Industrial collaborations

  • –

    often different interests than research: small steps are enough and there is little theoretical work needed to support this

  • –

    actual porting from theoretical work to practice is a lot of work and proves only worth it if something is found (risky for PhD projects)

  • –

    wish for push-bottom technology (e.g. Bedrock systems but fine with writing specifications)

  • –

    issue that universities seem to focus quite a bit on funding opportunities with such collaborations rather than research content (tone down probably?)

• $\mathrm{■}$

  Possibilities for case studies/collaborations with more applied domains, even in CS

  • –

    it is likely that computing-heavy have software that suffers from issues BT solve

  • –

    hospitals as part of universities: problem with data-privacy and training that is needed

  • –

    IOT and intermittent computing

A large barrier to the widespread adoption of behavioural typing disciplines is that we must, at present, select a single tool and write our entire system using that tool. In practice at the very least we want to be able to design our system to make use of different components that use different, but not completely unrelated, behavioural type disciplines and tools (for example, having part of the system able to statically verify data constraints using refinement types, and another part of the system be able to check this using some form of monitoring).

There has been some work on runtime monitoring against local session types, but at present the results there only state that an invalid incoming message was dropped. There was a desire to go further than this, for example reporting failures, requesting message re-sends / reporting rejections to senders, or perhaps doing some message reordering.

Two related topics arose out of the discussion.

The first was a language design issue: what language features should our tools, at a minimum, support in order to allow interoperability? We thought that some way of handling failures (e.g., through exceptions) was probably important in this regard, although sometimes challenging to integrate into tools.

The second issue was about reconciling compatible yet subtly-different protocols, and a paper by Dezani et al. on session isomorphisms seemed important here. There was an extensive discussion about the notion of some sort of intermediate representation that could be used to implement adapters that can for example reorder messages and manipulate data sent along the wire in order to realise these transformations in practice in a uniform way.

We hope to write a position paper for PLACES in the coming weeks.

Why probabilistic behavioural types?

Emilio: the answer is not obvious. My coauthors and I started working on them as a specification of a desired probabilistic process behaviour, that we use for monitoring https://doi.org/10.1016/j.scico.2022.102847,https://doi.org/10.1007/978-3-030-78142-2_7. I also have a work on probabilistic analysis of session types https://doi.org/10.4230/LIPIcs.CONCUR.2020.14.

Silvia Ghilezan: my interest comes from the connection between probabilistic lambda calculus and probabilistic logic

Emanuele D’Osualdo: my interest comes from my work on hyperproperties, I would like to look at systems that are probabilistic in nature

Jorge Perez: I am not sure I understand the meaning of probabilistic session types. Even if we have a probabilistic calculus (like e.g. probabilistic pi-calculus) what do we gain by putting probabilities in types?

Nobuko Yoshida: I am interested in understanding how to encode probabilistic lambda calculus in a session typed calculus, and it seems we need probabilistic (multiparty) session types

Marco Peressotti: My main motivation is understand how to extend choreographic programming to express and reason about randomness (e.g., randomness in algorithms, in the underlying communication model etc.) and eventually quantum protocols.

Kirstin Peters: I have both practical interest and quantum systems, which have probabilistic LTSs. We may use probabilistic session types to check that e.g. a program deadlocks with a certain probability.

Alceste Scalas: I share Jorge’s doubts (in fact I have only worked on probabilistic session types as specifications for for run-time onitoring, with Emilio et al). I have a bit of difficulty in seeing the “killer application” where putting probabilities in a session type gives you a clearly useful verification technique that may not be achieved using other analysis techniques for probabilistic programs.

Marco Carbone: I am also looking for applications that would clarify my understanding, like Jorge and Alceste Applications of probabilistic session types.

Emilio: Ugo dal Lago’s paper uses probabilistic session types for modelling ‘cyptographic experiments: https://doi.org/10.4230/LIPIcs.CONCUR.2022.37.

Marco Peressotti: Self-stabilising algorithms may also be a field of application

Marco Carbone: Tools like Prism allow for writing models with probabilities, but some models cannot be model-checked due to the state explosion problem. Could a type discipline like probabilistic session types help?

Nobuko Yoshida, Kirstin Peters, Marco Carbone, Marco Peressotti, Emilio Tuosto: we could look at probabilistic CCS examples, probabilistic dining philosophers, and see how probabilistic session types could allow e.g. to abstract and reduce the state space while still deriving useful probabilistic information (e.g. discarding low-probability events that may not relevantly impact the result). Probabilistic behavioural types could reduce the amount of concurrency to verify, and speed up the verification. Kirstin Peters has related work on the topic https://doi.org/10.1007/978-3-030-32505-3_12.

Jorge: on the topic of session-based execution optimisation, there is also related work by Luis Caires and Bernardo Toninho at ESOP 2024. Still, it is not clear whether bringing these optimisations in a probabilistic setting (e.g. to optimise analysis against PRISM model checking) would require probability annotations, maybe just having session-structured interaction is enough We discuss a leader election protocol modelled in PRISM, and the properties that are verified (e.g. leader eventually elected with probability 1), and queries (i.e. computing the probability that a property eventually holds).

Everyone: the most popular probabilistic functional programming system should be Anglican https://probprog.github.io/anglican/. Recent work on quantum computing: https://doi.org/10.1145/3632885.

Emanuele: there are works proposing type systems for compositional abstraction for reasoning about the privacy of programs, with programs able to add noise to the computation (with some given probability annotations). eg https://doi.org/10.1145/3009837.3009884. We may do something similar for concurrency, e.g. prove that deadlocks may happen or not with some probability, depending on some probabilistic information.

Kirstin Peters: I see two lines: Adding probabilities to session types: do we gain anything from it? Take a program LTS with probabilities as input, but session types have no probabilities (a bit like probabilistic lambda calculus): how would it work?

Emilio: what if you put probabilities on the payload carried by messages? E.g. I may send an integer with probability p, or a string with probability 1-p? Can we get something?

Jorge, Alceste: mention work by Padovani at al. on fair termination; uses non-deterministic choices, what if they are probabilistic? Emanuele believes that even in this case it may not be necessary to annotate types with probabilities (or probability intervals) to achieve probabilistic results, because e.g. the work on probabilistic privacy does not do it.

Jesper: defining a logic into a proof assistant is hard. Because of adequacy.

Again: depending on what you need to do, you need to pick the right proof assistant and techniques

Binders seem to be the main issue. Robert: avoid binders, but not clear how.

Discussion on nominal => Jesper thinks it’s by far the best way to deal with binders, if a deep embedding is the goal.

Luis: why hard in pi-calculus and easy in lambda. Coq can do it for you. In a functional language.

Ok, they are talking about embedding, deep vs shallow. This can make a difference.

- Deep embedding, hard.

- Shallow embedding.

==> Design a framework for working on session type mechanisation. Using Iris as an example.

Luis: the use of binders is different from pi to lambda. Substitution: names for names only.

Jesper & Kirstin: use nominal for deep embedding.

Robbert explains shallow vs deep. A shallow embedding allows to make the language modular (you can add new stuff).

Jesper: use nominal!

Kirstin: there is a need to reach out to people who are not expert.

Robbert: mechanise for confidence and mechanise for improving the proof assistant.

Jonas: having tutorial material.

Message: write about experiences, people can reuse it.

Ideally we should have a framework where to mechanise behavioural types (and linear stuff).

Robbert: If you want to build something more traditional, then somebody needs to make an effort, and perhaps nominal is a good way of doing it. There is also the Iris approach (shallow embedding) – this is great but (Kirstin says) it is hard to use (given the decoupling from syntax). (Kirstin says) An explanation of how the embedding allows to model Process calculi and about the advantages in proving in combination with a tutorial for how to get things working might allow also non-experts maybe without an understanding of the relation to logic to use this framework.

Robbert: third approach, intrinsic typing – (Agda?)

Alceste: Concurrency benchmark.

Ralf: The benchmark is excluding semantic approaches (like logical relations).

Introduction round: what do we want out of the session?

• $\mathrm{■}$

  session types are important (send number $N$, followed by N messages where $N=5$)

• $\mathrm{■}$

  systems: level-dependent session types, Actris

• $\mathrm{■}$

  refinement types: not allowing the highest bidder to bid again until a yet higher bid has been submitted

• $\mathrm{■}$

  what are dependent types in the context of session types? type families? type-level computation? indexed types?

• $\mathrm{■}$

  dependent types are functions from values to types, where values should be behaviours (which can encode arbitrary data)

• $\mathrm{■}$

  should you be able to depend on messages that you haven’t observed?

• $\mathrm{■}$

  tracking dependency structures in multi-party sessions is non-trivial (it is intuitive in binary sessions, however)

• $\mathrm{■}$

  logistics auction: only the winning participant can continue the process after the auction

Example discussion:

• $\mathrm{■}$

  Simon: sending JSON, not labels

  • –

    Actris can do this by using Coq “if/else” on the type-level

• $\mathrm{■}$

  Roland: factory logistics bidding

  • –

    Brigitte proposes «Message-aware session types» (ESOP24) as a possible solution

  • –

    importantly, the continuation may depend on what messages the process got from other channels prior

• $\mathrm{■}$

  Jonas: round-trip example ($A\to B\to C\to A$)

  • –

    bind variable x on the first send, then refer to it for the other sends to ensure that all send the same value

  • –

    the problem is that $B\to C$ has a binder (by duality) at B, but none at C

  • –

    solution might be to trace who will learn of the value and permit those roles to have binders when they receive it

  • –

    even more complicated is when only a location is sent around pointing to a linear resource

  • –

    the setting here specifically is that the global type is not known, the endpoint types are known and need to be combined to figure out whether the composition is well-typed (basically recovering a global type)