Florian Vanhems

Narjes Jomaa

Samuel Hym

David Nowak

On the Proof-Oriented Design of a Context-Switching Service in the Pip Protokernel

The Pip protokernel is a kernel whose trusted computing base is reduced to its bare bones. The goal of such minimisation is twofold: reduce the attack surface and reduce the cost of the formal proof of security. In particular, multiplexing is not implemented in the kernel but in a partition whose code is executed in user mode. This of course assumes that the kernel provides minimal services dedicated to signal sending. In this paper, we describe a streamlined service designed to allow for inter-partition communication through userland structures that mimic the traditional Interrupt Descriptor Table .

Introduction

Control flow transfer mechanisms are vital components of a system. Transfers occur thousands of times a second in our modern computers. Providing a robustand efficient -control flow transfer mechanism is therefore paramount in most systems. Yet, numerous software attacks targeting the execution flow exist, notably through memory corruption (use-after-free, buffer overflow, heap overflow, etc.). Formally proving that no illegal accesses are made to the system's memory is a strong protection against those attacks. Pip is a one-of-a-kind kernel that provides formally proven memory isolation. In this paper, we report on the design of Pip's control flow transfer service. Related work seL4 [START_REF] Klein | seL4: Formal verification of an OS kernel[END_REF] is the world's first formally verified general usage microkernel. It provides virtual memory management, thread scheduling, inter-process communication and access control. Whereas in the case of the Pip protokernel those last two features are to be implemented in userland. CertiKOS [START_REF] Gu | CertiKOS: An extensible architecture for building certified concurrent OS kernels[END_REF] provides a certified programming method to formally develop kernels in Coq, targeting an extension of CompCert Clight and assembly code. It has been used to prove noninterference results [START_REF] Costanzo | End-to-end verification of information-flow security for C and assembly programs[END_REF]. Prosper [START_REF] Dam | Formal verification of information flow security for a simple ARMbased separation kernel[END_REF] is a separation kernel that supports dataflow functionalities of the ARMv7 processor, including interpartition communication, scheduling. Security properties have been proved in HOL4. Bisimulation is used to carry higher-level proofs, based on an abstract model including communication channels, over to a concrete one based on an intermediate language that represents the ARM instruction set [START_REF] Fox | A trustworthy monadic formalization of the armv7 instruction set architecture[END_REF]. The security property about the communication between isolated entities is the goal of formal verification. This information flow property [START_REF] Goguen | Security policies and security models[END_REF] is verified at the binary code level using HOL4. In [START_REF] Ni | Using XCAP to certify realistic systems code: Machine context management[END_REF], the theoretical verification framework XCAP is used to formally verify a realistic x86 implementation of machine context management.

Outline This paper is structured as follows. First, in Section 2, we give an overview of the Pip protokernel and its security properties. Then, in Section 3, we describe how we designed the context switching service and provide some insight on how this service is meant to be used. We focus in Section 4 on the formal proof of security and the impact of our context switching mechanism on it. Finally, we illustrate in Section 5 the usability of this context-switching service.

About the Pip protokernel

Pip's philosophy

Pip is a minimal operating system kernel where the minimisation of its size is motivated by the reduction of both the cost of proof and the attack surface, while allowing for efficiency and usability. The code of Pip is written in Gallina (the language of the Coq proof assistant). More precisely, we restrict ourselves to a monadic code that allows for a word-for-word translation into C code.

The primary goal of Pip is to provide memory isolation to applications that run inside memory partitions (that we simply call partitions). At boot, Pip creates a single partition congregating the system's whole memory, called the root partition. At any time, a partition can decide to create another partition. We refer to the newly created partition as a child of the first partition, while we refer to the first partition as the parent of the new partition. In order to create a child partition, a parent has to share a part of its own memory, and provide it to its child. The memory shared this way is accessible to both the child and its parent, except for a tiny amount requisitioned by Pip to maintain its internal structures. The memory requisitioned by Pip is no longer accessible to any of the partitions.

These parent-child relation between the partitions create a partition hierarchy called partition tree. Fig. 1 shows a partition tree where P root is the root partition, that has P 1 and P 2 as children partitions. In a partition tree, we say that two partitions are incomparable if none of them is an ancestor of the other. For example in Fig. 1 Note that only Pip's code is allowed to run in kernelland. Any other piece of code (such as the code of a partition) runs in userland, with no privilege.

Pip's security properties

Significant works were carried out to formalise security properties that should be ensured by operating systems [START_REF] Rushby | The design and verification of secure systems[END_REF], [START_REF] Rushby | A trusted computing base for embedded systems[END_REF]. This includes the isolation between applications as well as controlling the communications between them. Therefore, a first step in this verification process is to require a concise definition of the security properties and to identify hardware and software components on which these properties are founded. In this context, we are interested in the memory isolation property. This property ensures that an application cannot illegally access the memory of another application, nor the kernel's. We consider it the most fundamental security property, because it allows to prove several other security properties such as ensuring the security of communication between processes. We decomposed the isolation property into four lesser properties described below.

Kernel isolation This property mainly defines the isolation of the kernel's data and code from unauthorised access that may occur from userland. In our case, this property is based on memory partitioning. Memory configuration is performed by the kernel and user accesses are controlled by the hardware component MMU (Memory Management Unit).

Horizontal isolation This property states isolation between incomparable partitions (see definition and example at Sec. 2.1). It guarantees that the configuration of the address space of a partition does not allow it to access the physical memory of another incomparable partition. Like the previous one, this property relies on the MMU to control user accesses.

Vertical sharing This property ensures that all pages of a partition are a subset of its parent pages and (recursively) of its ancestors in the partition tree. It is important to manage the hierarchical model of the TCB where the security of a partition relies on the security of its ancestors.

Internal consistency This property states that informations stored in the kernel structures are consistent with the current state of the memory. For example, these structures include the configuration of the MMU for each partition.

Designing Pip's control flow service

We will further refer to the context switching service as switch. Pip's philosophy is to reduce the TCB to a strict minimum. Pushing the microkernel, then exokernel philosophy further, Pip throws multiplexing outside of the kernel. This allows for a lighter proof cost as well as a tighter attack surface [START_REF] Jomaa | Prooforiented design of a separation kernel with minimal trus ted computing base[END_REF].

As such, Pip's sole concern about hardware interrupts is to forward them to the root partition, which will assume the multiplexer's role and process them as it sees fit. In case of a software interrupt, Pip will handle it only if it is a call to one of its own services. It will otherwise forward it to the parent of the caller and pass the execution flow.

It becomes obvious that Pip needs to provide a way for multiplexers -and generally every partition -to send signals to each other, and that partitions should be able to process these signals their own way. This is semantically close to software interrupts, but each partition should be able to configure its interrupt handlers independently from one another. It follows that a per-partition structure is required to hold the configuration. We decided that switch would be built on this observation.

VIDT and contexts

switch uses a structure called "Virtual Interrupt Descriptor Table " (VIDT). This structure lives in userland, in the partition's virtual address space, to allow partitions to manipulate it at will. The VIDT holds pointers to CPU states (mainly snapshots of the CPU registers) that we call contexts. These contexts are stored in the partition's own memory. Each interrupt number is associated to a context as seen on Fig. In order to pass the execution flow from a partition A to another partition B, switch first creates a context out of partition A's CPU state, and stores it inside partition A's virtual IDT. Next, it switches to the memory space of partition B by modifying the page table root register (CR3) which is stored inside Pip's structures. Last, it restores a context from partition B's VIDT, and lets partition B resume its execution.

Pointers and contexts living in userland implies that some partitions may try to alter them. Even though, partitions can not use this ability to threaten Pip's security measures, if Pip carefully checks the data it uses from the partitions. Those checks include verifying that some pages are accessible to the memory partition, that the pointers Pip dereferences actually points inside the partition, etc. On another side, we do not need to check the "validity" of the contexts we restore, as they would run in user mode. Any illegal access to the memory would be prevented by the MMU, generating a fault.

However, we did find a way to circumvent Pip isolation properties if those checks were not thoroughly made; we will further discuss this in Sec. 4.

Calling switch

In this section, we review the different arguments required to call switch, in order to highlight parts of its behaviour.

The caller must first indicate the partition it wants to call. In order to do so, Pip provides a structure called partition descriptor, that lives in kernelland. The partition descriptor's address is returned by Pip at creation time, allowing the parent to further refer to its newly created child. The caller hence uses the partition's descriptor virtual address (in its virtual address space) to refer to its callee. This is fine if the callee is any of its child, as their accessible memory resides in the caller's addressing space by design (although the memory requisitioned by Pip is not accessible anymore). On the contrary, a caller has no way to refer to any of its ancestors through an address since its ancestor's partition descriptors are stored outside of its virtual memory (it would otherwise break Pip's recursive tree structure, thus breaking invariants required by the isolation property). That is why we set a particular address (an address that cannot be used as a partition descriptor for a child) to allow a partition to send an interrupt to its parent. We call that particular address the default address.

Second, the caller partition must provide the interrupt number it wants to send to the callee. Being able to choose from different interrupt numbers allows a partition to have multiple entrypoints, allowing it to declare specific handlers for specific situations.

Third, it must declare an interrupt number to associate its current context with. That context will be restored whenever said associated service is called. The partition only has to provide an interrupt number. Pip will then read the address located at the corresponding index in the VIDT, and then save the context at this address, as seen on Fig. If the address is invalid (for example if some part of the context would be written out of the partition's accessible memory), Pip will cancel the call and throw an error to the caller. If the partition wants its context to be dropped, it can provide an unused interrupt number, where the default address is written. In that case Pip will skip saving the partition's context and will not throw an error.

Context write location

Fourth, Pip provides a way for partitions to ignore specific interrupts. This allows partitions that do not implement some interrupt handlers to ignore the associated interrupts. It can also be used by partitions to ensure they are not called on specific handlers when being in an unstable state. There are two sets of flags to provide when calling Pip. The first ones are applied to the caller if the execution flow transfer is to be successful. These flags are applied until Pip restores one of the caller's contexts. The second ones are only useful if the caller chose to save its context. In that case, these flags will be inserted in its current context, and restored whenever the context is loaded again. These flags are applied atomically, which means they are effective as soon as Pip did transfer the execution flow. This is akin to the hardware features an OS kernel uses when it needs to ensure atomicity of sequences of instructions (by blocking interrupts for some time).

Impact on Pip's isolation properties

Pip's fundamental security properties. The isolation proof of switch remains to be written. We can only give some insight, but we believe there will be no major obstacle to the isolation's proof. Indeed, this service does not deal with Pip's internal structures, as opposed to Pip's other services. We briefly explained in Section 2.2 what are Pip's isolation properties, and are going to provide arguments on why we believe this service does not break these properties.

While switch needs to access kernel structures to translate the partition's addresses, it does not tinker with them in any way. The service sometimes has to write in memory, but it only does so inside its caller's accessible memory. Moreover, the kernel isolation property assures that -before the service execution -the partition's accessible memory is disjoint to Pip's memory. That implies that structures tracking memory partitioning remain untouched during the service's execution, therefore making the whole set of properties trivial to prove (once we proved that Pip only writes in userland).

Extending Pip's isolation properties. This section will focus on security aspects that are not covered by Pip's fundamental security properties. As pointed out in Section 3.1, without the proper checks, a malicious partition's code could use Pip to read into protected memory.

By making a child's handler context point into kernel pages, and calling that handler, the malicious partition would make Pip load part of its kernel pages as if it were a context. This would most certainly make the child's partition fault, and Pip would dump the faulting context to the child's VIDT (this dumping mechanism is provided by Pip, and is required to let parents handle expected faultssuch as stack overflows -from their children). This would allow the malicious parent to retrieve the faulting context, thus reading parts of the kernel's memory. This particular setup is pictured on Fig. 4.

However, this does not break any of Pip's fundamental properties, as this particular attack does not involve configuration pages. It has been shown that those fundamental properties imply some basic information flow properties [START_REF] Jomaa | Prooforiented design of a separation kernel with minimal trus ted computing base[END_REF]. We do not want them to be too rigid because each partition should be able to enforce the information flow policy for itself and its descendants. But still, this particular example suggests that we should prove a new security property stating that each address a service dereferences from a partition's accessible memory needs to point to that same partition's accessible memory (beside the eventual default values for which Pip acts differently). This property did not appear when dealing with the other

Application to the real world

This section will illustrate how this service can be used with a real world example. We will illustrate how a Linux partition can use Pip to notify a server process that it should close.

Let's assume we have a Linux partition somewhere in Pip's partition tree, and that Linux has spawned processes which are inside their own partitions, including the aforementioned server. Linux uses Pip's VIDT structure to register its system calls, and most notably the exit() system call. The server is configured to handle SIGINT signals.

The setup is pictured on Fig. 5.

Lightweight Server

Linux Linux sends a SIGINT signal Server calls exit() The model allows for whatever semantic you'd like behind each interrupt, so let's arbitrarily pretend Linux chose interrupt 0xA3 to signal a SIGINT and interrupt 0xB7 to handle an exit() syscall.

Linux calls Pip with the server's partition descriptor and interrupt number 0xA3 (in this example, flag arguments have no influence whatsoever, they'll be omitted). Pip performs the checks described in Section 3.1, and loads the server's context associated with the 0xA3 interrupt.

Note that the server may have disabled this interrupt through the flags, for whatever reason. Let's assume this is not the case, that the interrupt is not masked and a proper context has been set up to handle the situation correctly. The server's handler does its housekeeping, closing incoming connections and preparing it for deletion. Once it's done, the handler calls Linux's system call exit() to notify its termination. It provides Pip with the default address (to notify its parent), interrupt number 0xB7 (here flags don't matter neither). Once again we suppose that Linux was set up to let this happen.

Linux's context associated with interrupt 0xB7 is hence loaded. Linux then proceeds with the deletion of the process' partition and collects its memory.

Conclusions

In this paper we have described a kernel service designed to allow memory isolated processes to communicate through signals. It follows Pip's philosophy as it only provides for the code that must run in kernelland. Anything else, such as a multiplexer, is implemented efficiently in userland by relying on Pip services. We have argued that Pip's fundamental security properties are preserved by the discussed service and that it can be (and will be) formally proved in Coq without any obstacle. We have also noticed that the specificity of system call require an additional information-flow security property.

P 2 and P 1 . 1

 11 are incomparable.

Figure 2 .

 2 Figure 2. A partition VIDT and its pointers to contexts

Figure 3 .

 3 Figure 3. Pip saving a context in the caller's memory

4 .

 4 Pip loads the memory pointed by the handler's pointer 6. Pip dumps the faulting context to the Child's VIDT, and returns to the parent 5. Pip data context is loaded, Child partition faults

Figure 4 .

 4 Figure 4. A partition reading Pip's supposedly inaccessible data

Figure 5 .

 5 Figure 5. Linux sending a signal to a lightweight server


Jérémie Bettinelli
email: jeremie.bettinelli@normalesup.org.

Convergence of uniform noncrossing partitions toward the Brownian triangulation

Keywords: noncrossing partition, noncrossing pair partition, lamination, Brownian triangulation, Brownian excursion, Dyck path

We give a short proof that a uniform noncrossing partition of the regular ngon weakly converges toward Aldous's Brownian triangulation of the disk, in the sense of the Hausdorff topology. This result was first obtained by Curien & Kortchemski, using a more complicated encoding. Thanks to a result of Marchal on strong convergence of Dyck paths toward the Brownian excursion, we furthermore give an algorithm that allows to recursively construct a sequence of uniform noncrossing partitions for which the previous convergence holds almost surely.

In addition, we also treat the case of uniform noncrossing pair partitions of even-sided polygons.

Introduction

Configurations of noncrossing diagonals of a regular polygon have been the focus of many studies, from a geometrical, from an enumerative and from a probabilistic point of view. Various natural models have been studied (see for instance [3] and the references therein). Among these models, noncrossing partitions are of particular interest as they bear many applications in a wide range of areas; see for instance [START_REF] Mccammond | Noncrossing partitions in surprising locations[END_REF] for a survey of the topic.

We denote by P n the regular n-gon of the complex plane with vertex coordinates ω k n := e 2iπk/n , k ∈ {0, 1, . . . , n -1}. A noncrossing partition of P n is a partition of the set {ω 0 n , . . . , ω n-1 n } such that the convex hulls of its blocks are pairwise disjoint; a noncrossing pair partition of P n is a noncrossing partition of P n whose blocks are all of size exactly 2 (see Figure 1). Note that the latter only exists for even values of n.

A (geodesic) lamination is a closed subset of the unit disk D := z ∈ C : |z| ≤ 1 that can be expressed as a union of chords whose intersections with the open unit disk D are pairwise disjoint. For two complex numbers z, z , we denote by [z, z ] the Euclidean line Right. The noncrossing pair partition {ω 0 10 , ω 3 10 }, {ω 1 10 , ω2 10 }, {ω 4 10 , ω 5 10 }, {ω 6 10 , ω 9 10 }, {ω 7 10 , ω 8 10 } of P 10 .

as a lamination as follows. With the block ω i 1 n , ω i 2 n , . . . , ω i k n , where i 1 < i 2 < . . . < i k , we associate the polygon

[ω i 1 n , ω i 2 n ] ∪ [ω i 2 n , ω i 3 n ] ∪ . . . ∪ [ω i k n , ω i 1 n ].
The lamination is then defined as the union over the partition blocks of the associated polygons.

Recall that the Hausdorff distance between two closed subsets A, B ⊆ D is defined as inf ε > 0 : A ⊆ B (ε) and B ⊆ A (ε) ,

where, for any X ⊆ D, we denoted by X (ε) := {z ∈ D : d(z, X) ≤ ε} the ε-enlargement of X. Endowed with the Hausdorff metric, the set of all closed subsets of D is a compact metric space. Moreover, it is not hard to check that the set of all laminations is a closed, thus compact, subset of this metric space. We are interested in the limit of sequences of larger and larger noncrossing partitions, seen as laminations, for the Hausdorff topology. The above setting was proposed by Aldous [1,2] for the study of random triangulations; it was later used by Kortchemski [6], Curien & Kortchemski [3], Curien & Le Gall [4], Kortchemski & Marzouk [8,7] for the study of many models, including uniform noncrossing partitions and uniform noncrossing pair partitions.

In many cases, the limiting object is a random compact set called the Brownian triangulation B defined as follows. Let ( t ) 0≤t≤1 be a normalized Brownian excursion 2 and, segment of the complex plane joining z with z . A noncrossing partition can thus be seen as a lamination as follows. With the block

ω i 1 n , ω i 2 n , . . . , ω i k n , where i 1 < i 2 < . . . < i k , we associate the polygon [ω i 1 n , ω i 2 n ] ∪ [ω i 2 n , ω i 3 n ] ∪ . . . ∪ [ω i k n , ω i 1 n ].
The lamination is then defined as the union over the partition blocks of the associated polygons.

Recall that the Hausdorff distance between two closed subsets A, B ⊆ D is defined as

inf ε > 0 : A ⊆ B (ε) and B ⊆ A (ε) ,
where, for any X ⊆ D, we denoted by X (ε) := {z ∈ D : d(z, X) ≤ ε} the ε-enlargement of X. Endowed with the Hausdorff metric, the set of all closed subsets of D is a compact metric space. Moreover, it is not hard to check that the set of all laminations is a closed, thus compact, subset of this metric space. We are interested in the limit of sequences of larger and larger noncrossing partitions, seen as laminations, for the Hausdorff topology. The above setting was proposed by Aldous [1,2] for the study of random triangulations; it was later used by Kortchemski [6], Curien & Kortchemski [3], Curien & Le Gall [4], Kortchemski & Marzouk [8,7] for the study of many models, including uniform noncrossing partitions and uniform noncrossing pair partitions.

In many cases, the limiting object is a random compact set called the Brownian triangulation B defined as follows. Let (e t ) 0≤t≤1 be a normalized Brownian excursion 1 The set B is almost surely a closed subset of D and furthermore a continuous trian- gulation of D, in the sense that each connected component of D \ B is an open Euclidean triangle whose vertices belong to the unit circle [START_REF] Gall | Scaling limits of bipartite planar maps are homeomorphic to the 2-sphere[END_REF]. Theorem 1.1 ([3,Theorem 3.8]). Let P n (resp. Pn ) be a random variable uniformly distributed over the set of all noncrossing partitions of P n (resp. noncrossing pair partitions of P 2n ), seen as a lamination. Then P n and Pn both weakly converge toward the Brownian triangulation, for the Hausdorff topology.

The point of the present work is to provide a more straightforward proof of the previous theorem. For this reason, we chose not to include too many historical references on the subject; we refer the reader to the above references and references therein for more details. In [3], the authors first notice that a noncrossing partition of P n is close to a noncrossing pair partition of P 2n ; as a consequence, the result for noncrossing pair partitions implies the result for noncrossing partitions. They then encode a noncrossing pair partition by a tree, which they further encode by a Dyck path; after proper scaling, this path converges to the normalized Brownian excursion. This approach is quite robust but needs in particular a nontrivial result stating that the leaves of a conditioned Galton-Watson tree are asymptotically uniformly spread on the tree.

Instead, we will give a direct encoding of a noncrossing partition of P n by a Dyck path and conclude in a more straightforward manner. In addition, we will give below a recursive construction of noncrossing partitions and noncrossing pair partitions that converge almost surely. The algorithms we propose are the transcription in terms of partitions of an algorithm on Dyck paths due to Marchal [START_REF]Constructing a sequence of random walks strongly converging to Brownian motion[END_REF], which itself is the transcription in terms of Dyck paths of Rémy's famous algorithm [START_REF] Rémy | Un procédé itératif de dénombrement d'arbres binaires et son application à leur génération aléatoire[END_REF] on trees. Let us also mention at this point that Curien & Le Gall [4] also study some sequences of laminations obtained by a recursive construction but, in their case, the limiting object is a continuous triangulation that differs from the Brownian triangulation.

Before presenting our growing algorithms, let us define the Kreweras complement of a noncrossing partition P of P n as the partition K of the set {ω 1 2n , ω 3 2n , . . . , ω 2n-1 2n } whose blocks are given by the connected components of the complement in D of the lamination corresponding to P (see Figure 2). Up to rotation of -π/n, the Kreweras complement of a noncrossing partition of P n is also a noncrossing partition of P n . Taking again the Kreweras complement of the latter noncrossing partition of P n and rotating it by an angle of π/n yields back the original noncrossing partition. We will see two possible ways of defining a noncrossing partition of P n+1 from a noncrossing partition P of P n and an index k ∈ {0, 1, . . . , 2n} (see Figure 3). The first operation consists in adding two vertices between ω k 2n and ω k+1 2n , and declaring the second vertex as belonging to the block of ω k 2n . We then remap the 2n + 2 vertices onto the 2n + 2-th roots of unity in such a way that the cyclic order is preserved and ω k 2n is mapped to ω k 2n+2 . The resulting noncrossing partition of P n+1 is said to be obtained from P by inserting a vertex at position k.

For the second operation, we need to consider the last element in counterclockwise order before ω 2n 2n that belongs to the same block of P ∪ K as ω k 2n : let l := max{j ≤ 2n : ω k 2n and ω j 2n are in the same block of P ∪ K} .

We split each of the vertices ω k 2n and ω l 2n into two new vertices and remap the resulting 2n + 2 vertices onto the 2n + 2-th roots of unity in such a way that the cyclic order is preserved and ω 0 2n is mapped to ω 0 2n+2 . We define a noncrossing partition of P n+1 by declaring any two n + 1-th roots of unity to be in the same block whenever their preimages were in the same block of P ∪ K. Note that the Kreweras complement of this noncrossing partition is obtained in a similar manner by considering the other 2n + 2-th roots of unity. Our operation has the effect of slicing the block of ω k 2n along the chord [ω k 2n , ω l 2n ] into two blocks, one lying in the noncrossing partition and the other one lying in its Kreweras complement. We say that the resulting noncrossing partition of P n+1 is obtained from P by slicing at position k. We will see two possible ways of defining a noncrossing partition of P n+1 from a noncrossing partition P of P n and an index k ∈ {0, 1, . . . , 2n} (see Figure 3). The first operation consists in adding two vertices between ω k 2n and ω k+1 2n , and declaring the second vertex as belonging to the block of ω k 2n . We then remap the 2n + 2 vertices onto the 2n + 2-th roots of unity in such a way that the cyclic order is preserved and ω k 2n is mapped to ω k 2n+2 . The resulting noncrossing partition of P n+1 is said to be obtained from P by inserting a vertex at position k.

For the second operation, we need to consider the last element in counterclockwise order before ω 2n 2n that belongs to the same block of P ∪ K as ω k 2n : let l := max{j ≤ 2n : ω k 2n and ω j 2n are in the same block of P ∪ K} . We split each of the vertices ω k 2n and ω l 2n into two new vertices and remap the resulting 2n + 2 vertices onto the 2n + 2-th roots of unity in such a way that the cyclic order is preserved and ω 0 2n is mapped to ω 0 2n+2 . We define a noncrossing partition of P n+1 by declaring any two n + 1-th roots of unity to be in the same block whenever their preimages were in the same block of P ∪ K. Note that the Kreweras complement of this noncrossing partition is obtained in a similar manner by considering the other 2n + 2-th roots of unity. Our operation has the effect of slicing the block of ω k 2n along the chord [ω k 2n , ω l 2n ] into two blocks, one lying in the noncrossing partition and the other one lying in its Kreweras complement. We say that the resulting noncrossing partition of P n+1 is obtained from P by slicing at position k.

Remark.

Observe that, whenever l = k, the noncrossing partitions obtained from P by g replacements Remark. Observe that, whenever l = k, the noncrossing partitions obtained from P by slicing and by inserting a vertex at position k are the same. Note also that the result is not the same when k = 0 and when k = 2n. In fact, the partitions obtained by insertion only differ by a rotation of 2π/n and the ones obtained by slicing differ by complement and rotation of π/n.

1 2 3 ≥ 2 +1 k l inserting a vertex slicing
We iteratively construct a sequence of random noncrossing partitions (P n ) n≥1 using the following algorithm.

Algorithm 1 (Constructing a sequence of noncrossing partitions).

1. Let P 1 = {ω 0 1 } be the only partition of P 1 . 2. Generate P n+1 from P n as follows:

(a) choose an integer k uniformly at random in {0, 1, . . . , 2n};

(b) with probabilities 1/2 -1/2, set P n+1 to be obtained from P n

• either by inserting a vertex at position k,

• or by slicing at position k. Proposition 2. Let (P n ) n≥1 be constructed by Algorithm 1. Then, for each n, the partition P n is uniformly distributed over the set of noncrossing partitions of P n . Moreover, seen as a lamination, P n almost surely converges toward the Brownian triangulation, for the Hausdorff topology.

We can play a similar game for noncrossing pair partitions (see Figure 4). Let P be a noncrossing pair partition of P 2n and let k ∈ {0, 1, . . . , 2n}. It will be more convenient slicing and by inserting a vertex at position k are the same. Note also that the result is not the same when k = 0 and when k = 2n. In fact, the partitions obtained by insertion only differ by a rotation of 2π/n and the ones obtained by slicing differ by complement and rotation of π/n.

We iteratively construct a sequence of random noncrossing partitions (P n ) n≥1 using the following algorithm. Algorithm 1.2 (Constructing a sequence of noncrossing partitions).

1. Let P 1 = {ω 0 1 } be the only partition of P 1 .

2. Generate P n+1 from P n as follows:

(a) choose an integer k uniformly at random in {0, 1, . . . , 2n};

(b) with probabilities 1/2 -1/2, set P n+1 to be obtained from P n

• either by inserting a vertex at position k,

• or by slicing at position k.

Proposition 1.3. Let (P n ) n≥1 be constructed by Algorithm 1.2. Then, for each n, the partition P n is uniformly distributed over the set of noncrossing partitions of P n . Moreover, seen as a lamination, P n almost surely converges toward the Brownian triangulation, for the Hausdorff topology.

We can play a similar game for noncrossing pair partitions (see Figure 4). Let P be a noncrossing pair partition of P 2n and let k ∈ {0, 1, . . . , 2n}. It will be more convenient to rotate the picture by an angle of -π/2n, so that P is now a partition of ω j 4n , j odd . We consider the Kreweras complement K of P and we set l := max{j ≤ 2n : ω k 2n and ω j 2n are in the same block of K} .

We either add two vertices at the location of ω k 2n or one at the location of ω k 2n and one at the location of ω l 2n . Then, in both cases, we declare the added vertices to form one new block and remap the 2n + 2 vertices onto the odd 4n + 4-th roots of unity in such a way that the cyclic order is preserved and ω 2k-1 4n is mapped to ω 2k-1 4n+4 . We say that the resulting noncrossing pair partitions of P 2n+2 are obtained from P respectively by inserting a short chord and by inserting a long chord at position k.

6

Jérémie Bettinelli to rotate the picture by an angle of -π/2n, so that P is now a partition of ω j 4n , j odd . We consider the Kreweras complement K of P and we set l := max{j ≤ 2n : ω k 2n and ω j 2n are in the same block of K} . We either add two vertices at the location of ω k 2n or one at the location of ω k 2n and one at the location of ω l 2n . Then, in both cases, we declare the added vertices to form one new block and remap the 2n + 2 vertices onto the odd 4n + 4-th roots of unity in such a way that the cyclic order is preserved and ω 2k-1 4n is mapped to ω 2k-1 4n+4 . We say that the resulting noncrossing pair partitions of P 2n+2 are obtained from P respectively by inserting a short chord and by inserting a long chord at position k. Similarly as above, we iteratively construct a sequence of random noncrossing pair partitions ( Pn ) n≥1 .

Algorithm 2 (Constructing a sequence of noncrossing pair partitions).

1. Let P1 = {ω 0 2 , ω 1 2 } be the only pair partition of P 2 . 2. Generate Pn+1 from Pn as follows:

(a) choose an integer k uniformly at random in {0, 1, . . . , 2n};

(b) with probabilities 1/2 -1/2, set Pn+1 to be obtained from Pn by inserting at position k

• either a short chord,

• or a long chord.

Proposition 3. Let ( Pn ) n≥1 be constructed by Algorithm 2. Then, for each n, the partition Pn is uniformly distributed over the set of noncrossing pair partitions of P 2n . Moreover, seen as a lamination, Pn almost surely converges toward the Brownian triangulation, for the Hausdorff topology. Similarly as above, we iteratively construct a sequence of random noncrossing pair partitions ( Pn ) n≥1 .

Algorithm 1.4 (Constructing a sequence of noncrossing pair partitions).

1. Let P1 = {ω 0 2 , ω 1 2 } be the only pair partition of P 2 .

2. Generate Pn+1 from Pn as follows:

(a) choose an integer k uniformly at random in {0, 1, . . . , 2n};

(b) with probabilities 1/2 -1/2, set Pn+1 to be obtained from Pn by inserting at position k

• either a short chord,

• or a long chord.

Proposition 1.5. Let ( Pn ) n≥1 be constructed by Algorithm 1.4. Then, for each n, the partition Pn is uniformly distributed over the set of noncrossing pair partitions of P 2n . Moreover, seen as a lamination, Pn almost surely converges toward the Brownian triangulation, for the Hausdorff topology.

The remainder of the paper is organized as follows. In Section 2, we show how to encode a noncrossing partition by a Dyck path. Section 3 is devoted to the proof of Theorem 1.1 and Section 4 to the proofs of Propositions 1.3 and 1.5.

Encoding noncrossing partitions by Dyck paths

We encode a noncrossing partition P of P n by assigning integer labels to ω k 2n , 0 ≤ k ≤ 2n -1, as follows (see Figure 5). We let K be the Kreweras complement of P and we say that two blocks of P ∪ K are neighbors if there exists an integer k such that ω k 2n belongs to one block and ω k+1 2n belongs to the other block. We first label the blocks of P ∪ K by assigning label 0 to the block that contains ω 0 2n and, inductively, assigning label + 1 to each not yet labeled neighbor of a block labeled . We then assign to each ω k 2n , 0 ≤ k ≤ 2n -1, the label of the block to which it belongs.

Convergence of uniform noncrossing partitions toward the Brownian triangulation 7

The remainder of the paper is organized as follows. In Section 2, we show how to encode a noncrossing partition by a Dyck path. Section 3 is devoted to the proof of Theorem 1 and Section 4 to the proofs of Propositions 2 and 3.

Encoding noncrossing partitions by Dyck paths

We encode a noncrossing partition P of P n by assigning integer labels to ω k 2n , 0 ≤ k ≤ 2n -1, as follows (see Figure 5). We let K be the Kreweras complement of P and we say that two blocks of P ∪ K are neighbors if there exists an integer k such that ω k 2n belongs to one block and ω k+1 2n belongs to the other block. We first label the blocks of P ∪ K by assigning label 0 to the block that contains ω 0 2n and, inductively, assigning label ℓ + 1 to each not yet labeled neighbor of a block labeled ℓ. We then assign to each ω k 2n , 0 ≤ k ≤ 2n -1, the label of the block to which it belongs. If we denote by ℓ k the label assigned to ω k 2n , 0 ≤ k ≤ 2n, then the path (ℓ 0 , ℓ 1 , . . . , ℓ 2n ) is a 2n-step Dyck path 3 . Moreover, this operation yields a bijection between noncrossing partitions of P n and 2n-step Dyck paths; the inverse operation goes as follows. Let (ℓ 0 , ℓ 1 , . . . , ℓ 2n ) be a 2n-step Dyck path. Then the noncrossing partition is given by the equivalence classes of the relation

ω i 2n ∼ ω j 2n ⇐⇒ ℓ i = ℓ j = min min(i,j)≤k≤max(i,j) ℓ k (2.1)
3 Recall that a Dyck path is a finite sequence (a 0 , a 1 , . . . , a l ) of nonnegative integers such that a 0 = a l = 0 and |a k+1 -a k | = 1 for all k ∈ {0, 1, . . . , l -1}. If we denote by k the label assigned to ω k 2n , 0 ≤ k ≤ 2n, then the path ( 0 , 1 , . . . , 2n ) is a 2n-step Dyck path 2 . Moreover, this operation yields a bijection between noncrossing partitions of P n and 2n-step Dyck paths; the inverse operation goes as follows. Let ( 0 , 1 , . . . , 2n ) be a 2n-step Dyck path. Then the noncrossing partition is given by the equivalence classes of the relation

ω i 2n ∼ ω j 2n ⇐⇒ i = j = min min(i,j)≤k≤max(i,j) k (2.1)
for even i, j. Furthermore, the Kreweras complement of this noncrossing partition is given by the equivalence classes of (2.1) for odd i, j. Note also that, if over the set [min(i, j), max(i, j)], the function only reaches its minimum at the extremities, then the chord [ω i 2n , ω j 2n ] belongs to the lamination.

Remark. Let us note that this encoding appeared in [START_REF] Stump | More bijective Catalan combinatorics on permutations and on signed permutations[END_REF]. It is also easy to check that this is in fact exactly the Dyck path that encodes the dual tree of the associated noncrossing pair partition (see Figure 6 and [3], in particular Figure 7) or, equivalently, the (properly rooted) dual two-type tree of [7] (see Figure 2 therein).

Convergence in distribution

Let us start with uniform noncrossing partitions. The proof is very similar to that of [3] but circumvent some technicalities because of the encoding we use; we give it in full detail for the sake of self-containment.

Proof of Theorem 1.1 for uniform noncrossing partitions. For each n ≥ 1, let P n be a random variable uniformly distributed over the set of noncrossing partitions of P n and let L n : [0, 1] → R + be the function defined as follows. We consider the labeling of the 2n-th roots of unity given by the encoding of Section 2. For k ∈ {0, 1, . . . , 2n}, we let L n (k/2n) be the label of ω k 2n and we extend L n to [0, 1] by linear interpolation between these values. A well-known conditioned version of Donsker's invariance principle due to Kaigh [5,Theorem 2.6] states that the following convergence holds in distribution for the uniform topology on the space of continuous real-valued functions on [0, 1]:

L n (s) √ 2n 0≤s≤1 → (e s ) 0≤s≤1 . (3.1)
Using Skorokhod's representation theorem, we may and will assume that the previous convergence holds almost surely. As the set of all closed subsets of D endowed with the Hausdorff metric is a compact metric space, it suffices to show that any accumulation point of (P n ) n is the Brownian triangulation B, defined by (1.1). Let P be such an accumulation point.

We first claim that B ⊆ P almost surely. It is a classical fact that the local minimums of e on (0, 1) are almost surely distinct. On the set of full measure where this property holds, if s e ∼ t with s < t, we can always find even s n , t n ∈ {0, 2, 4, . . . , 2n} such that s n < t n ,

s n 2n → s , t n 2n → t and L n s n 2n = L n t n 2n < min [ s n +1 2n , t n -1 2n ] L n .
Indeed, this fact is plain if e r > e s = e t for all r ∈ (s, t); otherwise, there exists r ∈ (s, t) such that e r = e s = e t , so that e r is a local minimum and, as a result, neither s nor t are times of a local minimum and one can find s < s and t > t arbitrarily close to s and t such that (s , t ) falls into the previous case. The latter property implies that the chord ω s n 2n , ω t n 2n belongs to P n (recall (2.1) and the discussion thereafter). As a result, the segment [e 2iπs , e 2iπt ] ⊆ P and the claim follows. Now, in order to see that P ⊆ B, observe that, as all the P n are laminations, P is also a lamination. Then, as B is almost surely maximal for the inclusion relation ([9, Proposition 2.1]), we necessarily have B = P. This completes the proof.

We now turn to noncrossing pair partitions. We can use the observation of [3] that there exists a simple bijection between noncrossing partitions of P n and noncrossing pair partitions of P 2n , such that the corresponding laminations are at Hausdorff distance less than π/2n (see Figure 6).

Convergence of uniform noncrossing partitions toward the Brownian triangulation 9

Indeed, this fact is plain if r > s = t for all r ∈ (s, t); otherwise, there exists r ∈ (s, t) such that r = s = t , so that r is a local minimum and, as a result, neither s nor t are times of a local minimum and one can find s ′ < s and t ′ > t arbitrarily close to s and t such that (s ′ , t ′ ) falls into the previous case. The latter property implies that the chord ω s n 2n , ω t n 2n belongs to P n (recall (2.1) and the discussion thereafter). As a result, the segment [e 2iπs , e 2iπt ] ⊆ P and the claim follows. Now, in order to see that P ⊆ B, observe that, as all the P n are laminations, P is also a lamination. Then, as B is almost surely maximal for the inclusion relation ([9, Proposition 2.1]), we necessarily have B = P. This completes the proof.

We now turn to noncrossing pair partitions. We can use the observation of [3] that there exists a simple bijection between noncrossing partitions of P n and noncrossing pair partitions of P 2n , such that the corresponding laminations are at Hausdorff distance less than π/2n (see Figure 6). Alternatively, we will see that the encoding of Section 2 is well behaved with respect to the property of being a noncrossing pair partition.

Proof of Theorem 1 for uniform noncrossing pair partitions. Let P be a noncrossing partition of P 2n . As in the introduction, we rotate the picture by an angle of -π/2n and see P as a partition of ω j 4n , j odd (plainly, this will bear no effects in the limit). We consider the Kreweras complement K of P and let (ℓ 0 , ℓ 1 , . . . , ℓ 4n ) be its encoding Dyck path. By definition, P is a noncrossing pair partition if and only if the equivalence classes given by (2.1) for odd indices are all of size 2 (where n is replaced by 2n). Equivalently, for each k ∈ {0, 1, . . . , 2n -1}, we have |ℓ 2k+2ℓ 2k | = 2, so that the path (ℓ 0 /2, ℓ 2 /2, ℓ 4 /2, . . . , Alternatively, we will see that the encoding of Section 2 is well behaved with respect to the property of being a noncrossing pair partition.

Proof of Theorem 1.1 for uniform noncrossing pair partitions. Let P be a noncrossing partition of P 2n . As in the introduction, we rotate the picture by an angle of -π/2n and see P as a partition of ω j 4n , j odd (plainly, this will bear no effects in the limit). We consider the Kreweras complement K of P and let ( 0 , 1 , . . . , 4n ) be its encoding Dyck path. By definition, P is a noncrossing pair partition if and only if the equivalence classes given by (2.1) for odd indices are all of size 2 (where n is replaced by 2n). Equivalently, for each k ∈ {0, 1, . . . , 2n -1}, we have | 2k+2 -2k | = 2, so that the path ( 0 /2, 2 /2, 4 /2, . . . , 4n /2) is a Dyck path that encodes all the information of the original Dyck path, and which does not satisfy any constraints (see Figure 7). Jérémie Bettinelli ℓ 4n /2) is a Dyck path that encodes all the information of the original Dyck path, and which does not satisfy any constraints (see Figure 7). As a result, a uniform noncrossing pair partition of P 2n is encoded by a uniform 2nstep Dyck path. By Kaigh's theorem, after proper rescaling, this path to the normalized Brownian excursion, and the original encoding 4n-step Dyck path clearly converges toward the same limit, multiplied by √ 2. One then concludes exactly as in the case of uniform noncrossing partitions (the extra multiplicative factor does not alter the identifications).

Almost sure convergence

In this section, we prove Propositions 2 and 3. In fact, they are both straightforward consequences of [START_REF]Constructing a sequence of random walks strongly converging to Brownian motion[END_REF] and the encoding we use.

Proof of Proposition 2. In terms of encoding Dyck paths, inserting a vertex at position k amounts to inserting one up-step followed by one down-step right after time k and slicing at position k amounts to lifting up by one the part of the path between time k and the first subsequent time the path becomes strictly lower than its height at time k (see Figure 8).

These are exactly the moves considered in [START_REF]Constructing a sequence of random walks strongly converging to Brownian motion[END_REF] (see in particular [10, Figure 1]). The latter reference implies that, for each n, the encoding Dyck path of P n is uniformly distributed over the set of 2n-step Dyck paths and that the convergence (3.1) holds almost surely for this choice of sequence (P n ) n . As a result, there is no need to apply Skorokhod's representation theorem in the proof of Theorem 1, so that P n strongly converges toward the Brownian triangulation. As a result, a uniform noncrossing pair partition of P 2n is encoded by a uniform 2nstep Dyck path. By Kaigh's theorem, after proper rescaling, this path converges to the normalized Brownian excursion, and the original encoding 4n-step Dyck path clearly converges toward the same limit, multiplied by √ 2. One then concludes exactly as in the case of uniform noncrossing partitions (the extra multiplicative factor does not alter the identifications).

Almost sure convergence

In this section, we prove Propositions 1.3 and 1.5. In fact, they are both straightforward consequences of [START_REF]Constructing a sequence of random walks strongly converging to Brownian motion[END_REF] and the encoding we use.

Proof of Proposition 1.3. In terms of encoding Dyck paths, inserting a vertex at position k amounts to inserting one up-step followed by one down-step right after time k and slicing at position k amounts to lifting up by one the part of the path between time k and the first subsequent time the path becomes strictly lower than its height at time k (see Figure 8).

These are exactly the moves considered in [START_REF]Constructing a sequence of random walks strongly converging to Brownian motion[END_REF] (see in particular [10, Figure 1]). The latter reference implies that, for each n, the encoding Dyck path of P n is uniformly distributed over the set of 2n-step Dyck paths and that the convergence (3.1) holds almost surely for this choice of sequence (P n ) n . As a result, there is no need to apply Skorokhod's representation theorem in the proof of Theorem 1.1, so that P n strongly converges toward the Brownian triangulation.

Proof of Proposition 1.5. Inserting a short chord and inserting a long chord at position k respectively correspond on the unconstrained encoding Dyck path of Figure 7 to inserting one up-step followed by one down-step right after time k and lifting up by one the part of the path between time k and time l. We conclude as above.

Figure 1 :

 1 Figure 1: Left. The noncrossing partition {ω 0 7 , ω 2 7 , ω 3 7 }, {ω 1 7 }, {ω 4 7 , ω 6 7 }, {ω 5 7 } of P 7 . Right. The noncrossing pair partition {ω 0 10 , ω 3 10 }, {ω 1 10 , ω 2 10 }, {ω 4 10 , ω 5 10 }, {ω 6 10 , ω 9 10 }, {ω 7 10 , ω 8 10 } of P 10 .

Figure 2 :

 2 Figure 2: The Kreweras complement of the partition {ω 0 10 , ω 2 10 , ω 3 10 }, {ω1 10 }, {ω 4 10 , ω 5 10 }, {ω 6 10 , ω 7 10 , ω 8 10 , ω 9 10 } is {ω 1 20 , ω 3 20 }, {ω 5 20 }, {ω 7 20 , ω 11 20 , ω 19 20 }, {ω 9 20 }, {ω 13 20 }, {ω 15 20 }, {ω 17 20 } . For instance, the blocks {ω 0 10 , ω 2 10 , ω 3 10 } and {ω 5 20 } are neighbors.

Figure 2 :

 2 Figure 2: The Kreweras complement of the partition {ω 0 10 , ω 2 10 , ω 3 10 }, {ω1 10 }, {ω 4 10 , ω 5 10 }, {ω 6 10 , ω 7 10 , ω 8 10 , ω 9 10 } is {ω 1 20 , ω 3 20 }, {ω 5 20 }, {ω 7 20 , ω 11 20 , ω 19 20 }, {ω 9 20 }, {ω 13 20 }, {ω 15 20 }, {ω 17 20 } . For instance, the blocks {ω 0 10 , ω 2 10 , ω 3 10 } and {ω 5 20 } are neighbors.

Figure 3 :

 3 Figure 3: The noncrossing partitions obtained by inserting a vertex and by slicing at position k.

Figure 3 :

 3 Figure 3: The noncrossing partitions obtained by inserting a vertex and by slicing at position k.

Figure 4 :

 4 Figure 4: Growing a pair partition.

Figure 4 :

 4 Figure 4: Growing a pair partition.

Figure 5 :

 5 Figure 5: Encoding a noncrossing partition by a Dyck path.

Figure 5 :

 5 Figure 5: Encoding a noncrossing partition by a Dyck path.

Figure 6 :

 6 Figure 6: The noncrossing partition of P n that corresponds to a noncrossing pair partition of P 2n is obtained by identifying ω 2k-1 2n with ω 2k 2n for each 1 ≤ k ≤ n.

Figure 6 :

 6 Figure 6: The noncrossing partition of P n that corresponds to a noncrossing pair partition of P 2n is obtained by identifying ω 2k-1 2n with ω 2k 2n for each 1 ≤ k ≤ n.

10

 10

Figure 7 :

 7 Figure 7: The unconstrained Dyck path that encodes a noncrossing pair partition.

Figure 7 :

 7 Figure 7: The unconstrained Dyck path that encodes a noncrossing pair partition.

Figure 8 :

 8 Figure 8: Consequences on the encoding Dyck paths of inserting a vertex or slicing at position k.

Figure 8 :

 8 Figure 8: Consequences on the encoding Dyck paths of inserting a vertex or slicing at position k.

  and, for s, t ∈ [0, 1], declare s e ∼ t whenever e s = e t = min min(s,t)≤r≤max(s,t) e r . The Brownian

	triangulation is the set
	B :=	e 2iπs , e 2iπt .	(1.1)
	s	e ∼t

A normalized Brownian excursion is a standard Brownian motion on [0, 1] starting from 0 and conditioned on being at 0 at time 1 and staying positive on (0, 1). As this is a zero-probability event, some care is needed for a proper definition: see e.g.[START_REF] Revuz | Grundlehren der Mathematischen Wissenschaften[END_REF] Chapter XII].

A normalized Brownian excursion is a standard Brownian motion on [0, 1] starting from 0 and conditioned on being at 0 at time 1 and staying positive on (0, 1). As this is a zero-probability event, some care is needed for a proper definition: see e.g.[START_REF] Revuz | Grundlehren der Mathematischen Wissenschaften[END_REF] Chapter XII].

Recall that a Dyck path is a finite sequence (a 0 , a 1 , . . . , a l ) of nonnegative integers such that a 0 = a l = 0 and |a k+1a k | = 1 for all k ∈ {0, 1, . . . , l -1}.

This work is partially supported by Grant ANR-14-CE25-0014.