```h
let set (s : store) (x : 'a rref) (v : 'a) : unit =
begin (* Update the diff list. *)
match !s with
(* If the diff list is empty, the current version is the root version
  which has no undo log, so there is nothing to do. *)
| [] -> ()
| current_diff :: _rest ->
(* Add the write to the diff of the current version *)
Stack.push (Set (x, x.current)) current_diff;
end;
(* Update the global state. *)
x.current <- v
```

In the case where the current version is the root version, our representation does not maintain an undo log for the root version so we do not record the write. The root version has no parent so `commit` or `rollback` cannot be called, so we cannot observe the presence of an undo log.

## Branch and terminate

```h
let branch s =
s := Stack.create () :: !s
let terminate_nodiff s =
match !s with
| [] -> invalid_arg "terminate_nodiff_version: root version cannot be terminated"
| diff :: rest ->
  assert (Stack.is_empty diff);
s := rest
```

Note: checking that `diff` is empty is slightly stronger than our specification, which allows non-empty `diffs` of updates that cancel each other. Our implementation enforces the more intentional specification that `terminate_nodiff` is always called immediately after `branch`, `commit` or `rollback`.

## Rollback and commit
`rollback` mutates the current state to become equal to the parent state, while `commit` mutates the parent state to become equal to the current state.

```h
let rollback s =
match !s with
| [] ->
  invalid_arg "rollback: the root version cannot be rolled back"
| current_diff :: _ ->
  (* Current state:
     { current version    current diff    parent version
     in state A           in state B       in state B
     }
  *)
while not (Stack.is_empty current_diff) do
match Stack.pop current_diff with
| Set (x, old) ->
  x.current <- old
done;
(* Final state:
   { current version    0          parent version
   in state B           in state B
  }
 *)
```
commit relies on an auxiliary function on stacks, `move_stack s1 ~into:s2`. It moves all elements of `s1` into `s2`, in the same order as they were in `s1`, which is now empty. In other words, if before the call the list of elements of `s1` and `s2` were `11` and `12` respectively, then after the call it is `[]` and `11` @ `12`.

```hkl
let commit s =
  match !s with
  | [] ->
    invalid_arg "rollback: the root version cannot be committed"
  | diff :: [] ->
    (* Current state:
       { current version \mathrel{\overleftarrow{\mathrel{\to}}} diff root version
         in state A                 in state B
       }
    *)
    Stack.clear diff;
    (* Final state:
       { current version \mathrel{\overleftarrow{\mathrel{=}}} root version
         in state A                 in state A
       }
    *)
| diff :: parent_diff :: _ ->
  (* Current state:
     { current version \mathrel{\overleftarrow{\mathrel{to}}} diff parent version parent parent version
       in state A                 in state B                 in state C
     }
  *)
move_stack diff ~into:parent_diff;
  (* Final state:
     { current version \mathrel{\overleftarrow{\mathrel{=}}} root version
       in state A                 in state A                 in state C
     }
  *)
```

**Complexity** Ideally we want each operation to take constant time, possibly amortized. Amortized reasoning works well with `rollback`. It traverses the undo log of the current version to perform each undo action, removing it from the `diff`. Each undo action is rolled back at most once, and we can consider that its rollback cost was paid in advance by the corresponding `set`.

This reasoning fails for `commit` unfortunately. `move_stack` traverses the current undo log, and this traversal cost can be amortized, but the undo actions are not dropped after traversal, they remain in the `diff` of another version. One would need `set` to pre-pay for each version, which is not a constant cost. Amortized reasoning fails, and in fact we can observe quadratic complexity in the worst case: consider a sequence of *N* branch calls, then *N* writes, then *N* (`commit`; `terminate_nodiff`) sequences, this runs in $O(N^2)$. (This is not a concern if you only use backtracking and never the transactional interface, as in this case you always `rollback` and never `commit`.)

It would be possible to change the `diff` data-structure from stacks to something that provides constant-time concatenation, such as doubly-linked lists. Instead we move to our second implementation, which uses simpler data structures and can thus be expected to have lower constant factors – at the cost of being less abstract.

## 3.2 Stack and indices

In our second iteration, we use a single stack to store the undo actions of all versions. We remember the boundaries of each version in a separate list.
```javascript
type store = { journal: undo_action Stack.t;
  mutable children: int list; }
```

For each child (non-root) version, the list `children` stores the index of this version in the `journal`, that is, the starting position of the diff of this version. The children versions are stored in the list from the most recent (the current version) to the oldest (the immediate child of the root version). Note that the root version keeps no diff / undo log, so its immediate child always starts at position 0.

For example, a store with three children versions in addition to the root version may have the following representation – we draw the stacks and lists as growing from the right to the left.

<figure><img src="image_90.png" /></figure>

**Easy changes** Most functions are trivially adapted to this new representation. In the case of `set`, we have to check the list `s.children` to tell whether we are at the root version (which stores no diff) or not, and only push to `journal` in the non-root case:

```javascript
let set (s : store) (x : 'a rref) (v : 'a) : unit =
begin match s.children with
| [] -> ()
| _ :: _ ->
  Stack.push (Set (x, x.current)) s.journal;
end;
x.current <- v
```

`branch` uses the current length of the journal as the starting position of the new version:

```javascript
let branch s =
  s.children <- Stack.length s.journal :: s.children
```

Finally, `rollback` performs some length computation to determine how many undo actions to roll back from the journal:

```javascript
let rollback s =
  match s.children with
| [] ->
  invalid_arg "rollback: the root version cannot be rolled back"
| curr_start :: _ ->
  let current_version_length = Stack.length s.journal - curr_start in
  for _i = 1 to current_version_length do
    match Stack.pop s.journal with
    | Set (x, old) ->
      x.current <- old
  done;
  assert (Stack.length s.journal = curr_start);
```
**Commit** This function motivated the change of representation. In the case where the parent version is not the root version, **commit** does not touch the journal at all – the undo actions remain in the same position in the stack, we only need to adjust the version boundaries. We move the start of the current version to the end of the stack, so that the parent version adopts the undo actions that were previously in the current version.

```R
let commit s =
  match s.children with
  | [] ->
    invalid_arg "rollback: the root version cannot be committed"
  | _curr_start :: parent_start :: rest ->
    (* Current state:
       end of stack             pos. curr_start
     current version < current diff parent version < parent diff parent parent version
     state: A                 state: B                 state: C
    }
    We move the boundary of our current version to the current stack length. This moves the content of our diff to our parent version. *)
  s.children <- Stack.length s.journal :: parent_start :: rest;
  (* Final state:
     end of stack             pos. Stack.length      current diff      pos. parent_start
     current version ==       parent version          + parent diff      parent parent version
     state: A                 state: A                 state: C
    *)

| curr_start :: [] ->
  (* Current state:
     end of stack             pos. curr_start = 0
     current version < current diff root version
     state: A                 state: B
    }
    The current version is the immediate child of the root version, which has no undo log. We know that the current version starts in position [0], and can discard the changes in our undo log. *)
assert (curr_start = 0);
Stack.clear s.journal;
(* Final state:
     end of stack             pos. curr_start = 0
     current version ==       root version
     state: A                 state: A
    *)
```

In the case where the root version is the parent version, a linear cost may remain — depending on the complexity of `Stack.clear`. But there is no complexity issue there, this is amortized constant time. Indeed, we only pay this cost once per undo action, and then the actions are removed from the journal. We can consider that `set` paid for this cost in advance.

## 3.3 Record elision

Our last iteration is a small modification of our previous version that avoids recording several writes to the same cell in a given version. Recording only the first write suffices to rollback the changes if necessary.

During `set` we could walk back the undo log of the current version, and exit early if we
find another write to the same reference. This would be very slow. Instead we store, in each reference, information on when the last write to this reference was recorded – using positions inside the journal as a natural notion of *timestamp*.

```typescript
type 'a rref = {
  mutable current: 'a;
  (** The value of this reference in the current version. *)
  mutable last_record: int;
  (** [last_record] is the position of the most recent
     record of this reference recorded in the journal,
     or -1 this reference has no record. *)
}
```

```typescript
let make (_s : store) (v : 'a) : 'a rref =
{ current = v; last_record = -1; }
```

(Our actual code uses an abstract type `Pos_option.t` instead of `int` to hide the `-1` encoding, but auxiliary abstractions would make the presentation heavier here.)

We need to save this `last_record` field in our undo actions to be able to restore it correctly during rollback:

```typescript
type undo_action =
| Set : {
  ref: 'a rref;
  (** the reference that was written *)
  previous: 'a;
  (** the value of the reference before the write *)
  previous_record: int;
  (** the [last_record] value at write time *)
} -> undo_action
```

**Set** We can skip recording the write if the last record belongs to the current version. We update the `last_record` field when we extend the journal.

```typescript
let set (s : store) (x : 'a rref) (v : 'a) : unit =
begin match s.children with
| [] -> ()
| current_version_start :: _ ->
  if x.last_record >= current_version_start then ()
else begin
  let new_record = Stack.length s.journal in
  Stack.push (Set {
    ref = x;
    previous = x.current;
    previous_record = x.last_record;
  }) s.journal;
  x.last_record <- new_record;
end
end;
x.current <- v
```

Note that while the space-overhead complexity reduction may feel nebulous for many ap-
plications, this optimization also makes a qualitative difference in performance. Indeed, the (polymorphic) writes dominate the cost of `set`; with the previous implementations, each `set` would perform two such writes, one to the reference field and the other by pushing into the journal. With the new implementation, in the common case we perform a single write. Outside the root-version fast path, our previous `set` implementations was at least twice slower than with standard references, while the overhead of the new version becomes negligible for write-heavy workflows. Said otherwise, this implementation is low-cost even in presence of infrequent branching.

**Commit** There is a subtlety in the case where our parent version is the root version. The previous implementation simply clears the journal in this case, but doing so invalidates the `last_record` fields of the references mentioned in this journal, pointing to journal entries that no longer exist. This turns into a bug later where `set` does record a reference, falsely believing that it is already recorded. To avoid creating invalid `last_record` positions, we must clear this field for the references mentioned in the journal. We highlight the only lines of code that change since the last version:

```javascript
let commit s =
  match s.children with
  | [] -> invalid_arg "rollback: the root version cannot be committed"
  | _curr_start :: parent_start :: rest ->
    s.children <- Stack.length s.journal :: parent_start :: rest;
  | curr_start :: [] ->
    assert (curr_start = 0);
  s.journal |> Stack.iter (function
    | Set {ref; previous = _; previous_record = _} ->
      ref.last_record <- -1;
  );
  Stack.clear s.journal;
```

Note that, when the parent version is not the root version, it may be the case that a single reference was recorded in the current diff and also in the parent diff. In this case it ends up mentioned twice in the final diff of the parent version. We do not preserve the invariant that a reference is recorded at most once in each version. Enforcing this invariant saves no work, and the obvious way to do it is to perform a linear traversal during `commit`, which would create again a quadratic worst case.

# 4 Interface(s)

```javascript
module BtRef = StoreBacktrackingRef
let rec typeof env = function (*...*) | Use (t, u) ->
  match typeof env t with
  | TyEq (ty1, ty2) ->
    BtRef.branch env.store;
  let finally () =
    BtRef_rollback env.store;
    BtRef.terminate_nodiff env.store; in
  Fun.protect ~finally @@ fun () ->
  introduce_equalities env ty1 ty2;
  typeof env u
```
The primitives defined previously are enough to use our Union-Find with backtracking. In this section we build two higher-level interfaces, to show that our primitives are expressive enough. One expresses the transactional API of François Pottier, the other expresses the original semi-persistent API of Conchon and Filliâtre (2008).

## 4.1 Transactional API

François Pottier exposes the following function for his transactional reference implementation, `StoreTransactionalRef`:

(**[tentatively s f] runs the function [f] within a new transaction on the store [s]. If [f] raises an exception, then the transaction is aborted, and all updates performed by [f] on references in the store [s] are rolled back. If [f] terminates normally, then the updates performed by [f] are committed.

> Two transactions on a single store cannot be nested.

> A cell that is created during a transaction still exists after the transaction, even if the transaction is rolled back. In that case, its content should be considered undefined. *)

val tentatively: 'a store -> (unit -> 'b) -> 'b

We can implement this API for our backtracking references, with two improvements:

1. Our transactions can be nested at will. (This single change to the `StoreTransactionalRef` specification suffices to express arbitrary backtracking.)

2. Our specification naturally gives a meaning to the content of a reference that was created in a version since rolled back. In our specification, a reference is defined in all versions, and its initial value (in all versions) is the parameter provided to `make`.

As we remarked earlier, `StoreTransactionalRef` also provides the important property of being low-cost in the sense that read and writes outside a `tentatively` call are essentially as fast as raw references. We also preserve this property, thanks to the absence (in our implementations) of an undo log for the root version.

let tentatively (s : store) (f : unit -> 'b) : 'b =
  branch s;
  match f () with
    | v ->
        commit s;
        terminate_nodiff s;
    v
  | exception e ->
    let b = Printexc.get_raw_backtrace() in
    rollback s;
    terminate_nodiff s;
    Printexc raises_with_backtrace e b

## 4.2 Semi-persistent API

The API proposed in Conchon and Filliâtre (2008) has a more declarative, less imperative flavor than ours.
```python
module SemiPersistent : sig
    type versioned_store

    val new_store : unit -> versioned_store
    val branch : versioned_store -> versioned_store

    val make : versioned_store -> 'a -> 'a rref
    val get : versioned_store -> 'a rref -> 'a
    val set : versioned_store -> 'a rref -> 'a -> unit
end
```

This API manipulates versioned stores, whereas our imperative API acts on a global store. With this versioned API, `branch` returns a new store version. The functions `branch`, `get` or `set` do not need to be called on the current version, but they backtrack to the version they were given, invalidating/aborting any child version. There is no explicit way to terminate a version.

This gives nice, declarative code for our store-backtracking function.

```python
module SPRef = StoreBacktrackingRef.SemiPersistent
let rec typeof env = function (*...*) | Use (t, u) ->
    match typeof env t with
    | TyEq (ty1, ty2) ->
        let env = { env with store = SPRef.branch env.store } in
        introduce_equalities env ty1 ty2;
        typeof env u
```

On the other hand, we are not sure how to gracefully integrate the transactional features, the difference between `commit` and `rollback`. This is related to the fact that termination of versions is implicit. We could add a `commit` function, but it might break user expectations by having the user of a child version modify its parent version.

(It is also somewhat awkward that `make` takes a versioned store as input but adds the reference to all versions.)

In fact, we can define a generic functor that takes a data-structure with our imperative API, and implements the declarative API on top.

```python
module type Backtracking = sig
type t
    val branch : t -> unit
    val terminate : t -> unit
end
```

(With our primitives, `terminate` is defined by calling `rollback` then `terminate_nodiff`.)

```python
module type SemiPersistent = sig
type t
    type version

(* A root version with the given initial state;
it is initially the current version for this state. *)
val new_root : t -> version
```
(* Branches a new version from a given version
 (any previous transitive child of the given version is invalidated);
 the new version becomes the new current version. *)

val branch : version -> version

(* The given version becomes the current version
 (any transitive child is invalidated);
 the corresponding global state is returned. *)

val access : version -> t

end

module Make (D : Backtracking)

: SemiPersistent with type t = D.t

= struct ... end

The type version provided by this functor keeps the global state of the datastructure, along with a mutable status field that tracks whether it is currently the current version, is the parent of another version, or has been invalidated by backtracking.

type t = D.t
type version = {
  global : D.t;
  mutable status : status;
}

and status =
| Current
| Parent_of of version
| Invalid

let new_root global =
{ global; status = Current; }

Branching modifies the status of the branched version to track its child. We first implement `branch_current`, which assumes that it gets the current version.

let branch_current version =
  assert (version.status = Current);
  DIMP branch version.global;
  let child = { global = version.global; status = Current } in
  version.status <- Parent_of child;
  child

We then implement a backtrack primitive that backtracks the global state to make a given version the current version.

let backtrack version =
(* [collect] accumulates the transitive children of a version. *)
let rec collect children version =
  match version.status with
  | Current -> children
  | Invalid -> invalid_arg "backtrack: this version is invalid"
  | Parent_of child -> collect (child :: children) child
  in
```c
(* terminate and invalidate all children versions. *)
collect [] version |> List.iter (fun child ->
    child.status <- Invalid;
    D.terminate version.global;
);
version.status <- Current
```

Finally, `branch` and `access` first backtrack to the given version, then branch a new version or access the underlying global structure.

```hkl
let branch version =
    backtrack version;
    branch_current version

let access version =
    backtrack version;
    version.global
```

# 5 Related Work

**StoreTransactionalRef** Within the library ecosystem we are familiar with, our work is fairly similar to François Pottier’s StoreTransactionalRef implementation. We provide more features (nested transactions) with no additional costs. We haven’t discussed this with François Pottier yet, but we would expect our proposal to replace his StoreTransactionalRef module completely.

**In automated solvers** Automated solvers, for example SMT solvers, rely heavily on efficient backtracking. When we looked in the opam package repository for an implementation of backtrack-able Union-Find or backtrack-able references, we could not find anything; but since we worked on this paper every author of a solver we met tells us with “l’air penaud” that they have a version of this, deep in the middle of their own code, that they have never shown to anyone. Boo!

A kind anonymous reviewer also pointed us to the CVC5 overview paper: Barbosa, Barrett, Brain, Kremer, Lachmitt, Mann, Mohamed, Mohamed, Niemetz, Nötzli, Ozdemir, Preiner, Reynolds, Sheng, Tinelli, and Zohar (2022). In Section 2.4, “context-dependent data structures”, they mention a general idea of backtrackable data structures indexed by a *context* with an imperative push/pop interface – as common in SAT/SMT solvers. CVC5 supports various data-structures as first-class members of those contexts, which also correspond to our stores. It is not clear to non-experts as we are whether one should try to continue with just backtrackable stores of references as a simple building block, and define elaborate data structures on top of it (Union-Find, hashtables, etc.), or whether we really get noticeable efficiency benefits by adding more data structures as first-class concepts in the backtrackable store, creating opportunities for specialized implementations or more compact representations.

**Hidden OCaml implementations** After submitting this article we were pointed to, in particular, (unpublished) implementations of backtracking stores of references in the FaCiLe constraint-solving library and in the Colibri2 constraint solver, which more generally implements the context interface of CVC5 for various data structures. Note that SMT implementations typically support only backtracking, that is an `abort` operation, but not the `commit` operation of François Pottier’s transactional references. FaCiLe does support a `commit` operation which is described as a `cut` from logic programming.
**Specialized implementations** Finally, in the late 80s there was apparently a lot of work on specialized implementations of Union-Find with various forms of built-in backtracking support, see for example *Apostolico, Italiano, Gambosi, and Talamo* (1994). We don't know of released implementation of these algorithms. They may be marginally faster than building on top of stores of references, but cannot be reused for other data structures.

# 6 Benchmarks

We wrote some benchmarks to confirm experimentally our overall claim: the implementation we present in this work (the latest iteration, with the record-elision optimization) provides references with backtracking support at low cost. They are suitable to build backtracking data structures.

You can find our detailed performance results at https://gitlab.inria.fr/gscherer/unionfind/-/blob/jfla-benchmarks/bench/README.Store.JFLA.md A subset of these results are mentioned in Appendix A.

In our performance tests, the **Facile** implementation is around 15% slower than ours, while **Colibri2** is around 60% slower than our code. (These overheads are small and become negligible for most workflows that are not dominated by reference performance; for comparison, using a persistent Map is 13x slower than our implementation, and our attempt to use **CCHashTrie** with transient updates fared even worse.)

We believe that the **Colibri2** slowdown comes from an "on-demand" design where the backtracking work is done the next time a reference is accessed, instead of backtracking all references eagerly at abort/rollback time. This on-demand logic may save effort in some workloads, but it adds an extra *rewind* function call in the hot paths of *get* and *set*. In the common case the *rewind* function returns immediately because no backtracking is going on, or because it has already been performed, but a function call that returns immediately is enough in a very fast path for a noticeable performance difference.

# References

* Alberto Apostolico, Giuseppe F. Italiano, Giorgio Gambosi, and Maurizio Talamo. The set union problem with unlimited backtracking. *SIAM Journal on Computing*, 23(1):50–70, 1994.

* Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength smt solver. In Dana Fisman and Grigore Rosu, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, pages 415–442, Cham, 2022. Springer International Publishing. ISBN 978-3-030-99524-9.

* Sylvain Conchon and Jean-Christophe Filliâtre. *A Persistent Union-Find Data Structure*. In *ACM SIGPLAN Workshop on ML*, pages 37–45, Freiburg, Germany, October 2007. ACM Press.

* Sylvain Conchon and Jean-Christophe Filliâtre. *Semi-Persistent Data Structures*. In *17th European Symposium on Programming (ESOP’08)*, April 2008.
# A Boring Benchmarks

We benchmarked several implementations of stores of references, some backtracking, some supporting only non-nested transactions, some supporting no transaction at all:

**Ref** is just using raw references. No transactions or backtracking. transactional or backtracking workflows.

**Map** is François Pottier's **StoreMap** implementation. It supports constant-time backtracking, but the logarithmic overhead on each access is prohibitive.

**Vector** is François Pottier's implementation storing all references in a dynamic array. The array can be copied, which gives us a way to implement backtracking.

**BacktrackingRefv1** was our first implementation of backtracking reference store in Section 3.1. It contains a complexity bug for the `commit` operation.

**BacktrackingRefv2** was our second implementation of backtracking reference store in Section 3.2, fixing the complexity issue for `commit`.

**BacktrackingRef** is our final, third implementation of backtracking reference store in Section 3.3. It contains a record-elision optimization that elides redundant writes to the journal at the same version, improving space usage and also time constant factors (only one polymorphic write in the common case).

**TransactionalRef** is François Pottier's implementation of "transactional" references. It contains its own sort of record-eliding optimization, and should behave similarly well in write-heavy workflows.

**Facile** is an implementation of our interface on top of FaCiLe's backtracking references: https://github.com/Emmanuel-PLF/facile/blob/master/lib/fcl_stak.mli FaCiLE also implements a record-elision optimization.

**Colibri2** is an implementation of our interface on top of Colibri2's references in backtracking contexts. https://git.frama-c.com/pub/colibrics/-/blob/bobot/abs/colibri2/stdlib/context.mli Colibri2 also implements a record-elision optimization.

(For full scripts and even more results, see https://gitlab.inria.fr/gscherer/unionfind/-/blob/jfla-benchmarks/bench/README.Store.JFLA.md)

For most applications of references, reads dominate writes. The benchmarks that follow perform 2¹⁵ writes and 2²⁰ reads (so 32x more reads) to an array of 2¹⁰ references. (This workload is then iterated a certain number of times.)

## A.1 Raw benchmarks

These benchmarks only test read and write, no transactional or backtracking workflows. (No transaction is ever started or no backtracking snapshot taken.)
<table><thead><tr><td>impl.</td><td>time</td><td>memory</td></tr></thead><tbody><tr><td>Ref</td><td>1.37s</td><td>2.4Mio</td></tr><tr><td>TransactionalRef</td><td>1.64s</td><td>2.4Mio</td></tr><tr><td>BacktrackingRefv1</td><td>1.55s</td><td>2.4Mio</td></tr><tr><td>BacktrackingRefv2</td><td>1.52s</td><td>2.5Mio</td></tr><tr><td>BacktrackingRef</td><td>1.53s</td><td>2.4Mio</td></tr><tr><td>Facile</td><td>1.74s</td><td>2.4Mio</td></tr><tr><td>Colibri2</td><td>2.45s</td><td>2.4Mio</td></tr><tr><td>Vector</td><td>1.62s</td><td>2.4Mio</td></tr><tr><td>Map</td><td>20.00s</td><td>4.5Mio</td></tr></tbody></table>

We see that there is a very small performance difference between simple references and the transactional or backtracking version – mostly due to code size / inlining factors, simple references have shorter code but they do the same thing in the hot path.

Facile and Colibri2 are slower than our implementations. Facile is 15% slower, Colibri2 is 60% slower. (See our Related Work section 5 for our understanding of the performance disadvantage of Colibri2.)

Persistent maps have much worse performance than all other due to their logarithmic access overhead.

## A.2 Transactional benchmarks

This benchmark repeatedly performs the raw alloc-read-write workflow under one transaction, which is either committed or aborted.

<table><thead><tr><td>impl.</td><td>time</td><td>memory</td></tr></thead><tbody><tr><td>TransactionalRef</td><td>1.14s</td><td>2.4Mio</td></tr><tr><td>BacktrackingRefv1</td><td>1.42s</td><td>12.2Mio</td></tr><tr><td>BacktrackingRefv2</td><td>1.52s</td><td>12.3Mio</td></tr><tr><td>BacktrackingRef</td><td>1.13s</td><td>2.5Mio</td></tr><tr><td>Facile</td><td>1.20s</td><td>2.5Mio</td></tr><tr><td>Colibri2</td><td>1.63s</td><td>2.5Mio</td></tr><tr><td>Vector</td><td>1.66s</td><td>4.1Mio</td></tr><tr><td>Map</td><td>12.48s</td><td>4.5Mio</td></tr></tbody></table>

TransactionalRef, BacktrackingRef, Facile and Colibri2 perform well under this benchmark, with similar relative differences between them.

On the other hand, previous versions v1 and v2 of BacktrackingRef pay a 2x time overhead due to running under a transaction. Their memory usage is also noticeably higher, due to the absence of record-elision logic: they add each write to the log. (All further benchmarks show the same memory advantage to our final version of BacktrackingRef, corresponding to the better space-complexity claims.)
## B Backtracking benchmarks

<table><thead><tr><td>impl.</td><td>time</td><td>memory</td></tr></thead><tbody><tr><td>BacktrackingRefv1</td><td>18.96s</td><td>458.0Mio</td></tr><tr><td>BacktrackingRefv2</td><td>1.63s</td><td>231.1Mio</td></tr><tr><td>BacktrackingRef</td><td>0.89s</td><td>2.5Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Facile</td><td>1.25s</td><td>2.5Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Colibri2</td><td>1.77s</td><td>2.6Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Vector</td><td>1.87s</td><td>4.1Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Map</td><td>17.12s</td><td>4.6Mio</td></tr></tbody></table>

We can observe the complexity bug in commit for BacktrackingRefv1.

In our previous backtracking benchmark, the nesting depth is 100, with $2^{20}$ reads and $2^{15}$ writes at each level. We could observe better results with Map by having a longer nesting depth, and fewer reads and writes.

If we use a nesting depth of 30000, and only $2^5$ reads and $2^5$ writes at each level, we observe the following results:

<table><thead><tr><td>impl.</td><td>time</td><td>memory</td></tr></thead><tbody><tr><td>BacktrackingRefv1</td><td>0.51s</td><td>160.0Mio</td></tr><tr><td>BacktrackingRefv2</td><td>0.50s</td><td>161.5Mio</td></tr><tr><td>BacktrackingRef</td><td>0.09s</td><td>32.2Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Facile</td><td>0.10s</td><td>40.9Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Colibri2</td><td>0.13s</td><td>33.4Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Vector</td><td>0.78s</td><td>542.6Mio</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;Map</td><td>0.80s</td><td>42.0Mio</td></tr></tbody></table>

Map looks much better, but the record-eliding versions (BacktrackingRef, Facile, Colibri2) perform even better. Vector consumes a lot of memory due to frequent copies; copies corresponding to previous versions of the structure cannot be reclaimed by garbage collection, as we may still restore them on backtracking.

We are not sure whether this high-nesting-low-work scenario is relevant to any real-world use case. Automated theorem provers have very deep nestings of backtracking; but even SMT solvers tend to do a lot of propagation work in-between two backtracking points.
# Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs

Milla Valnet¹, Raphaël Monat² et Antoine Miné³

1 École Normale Supérieure, Université PSL, Paris
milla.valnet@ens.psl.eu

2 Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille
raphael.monat@inria.fr

3 Sorbonne Université, CNRS, LIP6, F-75005 Paris
antoine.mine@lip6.fr

## Résumé

Afin de prévenir les erreurs de programmation, des analyseurs statiques ont été développés pour de nombreux langages; cependant, aucun analyseur mature ne cible l'analyse de valeurs pour un langage fonctionnel à la ML. Des outils de vérification pour ces langages existent, tels les systèmes de types classiques ou les méthodes déductives, mais le raisonnement automatique sur des programmes numériques a jusqu'alors été peu exploré. Cet article décrit un analyseur statique de valeurs par interprétation abstraite pour un langage fonctionnel typé du premier ordre, approche sûre et automatique pour garantir l'absence d'erreurs à l'exécution. En se basant sur des domaines abstraits relationnels et en réalisant des résumés des champs récursifs des types algébriques, cette approche permet d'analyser des fonctions récursives manipulant des types algébriques récursifs et d'inférer dans un domaine abstrait leur relation entrée-sortie. Une implémentation est en cours sur la plateforme d'analyse multilangage MOPSA et analyse avec succès de courts programmes de quelques lignes. Ce travail ouvre ainsi la voie vers une analyse de valeurs précise et relationnelle basée sur l'interprétation abstraite pour les langages fonctionnels d'ordre supérieur à la ML.

## 1 Introduction

Même lorsqu'il est fortement et statiquement typé, un programme fonctionnel est toujours susceptible de signaler des erreurs lors de l'exécution — accès à un tableau en dehors de ses bornes, assertions fausses, divisions par zero, échec de filtrage, etc. — ou d'avoir un comportement indésirable tels les dépassements d'entier. Notre objectif est de développer une analyse capable de détecter statiquement de telles erreurs.

L'obtention de garanties sur les langages fonctionnels s'est jusqu'ici très largement reposée sur les systèmes de types, certains trop imprécis pour prouver l'absence d'erreurs, comme l'inférence à la ML, d'autres très précis comme les types de raffinements [31, 32] mais utilisant des solveurs lourds comme boîtes noires. D'autres techniques se basant sur des prouveurs de théorèmes [13, 30] supportent les fonctions récursives sur les types récursifs, mais demandent à l'utilisateur de spécifier les pré- et post-
conditions des fonctions récursives (équivalent des invariants de boucles) pour assister
le prouveur. Le choix d'une analyse statique comporte ainsi l'avantage d'une méthode
automatique, sans annotation.

Cependant, les analyses statiques de programmes fonctionnels se sont beaucoup
concentrées sur l'analyse de flot de contrôle (CFA), [24, 25] un type d'analyse visant à
déterminer à quel point du programme une fonction peut être appelée, ou encore sur
des analyses de strictness ou de terminaison [10]. Ces méthodes ne retiennent aucune
information concernant les valeurs des variables numériques et ne permettent donc pas
de garantir l'absence de certaines erreurs à l'exécution. Plus récemment, Montagu et
al. [23] se sont intéressés aux relations entre les champs des types algébriques et Bautista
et al. [2, 3] à celles entre leurs valeurs, mais aucun ne supporte les types récursifs.

Enfin, comparés aux langages impératifs et orientés objets, sur lesquels sont développés la plupart des analyseurs abstraits [4, 6, 12, 29] à ce jour, les langages fonctionnels introduisent des défis nouveaux, rassemblés sur l'exemple suivant :

```h
type list = Cons of int * list | Nil
let rec mult2 l =
  match l with
  | Cons(h, q) -> Cons(2*h, mult2 q)
  | Nil -> Nil
  in
let hd x = match x with Cons(h,q) -> h | Nil -> assert false in
let x = Cons(0, Cons(1, Cons(2, Nil))) in
assert(hd (mult2 x) <= 4)
```

La fonction `mult2` multiplie par deux tous les éléments de la liste — définie par un type utilisateur — passée en argument, tandis que la fonction `hd` renvoie son premier élément (sa tête). L'objectif de notre analyse est d'être en mesure de prouver l'assertion et donc l'absence d'erreurs à l'exécution. Cela implique d'être capable d'analyser les types algébriques récursifs, les fonctions récursives et le filtrage par motifs. Ce travail fournit donc les contributions suivantes :

- Un domaine abstrait relationnel pour les objets algébriques récursifs, modulaire en le domaine numérique choisi, effectuant des résumés par champ.

- Une analyse de valeurs par interprétation abstraite pour un langage fonctionnel monomorphe du premier ordre capable d'analyser des fonctions récursives manipulant des objets récursifs et d'inférer leur relation entrée-sortie.

- Une implémentation en OCaml dans la plateforme MOPSA, en cours de développement et analysant avec succès de courts programmes écrits en OCaml.

**Plan.** La section 2 décrit le langage fonctionnel sur lequel nous travaillerons. Les méthodes d'analyse sont présentées et formalisées en section 3. La section 4 s'attarde
sur leur implémentation dans la plateforme MOPSA, tandis que la section 5 détaille l'état de l'art. La section 6 présente les extensions possibles et conclut.

## 2 Un langage fonctionnel

Dans cette partie, nous décrivons un langage fonctionnel jouet que nous chercherons à analyser dans les parties suivantes.

Alors que les langages impératifs manipulent majoritairement des données numériques, des structures ou encore des pointeurs, les langages fonctionnels utilisent quant à eux largement la notion de type algébrique (ou Algebraic Data Types, ADTs). Il s'agit d'un type formé par combinaison (sommes ou produits) d'autres types. Nous considérons ici des types algébriques de la forme suivante :

$$ \mathcal{T}_0 ::= \mathit{int} \mid (C_1 \ \mathit{of} \ \tau_{1,1} * \dots * \tau_{1,m_1} \mid \dots \mid C_n \ \mathit{of} \ \tau_{n,1} * \dots * \tau_{n,m_n}) \quad \text{avec } \tau_{i,j} \in \mathcal{T}_0 $$

$$ \mathcal{T} ::= d \in \mathcal{T}_0 \mid d_1 \to \dots \to d_n \to d_{n+1}, \quad \text{avec } \forall i, d_i \in \mathcal{T}_0 $$

Ainsi, un type est dans $\mathcal{T}_0$ s'il est le type int (type des entiers), ou s'il est un type algébriquement construit à partir de lui-même et des types de $\mathcal{T}_0$, c'est-à-dire sous la forme d'une somme de constructions $C_i$ of $\tau_{i,1} * \dots * \tau_{i,m_i}$, où les $C_i$ sont appelés constructeurs de type. Un type $t$ sous cette forme représente ainsi les objets s'écrivant sous la forme $C_i(e_{i,1}, \dots, e_{i,m_i})$, où $e_{i,j}$ est une expression de type $\tau_{i,j}$.

Ce type peut être vu comme la somme des types $C_i$ of $\tau_{i,1} * \dots * \tau_{i,m_i}$, eux-mêmes réalisant le produit de types $\tau_{i,1} * \dots * \tau_{i,m_i}$. Cette définition des types algébriques, proche de celle de OCaml, n'est pas une définition générale. En effet, une construction unique réunit ici deux constructeurs différents, la somme et le produit, de sorte à obtenir une syntaxe et une sémantique plus compacte. Par souci de simplification, nous ne considérerons pas les types mutuellement récursifs dans ce formalisme, mais tous les raisonnements menés s'y étendraient sans difficulté. De plus, notre analyse se limitera à un langage monomorphe du premier ordre, aussi les types $\tau_{i,j}$ ne peuvent pas être des fonctions, et les types algébriques polymorphes ne sont pas supportés.

L'ensemble $\mathcal{T}$ des types possibles est donc l'ensemble des types $d \in \mathcal{T}_0$, ainsi que le type des fonctions de $d_1, \dots, d_n$ dans $d_{n+1}$ avec $d_i \in \mathcal{T}_0$. On considérera désormais un programme préfacé par une liste de déclarations de types sous la forme $\text{type } t = C_1 \text{ of } \tau_{1,1} * \dots * \tau_{1,m_1} \mid \dots \mid C_n \text{ of } \tau_{n,1} * \dots * \tau_{n,m_n}$. Un type peut être algébriquement construit uniquement à base des types précédemment déclarés, du type int et de lui-même. On note $\mathbb{C}$ l'ensemble (fini) des constructeurs de type $C_i$ utilisés dans le programme. En posant $e_1, \dots, e_n \in \mathcal{E}, p_1, \dots, p_n \in \Pi, C \in \mathbb{C}$, nous nous munirons ici du langage « à la ML » dont la syntaxe est détaillée en figure 1.

Ici, $\mathbb{V}$ représente l'ensemble des variables, le symbole $\oplus$ les opérateurs du langage $(+, -, *, /, =, \dots)$, $fv(e)$ correspond aux variables libres de l'expression $e$. $\Pi$, l'ensemble des motifs (patterns), contient ainsi le joker `_`, les variables, les entiers, les clauses when, et les constructeurs de types dont les paramètres sont des motifs aux variables libres disjointes. $\perp_X$ symbolise la non-terminaison des expressions à valeur dans $X$. Les
$$
\mathcal{E} ::= x \in \mathbb{V}
$$

<table>
  <tr>
    <td>|<i>n</i> &isin; &Zopf;</td>
    <td>|<i>e</i><sub>1</sub> &oplus; <i>e</i><sub>2</sub></td>
  </tr>
  <tr>
    <td>|<i>e</i><sub>1</sub><i>e</i><sub>2</sub> . . . <i>e</i><sub><i>n</i></sub></td>
    <td>|fun <i>x</i><sub>1</sub> . . . <i>x</i><sub><i>n</i></sub> &rarr; <i>e</i></td>
  </tr>
  <tr>
    <td>|let <i>x</i> = <i>e</i><sub>1</sub> in <i>e</i><sub>2</sub></td>
    <td>|let rec <i>x</i> = <i>e</i><sub>1</sub> in <i>e</i><sub>2</sub></td>
  </tr>
  <tr>
    <td>|if <i>e</i><sub>1</sub> then <i>e</i><sub>2</sub> else <i>e</i><sub>3</sub></td>
    <td>|assert <i>e</i></td>
  </tr>
  <tr>
    <td>|<i>C</i>(<i>e</i><sub>1</sub>, . . . , <i>e</i><sub><i>n</i></sub>)</td>
    <td>|(match <i>e</i><sub>0</sub> with <i>p</i><sub>1</sub> &rarr; <i>e</i><sub>1</sub> | &hellip; | <i>p</i><sub><i>m</i></sub> &rarr; <i>e</i><sub><i>m</i></sub>)</td>
  </tr>
</table>

$$
\Pi ::= \_ | x \in \mathbb{V} | n \in \mathbb{Z} | p_1 \text{ when } e_1 | C(p_1, \dots, p_n), \text{ où } \forall i \neq j, fv(p_i) \cap fv(p_j) = \emptyset
$$

$$
\mathcal{V}_0 ::= \mathbb{Z}^{\perp} \cup \mathbb{C}(\mathcal{V}_0)^{\perp} \cup \{\omega\}^{\perp}, \text{ avec } \begin{cases} X^{\perp} = X \cup \{\perp_X\} \\ \mathbb{C}(X) = \{C(x_1, \dots, x_n) \mid C \in \mathbb{C}, x_i \in X\} \end{cases}
$$

$$
\mathcal{V} ::= \mathcal{V}_0 \cup \Lambda^{\perp} \quad \text{avec} \quad \Lambda = [\mathcal{V}_0^n \to \mathcal{V}_0]
$$

$$
\Sigma = \mathbb{V} \to \mathcal{V}
$$

<caption>Figure 1 – Syntaxe du langage fonctionnel.</caption>

valeurs de premier ordre du langage $\mathcal{V}_0$ sont les entiers, les constructeurs de types dont les arguments sont des valeurs de premier ordre et les erreurs $\omega$ auxquelles on adjoint $\perp$. L'ensemble des valeurs $\mathcal{V}$ se constitue ainsi de l'ensemble des valeurs du premier ordre ainsi que des fonctions continues des valeurs d'ordre 1 dans les valeurs d'ordre 1 ($\perp$ en cas de non-terminaison). Enfin, $\Sigma$ représente l'environnement, associant une valeur à chaque variable. La sémantique concrète du langage définie en Annexe A, figure 4.

Nous avons mentionné les types et leur déclaration au début de cette sous-section. Dans la suite, nous travaillerons sous l'hypothèse que nos programmes sont bien typés. L'inférence de type ne sera pas détaillée ici, mais fonctionne de la manière habituelle. Au cours de l'analyse, les informations sur les déclarations de types comme sur les types des variables seront utilisées pour sélectionner le domaine d'abstraction adéquat, en particulier pour les objets algébriques. De plus, cette inférence permet de détecter de manière statique certaines situations dans laquelle une expression s'évalue en $\omega$. Elle échoue cependant à détecter cette erreur lorsque celle-ci est déclenchée par un échec de filtrage (i.e. lorsque l'élément ne correspond à aucun motif), d'assertions ou de division par zéro. Ainsi, c'est sur de telles propriétés, portant sur la valeur des variables, que notre analyse se focalisera.

On notera que le type *int* correspond ici aux entiers mathématiques; cependant, travailler sur des entiers machines dans le cadre de l'analyse d'OCaml ne représente pas de difficulté supplémentaire majeure. Enfin, le langage défini n'encode pas toutes les caractéristiques des langages fonctionnels. L'ordre supérieur et le polymorphisme ne sont pas supportés, et ce langage est fonctionnel *pur*, ce qui signifie qu'il ne permet aucun effet de bord — ceci exclut en particulier l'utilisation des références et des tableaux. Ce langage contient ainsi les caractéristiques fonctionnelles sur lesquelles nous travaillerons, les fonctions et types algébriques récursifs. Cela permettra en particulier d'analyser les
fonctions récursives manipulant des structures de données récursives.

# 3 Formalisation des domaines

## 3.1 L'interprétation abstraite

Le domaine des valeurs et les opérateurs définissant la sémantique concrète du langage de la section 2 sont trop complexes à manipuler : les propriétés intéressantes sont incalculables. On utilise la théorie de l'interprétation abstraite [9], qui consiste à remplacer un domaine concret $C$ par un domaine abstrait plus simple, $A$, aux éléments représentables en mémoire, munis respectivement d'ordre partiels $\le$ et $\sqsubseteq$ correspondant au niveau d'information contenu dans les éléments.

Une fonction de concrétisation $\gamma : A \to C$ donne alors le sens d'un élément abstrait, en expliquant quel élément concret il peut représenter, et doit être compatible avec l'ordre d'information — croissante, donc. Pour $a \in A, c \in C, \gamma(a)$ est alors la concrétisation de $a$ dans $C$, et si $\gamma(a) \ge c$, alors $a$ est une approximation correcte de $c$.

Par exemple, dans un programme manipulant des valeurs numériques, chaque variable peut être représentée par l'ensemble de ses valeurs possibles, dans $P(\mathbb{Z})$, ordonné par l'inclusion. Cependant, cet ensemble étant de taille non bornée, son stockage et sa manipulation sont coûteux. En choisissant comme ensemble abstrait des intervalles de valeurs [8], on sur-approxime $P(\mathbb{Z})$ en un ensemble plus léger à manipuler. Par exemple, on peut abstraire $\{1, 3, 18, 37\}$ par $[1, 37]$.

Il s'agit ensuite d'être capable d'abstraire les opérateurs du concret, telle l'addition des entiers, en des opérateurs sur les éléments abstraits. Une *abstraction sûre* de $f : C \to C$ est alors une fonction $f^\sharp : A \to A$ telle que $\forall a \in A, f(\gamma(a)) \le \gamma(f^\sharp(a))$.

Enfin, pour interpréter des boucles, ou dans notre cas, des fonctions récursives, analyser chaque itération puis effectuer l'union des résultats possibles demande un nombre d'opérations arbitrairement grand, voire infini. On doit donc se munir d'un opérateur capable d'assurer la convergence de telles itérations, l'élargissement (*wide-ning*) $\nabla : A \times A \to A$, qui sur-approxime l'union et force la convergence dans $A$ en temps fini.

À partir de cette théorie, on trouve dans la littérature de nombreux domaines abstraits numériques abstrayant $P(\mathbb{Z}^n)$, avec différents compromis entre coût et précision (intervalles, octogones, polyèdres, etc.), dont certains sont relationnels — i.e. ils permettent de garder trace des relations entre les variables plutôt que de les abstraire indépendamment. Nous les exploiterons par la suite pour construire nos domaines pour les types algébriques.

## 3.2 Abstractions relationnelles avec des variables symboliques

Nous présentons ensuite les domaines abstraits utilisés pour définir une sémantique abstraite calculable $\mathbb{E}^\sharp$. Traditionnellement, une telle sémantique prend en paramètre une expression et renvoie une valeur abstraite dans le domaine pertinent. Cependant,
$$
\begin{align*}
\mathcal{E}_Z &::= n \in \mathbb{Z} \mid v \in \mathbb{V}_Z \mid e_1 \oplus e_2, \text{où } e_1, e_2 \in \mathcal{E}_Z \\
\mathcal{V}^\sharp &:= \mathcal{D} \cup \mathbb{V}_Z \\
\mathcal{E}^\sharp &:= \mathcal{D} \cup \mathcal{E}_Z \\
\Sigma^\sharp &:= (\mathbb{V} \to \mathcal{V}^\sharp) \times \mathcal{D}_Z
\end{align*}
$$

<caption>Figure 2 – Formalisation de la sémantique abstraite.</caption>

cette méthode ne garde pas trace des relations entre variables numériques.

En effet, une telle analyse interprétera sur le programme ci-contre x et y comme des valeurs abstraites et pourra inférer, dans le domaine des intervalles, x -> [1,10] et y -> [2,11], mais pas l'information relationnelle y = x + 1. Pour pallier cela, on choisit d'abstraire une expression numérique par une expression symbolique, qui peut contenir des variables, et un environnement abstrait adjoint à un domaine numérique, qui garde la relation entre ces variables. Ce principe est utilisé dans l'analyseur MOPSA [19], pour l'analyse de C et de Python, et permet aux expressions non-numériques d'exploiter la relationnalité de domaines abstraites tels les domaines numériques relationnel — relation entre tailles de chaînes de caractère, par exemple.

La figure 2 définit nos ensembles abstraits. En notant $\mathbb{V}_Z$ l'ensemble des variables représentant des entiers, $\mathcal{E}_Z$ est l'ensemble des expressions numériques, et contient donc des variables symboliques. On note ensuite $\mathcal{D}$ l'union des domaines des objets algébriques et des fonctions, définis par la suite, et $\mathcal{D}_Z$ un domaine abstrait numérique existant sur $\mathbb{V}_Z$ — tels les intervalles ou les polyèdres. En particulier, il peut être relationnel. $\mathcal{V}^\sharp$ correspond alors à l'ensemble des valeurs abstraites, où les valeurs numériques sont représentées par des variables, et $\mathcal{E}^\sharp$ à l'ensemble des expressions abstraites. On note enfin $\Sigma^\sharp$ l'environnement abstrait : le premier composant est une fonction des variables dans les valeurs abstraites, le second composant donne une valeur aux variables numériques, et notamment aux variables symboliques. On cherche dans cette partie à définir la sémantique abstraite $\mathbb{E}^\sharp[.]$. : $\mathcal{E} \times \Sigma^\sharp \to \mathcal{E}^\sharp \times \Sigma^\sharp$.

Enfin, on note $s[x \to v]$ l'association de la valeur $v \in \mathcal{V}^\sharp$ à la variable $x \in \mathbb{V}$ dans un environnement $s \in (\mathbb{V} \to \mathcal{V}^\sharp)$, et avec $\mathbb{E}_Z$ la fonction de transfert, supposée donnée, du domaine numérique, $\mathbb{E}_Z[v_x \leftarrow v]$ est l'association de la variable $v_x$ à une valeur ou une expression symbolique $v$ dans le domaine numérique. Elle renvoie un environnement abstrait dont la deuxième composante $d$ est mise à jour. On note $\sqcup_{\Sigma^\sharp}$ l'union sur les environnements. On définit alors l'association de $v \in \mathcal{V}^\sharp$ à $x \in \mathbb{V}$ dans $(s, d) \in \Sigma^\sharp$ :

$$
\forall (s, d) \in \Sigma^{\sharp}, (s, d)[x \to v] = \begin{cases} \mathbb{E}_Z[v_x \leftarrow v]((s[x \to v_x], d)) & \text{si } x : \text{int} \\ (s[x \to v], d) & \text{sinon} \end{cases}
$$

Lorsque $x$ est entière, on la représente par la variable $v_x$ dans $\mathbb{V} \to \mathcal{V}^\sharp$, avant d'ef-
fectuer l'assignation de $v_x$ à $v$ dans le domaine numérique. Sinon, on associe $x$ à $v$ dans $s$. Dans ce contexte, la sémantique abstraite de notre programme peut renvoyer : $(v_y, ([x \to v_x][y \to v_y], [1 \le v_x \le 10][v_y = v_x + 1]))$. La variable numérique $v_y$ correspondant à $y$ est alors bien en relation avec la variable numérique $v_x$ correspondant à $x$. On différencie ici la variable numérique $v_x$ sur la quantité numérique et la variable de programme $x$. Notons enfin que $\forall e \in \mathcal{E}, \mathbb{E}^{\sharp}[e] \emptyset = (\perp^{\sharp}, \emptyset)$. Par souci de simplification, on supposera par la suite que les erreurs sont propagées implicitement : si l'abstraction d'une sous-expression contient $\omega$, l'expression aussi.

## 3.3 Une abstraction pour les types algébriques

Les types algébriques sont fréquemment manipulés en programmation fonctionnelle — on peut citer le type des listes d'entiers simplement chaînées :

type list = Cons of int * list | Nil

On souhaite pouvoir analyser des programmes manipulant des objets de ce type. Plus généralement, on cherche à disposer d'un domaine spécialisé pour des objets dont le type est un type algébrique (potentiellement récursif) de la forme :

type $\tau = C_1$ of $\tau_{1,1} * \dots * \tau_{1,m_1}$ $| \dots | C_n$ of $\tau_{n,1} * \dots * \tau_{n,m_n}$

Bautista et al. [2, 3] s'intéressaient déjà aux types algébriques lorsque ceux-ci étaient non récursifs. À notre connaissance, aucun domaine visant à abstraire les valeurs prises par un type algébrique *récursif* n'a pour l'heure été créé. On note $C_{\tau} = \{C_i \mid 1 \le i \le m\}$ l'ensemble des constructeurs du type $\tau$ et $T_{\tau}$ l'ensemble des objets concrets *finis* de type $\tau$. Remarquons que ces objets sont cependant de taille non bornée, et $T_{\tau}$ peut être infini. On cherche à définir, pour le type $\tau_{i,j}$, un domaine abstrait $D_{i,j}^{\sharp}$ pour représenter tous les objets de type $\tau_{i,j}$ contenus dans le champ $j$ des constructeurs $C_i$ accessibles dans un objet de type $\tau$.

$$ D_{i,j}^{\sharp} = \begin{cases} \mathcal{P}(C_{\tau}) & \text{si } \tau_{i,j} = \tau \\ \mathbb{V}_{\mathbb{Z}} & \text{si } \tau_{i,j} = \text{int} \\ D_{\tau_{i,j}}^{\sharp} & \text{le domaine du type } \tau_{i,j} \text{ déjà défini sinon} \end{cases} $$

On cherche désormais à définir un ensemble abstrait pour l'ensemble concret $T_{\tau}$ :

$$ D_{\tau}^{\sharp} = \prod_{\substack{1 \le i \le m \\ 1 \le j \le n_i}} (D_{i,j}^{\sharp})^{\perp} \times \mathcal{P}(C_{\tau}) $$

Intuitivement, $D_{\tau}^{\sharp}$ abstrait un objet $x$ de type $\tau$ en un objet abstrait $(g, \mathscr{C})$, où :

- $g \in \prod(D_{i,j}^{\sharp})^{\perp}$ est tel qu'en notant $g_{i,j}$ l'élément de $(D_{i,j}^{\sharp})^{\perp}$ dans le tuple $g$, celui-ci abstrait toutes les valeurs du $j$-ième élément des constructeurs $C_i$ de $x$.

- $\mathscr{C} \in \mathcal{P}(C_{\tau})$ est l'ensemble des constructeurs $C_i$ possibles pour $x$.

On crée alors $x.i.j$ une variable numérique symbolique, qui représente toujours le champ $j$ des constructeurs $C_i$ accessibles dans $x$ lorsque celui-ci est entier. Ainsi, le domaine numérique peut inférer des relations entre ces variables. Remarquons alors que $D_{i,j}^{\sharp} \neq D_{\tau_{i,j}}^{\sharp}$ lorsque $\tau_{i,j} = \tau$ ou $\text{int}$.
**Exemple 3.1.** Dans le cas des listes d'entiers, en choisissant pour $D_Z$ l'ensemble des intervalles $I$, on a $C_{list} = \{\text{Cons}, \text{Nil}\}$, $D_{list}^{\#} = (V_Z^{\perp} \times \mathcal{P}(C_{list})^{\perp}) \times \mathcal{P}(C_{list})$. En effet, le constructeur **Cons** a deux champs : le premier contient des entiers, représenté par les variables numériques $V_Z$ — associées dans un environnement $\sigma$ à des éléments de $I$ — et le second, récursif, des listes, donc représenté par $\mathcal{P}(C_{list})$. Pour un objet $x$, $x.1.1$ représente alors le champ 1 du premier constructeur, donc le champ **int** de **Cons**. Un objet de $D_{list}^{\#}$ serait $((r.1.1, \{\text{Cons}, \text{Nil}\}), \{\text{Cons}\}) \in D_{list}^{\#}$, avec $[r.1.1 \to [1, 10]] \in \sigma$.

L'étape suivante est de définir la concrétisation $\gamma_{\tau}$ qui à un objet abstrait de $D_{\tau}^{\#}$ dans un environnement abstrait associera un ensemble d'objets concrets de $\mathcal{T}_{\tau}$ pouvant lui correspondre. On note $\gamma_{\tau_{i,j}}$ la concrétisation associée au domaine de $\tau_{i,j}$ lorsque $\tau_{i,j} \neq \tau$.

**Définition 3.1.** Pour $(g, \mathscr{C}) \in D_{\tau}^{\#}, \sigma^{\#}$ un environnement abstrait, on a la concrétisation :

$$ \gamma_{\tau}((g, \mathscr{C}), \sigma^{\#}) = \{ x : \tau \mid x = C_i(x_{i,1}, \dots, x_{i,n_i}) \wedge C_i \in \mathscr{C} \wedge \\ \forall j, x_{i,j} \in \left\{ \begin{array}{ll} \gamma_{\tau}((g, g_{i,j}), \sigma^{\#}) & \text{si } \tau_{i,j} = \tau \\ \gamma_{\tau_{i,j}}(g_{i,j}, \sigma^{\#}) & \text{sinon} \end{array} \right. \} $$

Lorsque le type $\tau$ est fini, la récursion est bien fondée ($x_{i,j}$ contient strictement moins de constructeurs que $x$) et cette définition est correcte.

Intuitivement, un objet $x$ de type $\tau$ peut alors être abstrait par $(g, \mathscr{C})$ si :

- Il s'écrit à partir d'un constructeur $C_i$ de $\mathscr{C}$.

- Chaque $j$-ième champ de constructeur $C_i$ accessible dans $x$ a :

- son constructeur dans $g_{i,j}$, quand il est récursif ($\tau_{i,j} = \tau$);

- ou peut être abstrait par $g_{i,j}$ s'il est non récursif.

Ainsi, $g_{i,j}$ représente donc un résumé de tous les champs $j$ de constructeur $C_i$ accessibles dans $x$. L'environnement en paramètre permet de garder trace des variables numériques.

Un objet d'un type récursif étant de taille non bornée, il s'agit ici d'obtenir un domaine abstrait permettant de le représenter de manière finie. Pour ce faire, on « replie » chaque champ de constructeurs en un résumé, de sorte à ne mémoriser qu'une variable résumé pour chacun d'eux. Cette approche comporte des similitudes avec l'idée de Go-pan et al. [14] qui proposait d'utiliser un nombre fixé de dimensions pour sur-approximer les valeurs d'une collection non bornée d'objets numériques, dans le cadre d'analyses de tableaux dynamiques ou de structures allouées sur le tas. Remarquons que le « résumé » ou « repliement » est effectué au site d'allocation de la variable de type algébrique — l'abstraction est dite *object-sensitive* [28].

**Exemple 3.2.** Dans le cas des listes, en notant $(g, \mathscr{C}) = ((r, \{\text{Cons}, \text{Nil}\}), \{\text{Cons}\})$ et $\sigma^{\#} = [r \to [1, 10]]$, la concrétisation $\gamma_{list}((g, \mathscr{C}), \sigma^{\#})$ vaut :

$$ \{ x : \text{list} \mid x = \text{Cons}(h, q), q \in \gamma_{\text{list}}(((r, \{\text{Cons}, \text{Nil}\}), \{\text{Cons}, \text{Nil}\}), \sigma^{\#}) \wedge h \in [1, 10] \} $$

En particulier, $\text{Cons}(1, \text{Cons}(4, \text{Cons}(10, \text{Nil}))) \in \gamma_{list}((( [1, 10], \{\text{Cons}, \text{Nil}\}), \{\text{Cons}\}), \sigma^{\#})$, ce qui signifie que $((r, \{\text{Cons}, \text{Nil}\}), \{\text{Cons}\})$ est une sur-approximation correcte de
Cons(1, Cons(4, Cons(10, Nil))) dans $\sigma^\sharp$. De manière générale, c'est une sur-approximation correcte pour toutes les listes non vides dont les éléments sont dans [1, 10].

Pour définir un domaine abstrait, on doit également se munir d'une relation d'ordre entre les éléments de $\mathcal{D}_\tau^\sharp$.

**Définition 3.2.** On note $\sqsubseteq_{i,j}^\perp$ l'ordre plat sur $\mathcal{D}_{i,j}^{\sharp,\perp}$. On définit ensuite l'opérateur $\sqsubseteq$ :

$$ (g^1, \mathcal{C}_1) \sqsubseteq (g^2, \mathcal{C}_2) \iff \mathcal{C}_1 \subseteq \mathcal{C}_2 \land (\forall 1 \le i \le n, C_i \in \mathcal{C}_1 \Rightarrow \forall 1 \le j \le m_i, g_{i,j}^1 \sqsubseteq_{i,j}^\perp g_{i,j}^2) $$

**Exemple 3.3.** Pour les listes, $((x.1.1, \mathcal{C}_1), \mathcal{C}_1') \sqsubseteq ((y.1.1, \mathcal{C}_2), \mathcal{C}_2') \iff \mathcal{C}_1' \subseteq \mathcal{C}_2' \land \mathcal{C}_1 \subseteq \mathcal{C}_2 \land x.1.1 \sqsubseteq_\mathbb{I} y.1.1$. Par exemple, $((x.1.1, \{\mathbf{Nil}\}), \{\mathbf{Cons}\}) \sqsubseteq ((y.1.1, \{\mathbf{Cons}, \mathbf{Nil}\}), \{\mathbf{Cons}\})$ si $x.1.1 \to [1, 4]$ et $y.1.1 \to [1, 10]$. $x.1.1$ et $y.1.1$ représentent les valeurs numériques dans les listes d'entiers $x$ et $y$.

On construit maintenant une abstraction $\cup_\tau^\sharp$ sûre pour $\cup$ :

$$ (g^1, \mathcal{C}_1) \cup_\tau^\sharp (g^2, \mathcal{C}_2) = (g, \mathcal{C}_1 \cup \mathcal{C}_2) \quad \text{avec } \forall i \le n, \forall j \le m_j, g_{i,j} = g_{i,j}^1 \cup_{\mathcal{D}_{i,j}} g_{i,j}^2 $$

On définit l'élargissement de la même manière, en remplaçant $\cup_\tau^\sharp$ et $\cup_{\mathcal{D}_{i,j}}$ par $\nabla_\tau$ et $\nabla_{\mathcal{D}_{i,j}}$. On définit de même l'intersection abstraite. Les preuves de sûreté sont fournies en annexe D.1 et D.2. Il s'agit ensuite de définir les fonctions de transfert pour la construction d'objets de type algébrique, c'est-à-dire, étant donné un environnement abstrait $\sigma^\sharp$ et une expression concrète $C_k(e_1, \dots, e_n)$, en calculer une abstraction $(g, \mathcal{C})$ dans un nouvel environnement abstrait. Pour ce faire, on utilise un label syntaxique frais $r$ pour l'expression et les $r.i.j$ sont alors des variables fraîches résumant le champ entier du $j$-ème élément du constructeur $i$, dont la valeur $h_{i,j}$ est stockée dans l'environnement.

$$ \mathbb{E}^{\sharp} [ C_k(e_1, \dots, e_n)^r ] \sigma^{\sharp} = (g, \{C_k\}), \sigma_0^{\sharp}[\forall i \le n, j \le m_i, r.i.j \to h_{i,j}] \quad \text{avec} \\ \left\{ \begin{array}{l} v_i, \sigma_i^{\sharp} = \mathbb{E}^{\sharp}[[e_i]]\sigma^{\sharp} \\ (g^0, \mathcal{C}) = \bigcup_{e_i:\tau}^{\sharp} v_i \\ \sigma_0^{\sharp} = \bigcup_i^{\Sigma_i^\sharp} \sigma_i^{\sharp} \end{array} \right. \qquad h_{i,j} = \left\{ \begin{array}{ll} g_{k,j}^0 \cup_{\mathcal{D}_{k,j}} v_j & \text{si } i=k \\ g_{i,j}^0 & \text{sinon} \end{array} \right. \qquad g_{i,j} = \left\{ \begin{array}{ll} r.i.j & \text{si } \tau_{i,j} = \text{int} \\ h_{i,j} & \text{sinon} \end{array} \right. $$

L'idée est la suivante : la sémantique abstraite de $C_k(e_1, \dots, e_n)$ est un objet $x$ du domaine $\mathcal{D}_\tau^\sharp$. Le seul constructeur possible pour cet objet est $C_k$. On abstrait ensuite ses champs de la manière suivante, dans la variable $g$ : on note $(g^0, \mathcal{C})$ l'union abstraite des évaluations de tous ses champs récursifs — les $e_i$ de type $\tau$. De la sorte, le champ $g_{i,j}^0$ représente l'union de tous les contenus des champs $j$ des $C_i$ accessibles depuis l'objet $x$.

On définit $g$ en définissant ses composantes $g_{i,j}$, censées représenter tous les objets dans un champ $j$ de constructeur $C_i$ accessibles dans $x$ :

- Si $g_{k,j}$ correspond à un champ non récursif de $C_k$ : il vaut l'union de tous les champs $j$ des $C_k$ accessibles, c'est-à-dire l'union de la sémantique abstraite de $e_j$ — un champ $j$ de $C_k$ — avec $g_{k,j}^0$ — résumé de tous les autres champs $j$ des $C_k$.
— Sinon : tous les objets dans un champ *j* de constructeur $C_i$ sont accessibles uniquement via les champs récursifs, et donc résumés dans $g_{i,j}^0$.

Les champs $g_{i,j}$ de type `int` sont alors effectivement assignés à la variable `r.i.j`, de valeur $h_{i,j}$ dans l'environnement. Cette indirection permet, dans le cas où $D_Z$ est relationnel, d'obtenir des relations entre les `r.i.j`, comme illustré dans l'exemple 3.6. On remarque ainsi que ce domaine s'appuie largement sur les domaines numériques. Sa preuve de sûreté est fournie en annexe D.3.

**Exemple 3.4.** Ainsi, on peut écrire

$$ \mathbb{E}^{\#}[\text{Nil}]\sigma^{\#} = ((r.1.1, \perp), \{\text{Nil}\}), \sigma^{\#}[r.1.1 \to \perp] $$

$$ \mathbb{E}^{\#}[\text{Cons}(10, \text{Nil})]\sigma^{\#} = ((r.1.1, \{\text{Nil}\}), \{\text{Cons}\}), \sigma^{\#}[r.1.1 \to \perp \cup \mathbb{I}[10, 10]] $$

$$ \mathbb{E}^{\#}[\text{Cons}(1, \text{Cons}(10, \text{Nil}))]\sigma^{\#} = (r.1.1, \{\text{Nil}\} \cup \{\text{Cons}\}), \{\text{Cons}\}), \sigma^{\#}[x \to [1, 10]] $$

On remarque ici qu'on utilise largement les informations de type du programme. En effet, le type des champs `i,j` (`t` ou `int`, par exemple) guide l'abstraction en renvoyant la gestion des champs vers les domaines pertinents; pour ce faire, il est nécessaire de connaître la définition du type `t`. On repose donc très fortement sur l'hypothèse que le programme analysé est bien typé.

**Exemple 3.5.** On peut illustrer l'utilisation de ce domaine abstrait :

```hml
type tree = Node of tree * int * tree | Leaf of int
let x = Node(Node(Leaf(250), 100, Leaf(251)), 1, Leaf(252))
```

Dans ce contexte, $\mathbb{E}^{\#}[\text{Node}(\text{Node}, (\text{Leaf}(250), 100, \text{Leaf}(251)), 1, \text{Leaf}(252))][ ]$ vaut donc $(g, \mathscr{C}) = ((\{\text{Node}, \text{Leaf}\}, x.1.2, \{\text{Leaf}\}, x.2.1), \{\text{Node}\})$ dans l'environnement $\sigma^{\#} = ([v_{x.1.2} \to x.1.2][v_{x.2.1} \to x.2.1], [v_{x.1.2} \to [1, 100]] [v_{x.2.1} \to [250, 252]])$.

$$ \gamma((g, \mathscr{C}), \sigma^{\#}) = \{x \mid x = \text{Node}(t_1, n, t_2) \wedge n \in [1, 100] \wedge t_1 \in \gamma((g, \{\text{Node}, \text{Leaf}\})) \\ t_2 \in \gamma((g, \{\text{Leaf}\}))\} $$

Cela correspond à l'ensemble des arbres construits à partir de `Node` et poussant uniquement vers la gauche, dont les entiers des constructeurs `Leaf` sont entre 250 et 252 et ceux de `Node` entre 1 et 100.

Cet exemple permet de constater qu'une telle analyse perd beaucoup en précision dans des programmes simples. On pourrait par exemple souhaiter pouvoir garder trace du contenu exact de `x` dans un tel exemple, et ne pas effectuer de résumé des champs. Une proposition pour améliorer la précision de l'analyse décrite ci-dessus serait de n'effectuer un résumé d'un champ que lorsque nécessaire pour la convergence, i.e. lors d'une boucle ou d'un appel récursif, ou encore uniquement à partir d'une certaine profondeur `n` de l'objet. De telles améliorations n'ont pas encore été implémentées.
Cet exemple permet également de voir que bien qu'ils soient de mêmes types, le deuxième champ du constructeur **Node** est résumé dans une variable différente que le champ du constructeur **Leaf**. Cela permet de gagner en précision, notamment lorsque ces champs revêtent des significations différentes.

**Exemple 3.6.** L'analyse est également capable d'inférer des propriétés relationnelles :

```hml
let z = Cons(a, Nil) in
let x = if y <= 2*a + 1 then Cons(y, z) else Cons(2 * a + 1, z)
```

En choisissant comme domaine numérique le domaine des polyèdres [7], on est ici en mesure de prouver : $x_{1,1} \le 2a + 1$. Cela signifie que toutes les éléments de la liste sont inférieurs à $2a + 1$. Cet aspect relationnel est crucial dans l'inférence des relations entrées-sorties des fonctions (section 3.5), effectuée sans information sur les arguments.

## 3.4 Abstraction du filtrage par motifs

On s'intéressera ici à la fonction de transfert du filtrage par motifs. Celles des autres constructions du langage sont très standard et sont détaillées en Annexe B. Pour ce faire, on se munit de la fonction abstraite **match**<sup>‡</sup> : $V^{‡} \times \Sigma^{‡} \times \Pi \rightarrow \Sigma^{‡} \times \Sigma^{‡}$, détaillée en Annexe C.3. Elle prend en paramètre une valeur abstraite $e$, un environnement abstrait $\sigma^{‡}$, et un motif $p$, et renvoie un environnement abstrait restreint dans lequel $p$ et $e$ correspondent, et un dans lequel ils ne correspondent pas. On utilise pour ce faire la fonction de filtre $\mathcal{F}^{‡}$, fournie par le domaine numérique : étant donnée une expression numérique et un environnement abstrait, elle restreint cet environnement abstrait de sorte que l'expression numérique en paramètre soit non nulle. Par exemple, cela permet d'écrire lorsque le motif s'écrit $p$ when $e_1$ :

$$ \mathit{match}^{\mathit{‡}}(\sigma^{\mathit{‡}}, v^{\mathit{‡}}, p \text{ when } e_1) = \mathcal{F}^{\mathit{‡}}[e_1^n = 0] \sigma_1^{\mathit{‡}}, \sigma_{-1,0}^{\mathit{‡}} \text{ avec } \begin{cases} \mathit{match}^{\mathit{‡}}(\sigma^{\mathit{‡}}, v^{\mathit{‡}}, p) = \sigma_0^{\mathit{‡}}, \sigma_{-1,0}^{\mathit{‡}} \\ \mathbb{E}^{\mathit{‡}}[e_1] \sigma_0^{\mathit{‡}} = e_1^n, \sigma_1^{\mathit{‡}} \end{cases} $$

Ainsi, $v^{\mathit{‡}}$ et $p$ when $e_1$ correspondent dans l'environnement où $v^{\mathit{‡}}$ et $p$ correspondent, restreint au cas où $e_1^n$ est non nul.

$$ \mathbb{E}^{\mathit{‡}}[\mathit{match} \ e_0 \ \mathit{with} \ p_1 \to e_1 \ | \ \dots \ | \ p_m \to e_m] \sigma^{\mathit{‡}} = \begin{cases} \mathbb{E}^{\mathit{‡}}[e_1] \sigma_1^{\mathit{‡}} \cup \mathbb{E}^{\mathit{‡}}[e'_1] \sigma_{-1,1}^{\mathit{‡}} & \text{si } m \ge 1 \\ \{\omega\}, \sigma^{\mathit{‡}} & \text{si } m = 0 \end{cases} $$

$$ \text{avec } \begin{cases} \sigma_1^{\mathit{‡}}, \sigma_{-1,1}^{\mathit{‡}} = \mathit{match}^{\mathit{‡}}(\mathbb{E}^{\mathit{‡}}[e_0] \sigma^{\mathit{‡}}, p_1) \\ e'_1 = \mathit{match} \ e_0 \ \mathit{with} \ p_2 \to e_2 \ | \ \dots \ | \ p_m \to e_m \end{cases} $$

L'interprétation du filtrage de motif est l'union abstraite des interprétations $e_i$ dans un environnement dans lequel $e_i$ correspond au motif $p_i$ mais pas aux motifs $p_j$ avec $j < i$, $\{\omega\}$ si $e_0$ ne correspond à aucun motif. Cela correspond à l'intuition que l'expression $e_0$
est comparée successivement aux différents motifs, jusqu’à la première correspondance. On remarque qu’on renvoie une erreur lorsqu’après lecture du dernier motif, on analyse un filtrage sans motif dans un environnement non vide : cela correspond au cas où il reste des environnements possibles n’ayant été filtrés par aucun motif. Ainsi, notre analyse cible les échecs de filtrage, d’assertions, de division par zero et de dépassements d’entier — si le domaine numérique les traite. Les autres erreurs sont déjà évitées par le typage. La preuve de sûreté pour ces fonctions de transfert est fournie en Annexe D.3.

**Exemple 3.7.** Sur un exemple manipulant la structure de filtrage de motifs :

```h
let x = match Cons(1, Nil) with
  | Cons(h, q) -> h
  | Nil -> 0
  in assert (x = 1)
```

Informellement, on obtient comme abstraction $\mathbb{E}^{\#}[\text{Cons}(h, q)]\sigma_1^{\#} \cup^{\#} \mathbb{E}^{\#}[\text{Nil}]\sigma_{-1}^{\#}$ avec $\sigma_1^{\#} = [h \to 1]$ et $\sigma_{-1,1}^{\#} = \emptyset$. Le résultat sera donc $h \cup^{\#} \perp^{\#} = h$ dans l'environnement $[h \to 1]$.

Ainsi, on est en mesure d'inférer que $x = 1$ et l'assertion est donc prouvée correcte.

## 3.5 Fonctions récursives

Les fonctions récursives sont un incontournable des langages à la ML tel OCaml. Nous avons choisi ici de représenter les fonctions du premier ordre par des relations entre les variables d'entrées et la sortie, en se reposant donc sur un domaine relationnel pour inférer les relations d'entrée-sortie. Le langage étant pur, celles-ci correspondent simplement à l'état relationnel à la fin de la fonction, réduit aux arguments et à la valeur de retour. On s'intéresse aux fonctions de type $\tau = \tau_1 \to \dots \to \tau_{n+1}$ avec $\tau_1, \dots, \tau_{n+1} \in \mathcal{T}_0$. On note $\mathcal{D}_i^{\#}$ le domaine choisi pour représenter $\tau_i$.

**Définition 3.3.** On note $\mathcal{D}_i^f = \mathcal{P}(\mathbb{V}) \times \mathcal{E}^{\#} \times \Sigma^{\#}$ le domaine choisi pour représenter les fonctions de type $\tau$. On considère alors la concrétisation :

$$ \gamma_f(x_1, \dots, x_n, e^{\#}, \sigma^{\#}) = \{ f : \tau \mid \forall v_1 : \tau_1, \dots, v_n : \tau_n, \forall a_1 \in \mathcal{D}_1^{\#}, \dots, a_n \in \mathcal{D}_n^{\#}, \forall i, \\ v_i \in \gamma(a_i, \sigma^{\#}) \wedge f(v_1, \dots, v_n) \in \gamma(e^{\#}, \sigma^{\#}[x_1 = a_1, \dots, x_n = a_n]) \} $$

Ainsi, une fonction est abstraite par : le nom $x_1, \dots, x_n$ de tous ses arguments formels, la valeur abstraite de son résultat $e^{\#}$, et l'environnement $\sigma^{\#}$ dans lequel ce résultat est valide. Lorsqu'elle est appliquée à des arguments réels de valeurs $v_i$ abstraites par $a_i$, on ajoute dans l'environnement les contraintes d'égalité entre les arguments $x_i$ et les $v_i$. On définit ensuite les fonctions de transfert :

$$ \begin{gather*} \mathbb{E}^{\#}[\text{fun } x_1 \cdots x_n \to e_1]\sigma^{\#} = (x_1, \dots, x_n, \mathbb{E}^{\#}[e_1]\sigma^{\#}[x_1 \to \top, \dots, x_n \to \top]), \sigma^{\#} \\ \mathbb{E}^{\#}[\text{let rec } f = e_1 \text{ in } e]\sigma^{\#} = \mathbb{E}^{\#}[e]\sigma^{\#}[f \to \bigvee_{n \in \mathbb{N}} F^n((x_1, \dots, x_k, \bot, \sigma^{\#}[\forall i \le k, x_i \to \top]))] \end{gather*} $$

$$ \text{avec } F(v^{\#}) = \text{fst}(\mathbb{E}^{\#}[e_1]\sigma^{\#}[f \to v^{\#}]), f : \tau, \tau = \tau_1 \to \dots \to \tau_k \to \tau_{k+1} $$

$$ \mathbb{E}^{\#}[e_0 \dots e_n]\sigma^{\#} = e^{\#}, \sigma_n^{\#}[x_1 = e_1^{\#}, \dots, x_n = e_n^{\#}], \quad \text{avec} \quad \begin{cases} \mathbb{E}^{\#}[e_0]\sigma^{\#} = (x_1, \dots, x_n, e^{\#}, \sigma_0^{\#}), \\ \mathbb{E}^{\#}[e_{i+1}^{\#}]\sigma_i^{\#} = e_{i+1}^{\#}, \sigma_{i+1}^{\#} \end{cases} $$
Pour les fonctions définies récursivement, l'intuition est la suivante. On souhaite
réaliser une analyse modulaire de la fonction. Pour analyser le corps de la fonction, on
considère donc les valeurs des arguments initialisées à $\top$, le maximum du domaine. En
effet, pour obtenir la relation entrée-sortie la plus générale possible, on doit supposer
les arguments quelconques. De la sorte, on peut appliquer le résumé obtenu à chaque
appel, sans contrainte sur la valeur des arguments. Lorsque la fonction est récursive,
on cherche à sur-approximer le plus petit point fixe de la sémantique concrète. Par le
théorème de Kleene, calculer ce point fixe correspond à itérer l'analyse en débutant
à $f \to \bot$. Dans l'abstrait, on procède de même, mais en réalisant un élargissement,
ou *widening*, noté $\nabla_\tau$, pour assurer la convergence. Enfin, l'application $e_0...e_n$ de la
fonction $e_0$ aux arguments $e_1, ..., e_n$ ajoute les contraintes d'égalités entre les arguments
$x_i$ par l'interprétation abstraite des arguments $e_i$, dans l'environnement du résultat de
la fonction enrichie par les informations obtenues par abstraction des $e_j$ précédents.

On choisit ici d'effectuer l'analyse d'une fonction dès sa déclaration. En effet, cela
permet de ne l'analyser qu'une fois, et d'en instancier le résultat à chaque site d'appel
selon les valeurs des paramètres. Cela permet une analyse plus efficace. Dans le cas
de fonctions mutuellement récursives, non mentionnées ici, notre raisonnement s'étend
sans difficulté en itérant sur un vecteur d'abstractions de fonctions.

En notant $\mathcal{A}$ l'ensemble des types algébriques, $\mathcal{D}$ l'union des domaines d'objets algébriques et des domaines de fonctions est alors $\mathcal{D} = \bigcup_{\tau \in \mathcal{A}} \mathcal{D}_{\tau}^{\sharp} \cup \bigcup_{\tau=\tau_1 \to \dots \to \tau_n} \mathcal{D}_{\tau}^{f}$. Pour obtenir notre domaine abstrait global, on définira l'union $\cup^{\sharp}$ sur $\mathcal{E}^{\sharp} \times \Sigma^{\sharp}$ en Annexe C.2 et de la concrétisation $\gamma: \mathcal{E}^{\sharp} \times \Sigma^{\sharp} \to \mathcal{V}$. Sous certaines conditions, il existe une correspondance de Galois (annexe E).

**Exemple 3.8.** Cependant, cette méthode peut induire une perte de précision :

let rec binary = fun x -> if x > 0 then 10 else -10 in binary 1

Ici, notre analyse est en mesure de déduire, en analysant **binary** à sa déclaration, qu'étant donnée une entrée quelconque, elle renvoie une valeur dans l'intervalle [-10, 10]. Ainsi, on sait que la valeur de **binary 1** est entre -10 et 10. On aurait pu obtenir un résultat plus précis en analysant le corps de **binary** sachant que l'argument **x** valait 1, ou qu'il était strictement supérieur à 0.

On pourrait également choisir de ne pas être modulaire et d'effectuer cette analyse
pour des arguments connus. Ainsi, il suffit de les initialiser non pas à $\top$ mais à leur va-
leur abstraite. On réalise une analyse identique par élargissement, en se donnant cette
fois la possibilité de réaliser des élargissements sur les arguments si les appels récursifs
élargissent leur domaine. On pourrait même adapter la méthode de partitionnement,
développée par Bourdoncle [5] pour un langage récursif impératif : la fonction est ana-
lysée pour plusieurs valeurs abstraites couvrant les arguments d'entrée. Cette méthode
permet de gagner en précision sans pour autant analyser ou spécialiser la fonction à
chaque appel. Cette implémentation serait l'objet d'un travail futur.
Enfin, l'hypothèse d'un fragment pur est essentielle ici. En effet, une fonction est abstraite comme une relation entre les variables d'entrée et la variable de sortie : cette abstraction est permise puisque la fonction ne réalise aucune modification de l'état mémoire. Dans un fragment impur, contenant tableaux, références ou champs mutables, il serait nécessaire de modifier cette abstraction de sorte à garder trace des modifications de l'état mémoire. Des pistes pour travaux futurs seront résumées en section 6.

## 3.6 Exemple d'application

Détaillons l'analyse en calculant la sémantique abstraite de l'exemple introductif :

```h
let rec mult2 = fun l -> match l with
  | Cons(h, q) -> Cons(2*h, mult2 q) | Nil -> Nil in
let hd = fun y -> match y with Cons(h,q) -> h | Nil -> 0 in
let x = Cons(0, Cons(1, Cons(2, Nil))) in assert(hd(mult2 x) <= 4)
```

On note $body = match l with | Cons(h, q) \to Cons(2 * h, mult2 q) | Nil \to Nil$. On calcule alors $\nabla_{n \in \mathbb{N}} F^n((l, \perp, \sigma^\#))$, où $\sigma^\# = [l \to \top]$ puisque $l$ est quelconque. Enfin, on note $r$ l'identifiant unique pour le résultat de $body$. Comme l'analyse est générique en le domaine $D_Z$ choisi pour représenter les entiers, les opérateurs $+$, $-$, $*$ le sont aussi.

$$F((l, \perp, \sigma^\#)) = \mathbb{E}^\#[\text{fun } l \to \text{body}] \sigma^\#[\text{mult2 } (l, \perp, \sigma^\#)] \\ = (l, ((r.1.1, \perp), \{\text{Cons}\}, \sigma^\#[r.1.1 \to 2 * l.1.1]))$$

$$\cup_\tau^\# ((r.1.1, \perp), \{\text{Nil}\}), \sigma^\#[r.1.1 \to \perp]) \\ = (l, (r.1.1, \perp), \{\text{Cons}, \text{Nil}\}, \sigma^\#[r.1.1 \to 2 * l.1.1])$$

$$F^2((l, \perp, \sigma^\#)) = F((l, (r.1.1, \perp), \{\text{Cons}, \text{Nil}\}, \sigma^\#[r.1.1 \to 2 * l.1.1]))$$

$$= (l, (r.1.1, \{\text{Cons}, \text{Nil}\}), \{\text{Cons}, \text{Nil}\}), \sigma^\#[r.1.1 \to 2 * l.1.1])$$

$$F^3((l, \perp, \sigma^\#)) = F^2((l, \perp, \sigma^\#))$$

$$\nabla_{n \in \mathbb{N}} F^n((l, \perp, \sigma^\#)) = (l, (r.1.1, \{\text{Cons}, \text{Nil}\}), \{\text{Cons}, \text{Nil}\}), \sigma^\#[r.1.1 \to 2 * l.1.1]) = V_1$$

Par raffinement successif du résumé de la fonction, on est capable d'inférer que la variable résumé des éléments de la liste de retour $(r.1.1)$ vaut deux fois la variable résumé des éléments de la liste d'entrée $(l.1.1)$. Ainsi, si $D_Z$ est le domaine des intervalles et que les éléments de la liste d'entrée sont dans $[a, b]$, alors ceux de la liste de retour sont dans $[2a, 2b]$. On associe ensuite ce résultat à `mult2` et on poursuit l'analyse de $e$ :

$$\mathbb{E}^\#[\text{let rec } mult2 = \text{body in } e] \sigma^\# = \mathbb{E}^\#[e] \sigma^\# \sigma_1^\# \quad \text{avec } \sigma_1^\# = \sigma^\#[mult2 \to V_1]$$
Puis on évalue $body_2 = match x$ with $| Cons(h, q) \to h | Nil \to 0$, qu'on associe à $hd$.

$$ 
\begin{aligned}
\mathbb{E}^{\#}[\text{fun } y \to body_2]\sigma_1^{\#} &= (y, \mathbb{E}^{\#}[body_2]\sigma^{\#}[y \to \top]), \sigma_1^{\#} \\
&= (y, z, \sigma^{\#}[z \to y.1.1 \cup \mathbb{Z} \ 0]), \sigma_1^{\#} = V_2,
\end{aligned}
$$

$$ \mathbb{E}^{\#}[\text{let } hd = body_2 \text{ in } e_1]\sigma_1^{\#} = V_2, \sigma_2^{\#} \quad \text{où } \sigma_2^{\#} = \sigma_1^{\#}[hd \to V_2] $$

Ainsi, $hd$ renvoie $z$, dont la valeur est le résumé du premier champ de **Cons** pour $l$ (l.1.1) joint à 0. Enfin, on calcule l'abstraction de $x$.

$$ 
\begin{aligned}
\mathbb{E}^{\#}[\text{Cons}(0, \text{Cons}(1, \text{Cons}(2, \text{Nil})))]\sigma_2^{\#} &= ((r_2.1.1, \{\text{Cons}, \text{Nil}\}), \{\text{Cons}\}), \sigma_3^{\#}) \\
&= V_3, \sigma_3^{\#} \quad \text{où } \sigma_3^{\#} = \sigma_2^{\#}[r_2.1.1 \to 0 \cup \mathbb{Z} \ 1 \cup \mathbb{Z} \ 2])
\end{aligned}
$$

$$ \mathbb{E}^{\#}[\text{let } x = \text{Cons}(0, \text{Cons}(1, \text{Cons}(2, \text{Nil}))) \text{ in } e_2]\sigma_2^{\#} = \mathbb{E}^{\#}[e_2]\sigma_2^{\#}, \sigma_4^{\#} \quad \text{où } \sigma_4^{\#} = \sigma_3^{\#}[x \to V_3] $$

Puis on analyse l'assertion en applicant successivement $mult2$ et $hd$ à $x$ :

$$ 
\begin{aligned}
\mathbb{E}^{\#}[\text{mult2 } x]\sigma_4^{\#} &= V_1, \sigma_4^{\#}[l \to \sigma_4^{\#}(x)] \\
\mathbb{E}^{\#}[hd (\text{mult2 } x)]\sigma_4^{\#} &= z_1, \sigma_4^{\#}[l \to \sigma_4^{\#}(x)][y \to V_1][z_1 \to z]
\end{aligned}
$$

$z$ est la variable résultat de $body_2$, et $z_1$ est l'interprétation abstraite de l'expression testée par l'assertion. Avec le domaine des polyèdres, on a alors :

$$ 0 \le x.1.1 \le 2 \land l.1.1 = x.1.1 \land V_1.1.1 \le 2*l.1.1 \land y.1.1 = V_1.1.1 \land 0 \le z \le y.1.1 \land z_1 = z $$

On déduit $0 \le V_1.1.1 \le 4$, puis $0 \le z_1 \le 4$. Ainsi, le programme est prouvé correct.

# 4 Implémentation et expérimentation

## 4.1 La plateforme MOPSA

L'implémentation s'est effectuée dans MOPSA (Modular Open Platform for Static Analysis) [19], une plateforme en logiciel libre et multi-langage visant à faciliter le développement d'analyseurs statiques par interprétation abstraite.

Elle se différencie des analyseurs statiques existants, tels Astrée [4], Frama-C [6], Infer [12] ou Julia [29] en ce qu'elle tente de combiner des analyses relationnelles basées sur la coopération de domaines abstraits indépendants les uns des autres avec une plateforme modulaire non spécifique à un langage. Elle implémente des analyses ciblant du code écrit en C, en Python, ou mêlant du C et du Python. Elle vérifie l'absence d'erreurs à l'exécution et d'exceptions non rattrapées, et possède un langage de modélisation pour les bibliothèques C, appliqué, par exemple, à la bibliothèque standard. Pour améliorer la précision, les domaines communiquent et coopèrent via produit réduit, composition ou réécriture, ce qui est facilité par une signature commune.

La plateforme est développée en OCaml; l'environnement de travail consiste en 19 000 lignes de code. Le support pour OCaml, en cours de développement, correspond à
<table><caption>Figure 3 – Temps d'exécution de l'analyse de quelques programmes jouets.</caption><thead><tr><td>Programme</td><td>Lignes</td><td>Temps (ms)</td></tr></thead><tbody><tr><td>list.ml</td><td>3</td><td>3</td></tr><tr><td>tree.ml</td><td>2</td><td>5</td></tr><tr><td>match.ml</td><td>4</td><td>4</td></tr><tr><td>match_alarm.ml</td><td>4</td><td>5</td></tr><tr><td>match_error.ml</td><td>4</td><td>4</td></tr><tr><td>add.ml</td><td>3</td><td>4</td></tr></tbody></table>

quelques 2000 lignes de code<fnref n="1" />. Celui-ci récupère l'arbre de syntaxe abstraite typé dans le fichier .cmt résultant de la compilation d'OCaml, de sorte à bénéficier des parseurs et typeurs natifs et à faciliter la transition vers un support complet du langage. Il supporte actuellement les filtrages de motifs, les types algébriques récursifs et les fonctions non-récursives. Le domaine des fonctions récursives est encore en cours d'implémentation.

## 4.2 Résultats expérimentaux

Une évaluation expérimentale a été réalisée sur des programmes OCaml écrits à la main. Dans la figure 3, on s'intéresse au temps d'exécution de l'analyse sur un ordinateur portable standard pour de courts programmes jouets déclarant des listes ou des arbres et les manipulant via filtrage de motifs, et dont le code peut être trouvé en Annexe F. Sur des exemples simples, l'analyse trouve les résultats attendus de manière rapide. Pour l'heure, nous nous sommes limités à des programmes jouets de quelques lignes. Une extension serait de s'intéresser à des programmes à taille réelle, provenant de projets ou de la bibliothèque standard.

# 5 État de l'art

Pour établir des propriétés sur des programmes fonctionnels, les systèmes de types ont été largement utilisés. Les plus simples permettent de prévenir un certain nombre d'erreurs, telle l'addition d'un entier à une fonction. D'autres, tels les types de raffinements [31, 32], permettent d'exprimer des propriétés complexes sur des valeurs algébriques ou numériques mais délèguent pour cela des vérifications à des solveurs SMTs. Les méthodes dites déductives, telles Why3 [13] ou F* [30], peuvent quant à elles établir des propriétés plus fines sur les programmes, telle leur correction par rapport à une spécification. Elles reposent cependant sur des annotations utilisateurs et des solveurs SMT. Notre travail cherche un nouveau compromis, une méthode automatique et sans solveur paramétrée par un choix d'abstraction, pour inférer des propriétés numériques.

Si de nombreuses recherches traitent de l'analyse statique des langages fonctionnels, elles se sont beaucoup concentrées sur l'analyse de flots de contrôles (CFA) [24], ce qui, comme précisé dans [21] ne permet pas de garder trace des valeurs traversant les flots.

<footnote n="1">1. disponible sur gitlab au lien https://gitlab.com/mvalnet/mopsa-analyzer/-/tree/ocaml</footnote>
Cousot et Cousot [10], eux, se concentrent sur les fonctions comme objets de première classe mais ont pour but d'exprimer par interprétation abstraite des analyses classiques telles la *strictness* ou la terminaison et ne proposent aucune analyse de valeurs.

Dans [23], Montagu et Jensen cherchent à inférer une forme de *frame condition* pour les langages fonctionnels purs, c'est-à-dire identifier des relations d'égalité entre des parties de valeurs algébriques. Une telle approche, si elle se confronte à des problématiques proches, ne vise pas à garder trace des valeurs des variables, non plus que des relations *numériques* entre celles-ci. Elle cherche plutôt à prouver des propriétés de sorte à en décharger les assistants de preuves et à effectuer des optimisations à la compilation. De plus, elle ne permet pas de manipuler des types algébriques récursifs.

Bautista et al. [2] proposent quant à eux une méthode d'abstraction relationnelle pour des valeurs algébriques contenant des données numériques, qu'ils enrichissent ensuite [3] en inférant des égalités structurelles entre champs non numériques. Cependant, cette approche, quoique plus précise que la nôtre dans des cas non récursifs, ne permet pas l'analyse des structures de données récursives tels les listes ou les arbres.

À notre connaissance, le seul analyseur statique de valeurs par interprétation abstraite pour un langage fonctionnel est [16], écrit en 2011. Il génère des contraintes avec sous-typage dont la vérification implique la sûreté du programme, puis les transforme en langage impératif de sorte à réutiliser des analyseurs existants. Cependant, dans cette approche, on perd très tôt la particularité fonctionnelle de notre langage source, ce qui risque d'impliquer une perte de précision. L'article mentionne une implémentation, mais celle-ci n'est pas disponible en ligne, aussi n'avons-nous pu comparer nos résultats.

# 6 Limitations et prolongements

Nos travaux permettent de mettre en évidence de nombreuses pistes vers une analyse statique de valeurs pour des langages fonctionnels d'ordre supérieur réalistes.

Pour l'heure, nous n'avons pas développé de méthode générique pour le polymorphisme. Pour cette raison, notre approche pour une fonction polymorphe diffère de celle d'une fonction monomorphe : on effectue l'analyse non plus lors de sa définition, mais lors de son application à des arguments de type connu. Ainsi, l'inférence du résumé de la fonction est réalisée dans une spécialisation du type de la fonction, et les méthodes pour les fonctions monomorphes s'appliquent. Cependant, travailler sur une analyse polymorphe permettrait d'améliorer les performances en ne réalisant qu'une seule analyse par variable, mais également d'obtenir des propriétés générales sur les variables polymorphes telles des relations d'égalité et d'inégalité, ainsi que des relations d'ordre dans un langage comme OCaml où tout type est muni d'une relation d'ordre total. Lever cette limitation serait un premier pas pour parvenir à l'analyse d'une bibliothèque.

De même, une méthode possible pour supporter l'ordre supérieur serait de procéder par injection (*inlining*) du corps des fonctions lorsque celles-ci sont appliquées. Ainsi, lorsqu'un argument d'une fonction est d'ordre supérieur, on diffère l'analyse de cette fonction jusqu'à ce qu'il puisse être spécialisé par une fonction connue, se ramenant ainsi
à une analyse du premier ordre. Cependant, notre analyse semble pouvoir s'adapter à l'ordre supérieur : en effet, en modélisant comme des relations, donc comme des points du domaine des polyèdres, des fonctions manipulant des entiers, fonctions comme valeurs sont réduites à un ensemble de points dans un espace vectoriel. La complexité et la précision de cette méthode serait à évaluer, tandis que l'étendre ou créer de nouveaux domaines pour les fonctions manipulant des objets algébriques sont des travaux futurs.

De plus, notre analyse se concentre pour l'heure sur un fragment pur de langage fonctionnel. Cela exclut de nombreuses fonctionnalités — tableaux, références, champs mutables — mais permet de simplifier l'analyse des relations entrées-sorties. Diverses pistes ont été envisagées pour étendre aux fonctionnalités impures. L'impureté d'une variable pouvant être identifiée par son type — *'a array*, *'a ref*, *mutable* — on peut choisir d'abstraire toute variable impure par la valeur maximale du domaine abstrait pour signifier qu'on ne connaît aucune information à son sujet, ou de les passer en paramètre de toute fonction susceptible de les manipuler. Pour améliorer la performance, on pourrait également identifier les fonctions dont les variables impures locales n'échappent pas à leur corps et ainsi utiliser les méthodes précédemment élaborées à moindre surcoût.

Un objectif à long terme serait enfin de s'appuyer sur cette analyse pour créer des domaines plus sophistiqués, capable d'établir automatiquement des propriétés plus fines sur les programmes. De telles utilisations de l'interprétation abstraite ont déjà été réalisées pour des langages impératifs, par Cousot et al. dans [7] pour des analyses de contenu de tableau, par Journault et Miné dans [17] pour prouver la correction de programme manipulant des matrices, ou encore avec la *shape analysis* [27], pour prouver des propriétés sophistiquées sur les listes et les arbres. Nous aimerions nous en inspirer pour créer des domaines capables d'exprimer des propriétés sur la taille des listes, la profondeur des structures de données, ou l'équilibre d'un arbre.

## Conclusion

Ainsi, nous avons élaboré des méthodes d'analyse statique de valeur par interprétation abstraite dédiées aux langages fonctionnels. Les domaines abstraits sous-jacents sont relationnels, et permettent de traiter un fragment de langage fonctionnel du premier ordre supportant les types algébriques récursifs ainsi que les fonctions récursives les manipulant. Une partie de ces méthodes a été implémentées au sein de la plate-forme MOPSA pour un fragment de OCaml et ont montré des résultats concluants sur un petit ensemble de programmes écrits à la main. Ce travail dégage également de nombreuses pistes vers l'obtention d'une analyse de valeurs précise et efficace pour un langage fonctionnel d'ordre supérieur.

## Références

[1] Bagnara, R., Hill, P.M., Ricci, E. and Zaffanella, E., 2005. Precise widening operators for convex polyhedra. Science of Computer Programming, 58(1-2), pp.28-56.

[2] Bautista, S., Jensen, T. and Montagu, B., 2020, November. Numeric domains meet algebraic
data types. In Proceedings of the 9th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains (pp. 12-16).

[3] Bautista, S., Jensen, T. and Montagu, B., 2022, December. Lifting Numeric Relational Domains to Algebraic Data Types. In Static Analysis : 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5-7, 2022, Proceedings (pp. 104-134). Cham : Springer Nature Switzerland.

[4] Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A. and Rival, X., 2015. Static analysis and verification of aerospace software by abstract interpretation. Foundations and Trends in Programming Languages, 2(2-3), pp.71-190.

[5] Bourdoncle, F., 1992. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 2(4), pp.407-435.

[6] Bühler, D., 2017. Structuring an abstract interpreter through value and state abstractions : eva, an evolved value analysis for frama-c (Doctoral dissertation, Université de Rennes 1).

[7] P. Cousot & N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. POPL'78, 84-96, ACM, 1978.

[8] Cousot, P. and Cousot, R., 1977. Static determination of dynamic properties of generalized type unions. ACM SIGOPS Operating Systems Review, 11(2), pp.77-94.

[9] Cousot, P. and Cousot, R., 1977, January. Abstract interpretation : a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (pp. 238-252).

[10] Cousot, P. and Cousot, R., 1994, May. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL'94) (pp. 95-112). IEEE.

[11] Cousot, P., Cousot, R. and Logozzo, F., 2011. A parametric segmentation functor for fully automatic and scalable array content analysis. ACM SIGPLAN Notices, 46(1), pp.105-118.

[12] Distefano, D., Fähndrich, M., Logozzo, F. and O'Hearn, P.W., 2019. Scaling static analyses at Facebook. Communications of the ACM, 62(8), pp.62-70.

[13] Filliâtre, J.C. and Paskevich, A., 2013, March. Why3—where programs meet provers. In European symposium on programming (pp. 125-128). Springer, Berlin, Heidelberg.

[14] Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M., 2004. Numeric Domains with Summarized Dimensions, in : Jensen, K., Podelski, A. (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 512-529. https://doi.org/10.1007/978-3-540-24730-2_38

[15] C. Gunter & D. Scott. Semantic domains. Vol. B of Handbook of Theoretical Computer Science, pp. 633-674. Elsevier, 1990.

[16] Jhala, R., Majumdar, R., & Rybalchenko, A. (2011, July). HMC : Verifying functional programs using abstract interpreters. In International Conference on Computer Aided Verification (pp. 470-485). Springer, Berlin, Heidelberg.

[17] Journault, M. and Miné, A., 2016, September. Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs. In International Static Analysis Symposium (pp. 257-277). Springer, Berlin, Heidelberg.

[18] Journault, M., 2019. Analyse statique modulaire précise par interprétation abstraite pour la preuve automatique de correction de programmes et pour l'inférence de contrats (Doctoral
dissertation, Sorbonne université).

[19] Journault, M., Miné, A., Monat, R. and Ouadjaout, A., 2020. Combinations of reusable abstract domains for a multilingual static analyzer. In Working Conference on Verified Software : Theories, Tools, and Experiments (pp. 1-18). Springer, Cham.

[20] Krishnaswami, N., 2006. Separation logic for a higher-order typed language. In Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, SPACE (Vol. 6, pp. 73-82).

[21] Liang, S. and Might, M., 2013, November. Entangled abstract domains for higher-order programs. In Proceedings of the 2013 Workshop on Scheme and Functional Programming, Washington, DC.

[22] Monat, R., 2021. Static type and value analysis by abstract interpretation of Python programs with native C libraries (Doctoral dissertation, Sorbonne Université).

[23] Montagu, B. and Jensen, T., 2020. Stable relations and abstract interpretation of higher-order programs. Proceedings of the ACM on Programming Languages, 4(ICFP), pp.1-30.

[24] Montagu, B. and Jensen, T., 2021, June. Trace-based control-flow analysis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 482-496).

[25] Nielson, F. and Nielson, H.R., 1997, January. Infinitary control flow analysis : a collecting semantics for closure analysis. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 332-345).

[26] Rice, H. G., 1953, Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical society, 74(2), 358-366.

[27] Sagiv, M., Reps, T. and Wilhelm, R., 2002. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (TOPLAS), 24(3), pp.217-298.

[28] Smaragdakis, Y., Bravenboer, M. and Lhoták, O., 2011, January. Pick your contexts well : understanding object-sensitivity. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 17-30).

[29] Spoto, F., 2016, September. The Julia static analyzer for Java. In International Static Analysis Symposium (pp. 39-57). Springer, Berlin, Heidelberg.

[30] Swamy, N., Hriţcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M. and Zinzindohoue, J.K., 2016, January. Dependent types and multi-monadic effects in F. In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 256-270).

[31] Swamy, N., Weinberger, J., Schlesinger, C., Chen, J. and Livshits, B., 2013. Verifying higher-order programs with the Dijkstra monad. ACM SIGPLAN Notices, 48(6), pp.387-398.

[32] Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D. and Peyton-Jones, S., 2014, August. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (pp. 269-282).

# Annexe A Sémantique du langage fonctionnel

On définit en Fig 4 la sémantique concrète collectrice de notre langage fonctionnel. Ainsi, la valeur d'une variable $x$ dans un environnement $\sigma$ est $\sigma(x)$, celle d'un entier $n$ est ce même entier. L'expression fun $x_1...x_n \rightarrow e$ est interprétée comme une fonction
$$
\mathbb{E}[\cdot] : \Sigma \to \mathcal{V}
$$

$$
\mathbb{E}[x \in \mathbb{V}]\sigma = \sigma(x)
$$

$$
\mathbb{E}[n \in \mathbb{Z}]\sigma = n
$$

$$
\mathbb{E}[\text{fun } x_1 \dots x_n \to e] \sigma = \lambda a_1 \dots a_n . \mathbb{E}[e] \sigma [x_1 \to a_1, \dots, x_n \to a_n]
$$

$$
\mathbb{E}[e_1 e_2 \dots e_{n+1}]\sigma = \begin{cases} f[x_i \to \mathbb{E}[e_i]]\sigma & \text{si } \mathbb{E}[e_1]\sigma = \lambda x_1 \dots x_n \cdot f \wedge \forall 1 \le i \le n, \mathbb{E}[e_i]\sigma \in \mathcal{V}_0 \setminus \{\omega\} \\ \omega & \text{sinon} \end{cases}
$$

$$
\mathbb{E}[\text{if } e_1 \text{ then } e_2 \text{ else } e_3] \sigma = \begin{cases} \mathbb{E}[e_2] \sigma & \text{si } \mathbb{E}[e_1] \sigma = z \in \mathbb{Z} \wedge z \neq 0 \\ \mathbb{E}[e_3] \sigma & \text{si } \mathbb{E}[e_1] \sigma = 0 \\ \omega & \text{sinon} \end{cases}
$$

$$
\mathbb{E}[\text{assert } e] \sigma = \begin{cases} 1 & \text{si } \mathbb{E}[e] \sigma = z \in \mathbb{Z} \wedge z \neq 0 \\ \omega & \text{sinon} \end{cases}
$$

$$
\mathbb{E}[\text{let } x = e_1 \text{ in } e_2] \sigma = \begin{cases} \mathbb{E}[e_2] \sigma [x \to \mathbb{E}[e_1]] \sigma & \text{si } \mathbb{E}[e_1] \sigma \neq \omega \\ \omega & \text{sinon} \end{cases}
$$

$$
\mathbb{E}[\text{let rec } x_f = e_1 \text{ in } e_2] \sigma = \begin{cases} \mathbb{E}[e_2] \sigma [x_f \to \text{lfp}(F_{x_f,x,g})] & \text{si } \mathbb{E}[e_1] \sigma = \lambda x_1 \dots x_n \cdot g \\ \omega & \text{sinon} \end{cases}
$$

$$
\text{avec } F_{x_f, x, g}(\phi) = \lambda y_1 \dots y_n \mathbb{E}[g] \sigma [x_i \to y_i, x_f \to \phi]
$$

$$
\mathbb{E}[e_1 \oplus e_2] \sigma = \begin{cases} n_1 \oplus n_2 & \text{si } \mathbb{E}[e_1] \sigma = n_1 \in \mathbb{Z} \text{ et } \mathbb{E}[e_2] \sigma = n_2 \in \mathbb{Z} \\ \omega & \text{sinon} \end{cases}
$$

$$
\mathbb{E}[C(e_1, \dots, e_n)]\sigma = \begin{cases} C(\mathbb{E}[e_1]\sigma, \dots, \mathbb{E}[e_n]\sigma) & \text{si } \forall 1 \le i \le n, \mathbb{E}[e_i]\sigma \in \mathcal{V}_0 \setminus \{\omega\} \\ \omega & \text{sinon} \end{cases}
$$

$$
\mathbb{E}[\text{match } e_0 \text{ with } p_1 \to e_1 | \dots | p_m \to e_m] \sigma = \begin{cases} \mathbb{E}[e_1] \sigma' & \text{si } b_{\text{guard}} = \mathbf{true} \\ \mathbb{E}[e'_1] \sigma & \text{si } b_{\text{guard}} = \mathbf{false} \wedge m > 1 \\ \omega & \text{sinon} \end{cases}
$$

$$
\text{avec } \begin{cases} \mathbf{match}(\sigma, \mathbb{E}[e_0]\sigma, p_1) = (\sigma', b_{\text{guard}}), & \text{cf. Fig. 5} \\ e'_1 = \mathbf{match} \ e_0 \ \text{with} \ p_2 \to e_2 \ | \ \dots \ | \ p_m \to e_m \end{cases}
$$

<caption>Figure 4 – Sémantique fonctionnelle du langage.</caption>

mathématique, qui à des paramètres $a_1 \dots a_n$ renvoie l'objet mathématique correspondant à la sémantique de $e$ dans un contexte où les variables $x_i$ valent $a_i$. L'application s'interprète de la manière suivante : si $e_1$ s'interprète en une fonction, on évalue cette dernière avec pour arguments les interprétations des $e_i$ si ceux-ci ne sont pas des fonctions. Sinon, $\omega$ est renvoyée. La sémantique du if est naturelle : si $e_1$ s'interprète en un entier non nul, la valeur est celle de l'interprétation de $e_2$, celle de $e_3$ s'il s'interprète en
$$ match(\cdot, \cdot, \cdot) : \Sigma \times \mathcal{V} \times \Pi \to \Sigma \times \mathcal{B} \cup \{\omega\} $$

$$ match(\sigma, \omega, p) = \sigma, \omega $$

$$ match(\sigma, v, \_ ) = \sigma, true $$

$$ match(\sigma, v, x \in \mathcal{V}) = \sigma[x \to v], true $$

$$ match(\sigma, v, n_2 \in \mathbb{Z}) = \sigma, \begin{cases} n_1 = n_2 & \text{si } v = n_1 \in \mathbb{Z} \\ false & \text{sinon} \end{cases} $$

$$ match(\sigma, C(v_1, \dots, v_n), C(p_1, \dots, p_n)) = \sigma_n, \bigwedge_{i \in [1, n]} b_i $$

$$ \text{avec } \begin{cases} \sigma_0 = \sigma \\ \forall i \in [1, n], \sigma_{i+1}, b_{i+1} = \text{match}(\sigma_i, v_i, p_i) \end{cases} $$

$$ match(\sigma, v, C(p_1, \dots, p_n)) = \sigma, false \text{ avec } v \neq C(v_1, \dots, v_n) $$

$$ match(\sigma, v, p_1 \text{ when } e_1) = \sigma', b \wedge \mathbb{E}[e_1] \sigma' \neq 0 \text{ avec } match(\sigma, v, p) = \sigma', b $$

<caption>Figure 5 – Définition de match.</caption>

0, une erreur sinon. L'assert s'interprète en 1 si $e$ s'interprète en un entier non nul, une erreur sinon. Le let correspond à l'interprétation de $e_2$ dans un environnement où $x$ a comme valeur l'interprétation de $e_1$ si celle-ci n'est pas une erreur, $\omega$ sinon.

Le let rec quant à lui associe à $x_f$ l'interprétation suivante : si $e_1$ est une fonction, on considère la fonction $F_{x_f,x,g}$, qui à une fonction $\phi$ associe la fonction qui à $y$ associe l'interprétation du corps $g$. Cette fonction, $F_{x_f,x,g}(\phi)$, est ainsi une meilleure approximation de $x_f$ que $\phi$. On associe alors à $x_f$ le plus petit point fixe de $F_{x_f,x,g}$, défini sur les fonctions continues. Ce point fixe est bien défini [15].

Enfin, $e_1 \oplus e_2$ a pour valeur l'opération mathématique correspondant à $\oplus$ appliquée aux interprétations de $e_1$ et $e_2$ si toutes deux sont des entiers, $\omega$ sinon. $C(e_1, \dots, e_n)$ s'interprète en interprétant chacune des expressions en paramètres du constructeur de type si celles-ci ne sont pas des fonctions et ne renvoient pas d'erreurs, $\omega$ sinon. La sémantique du match est plus complexe. On définit pour ce faire la fonction match en Fig. 5.

La fonction match prend en paramètre un environnement, une valeur et un motif. Elle renvoie un booléen, vrai si et seulement si la valeur peut correspondre au motif, ainsi que l'environnement dans lequel les variables du motif sont associées aux valeurs correspondantes de l'expression.

Ainsi, si le v est un joker $_\_$, la valeur peut correspondre au motif : le booléen est vrai et l'environnement est inchangé car aucune variable n'a été liée. Si le motif est une variable $x$, la valeur $v$ peut également correspondre au motif dans un environnement où $x$ est lié à $v$. Si le motif est un entier $n_2 \in \mathbb{Z}$, alors $v$ correspond à $n_2$ si et seulement si $n_1$ et $n_2$ vus comme des entiers mathématiques sont égaux. Sinon, le booléen est faux.
Enfin, si le motif est sous la forme $C(p_1, \dots, p_n)$ et la valeur de la forme $C(v_1, \dots, v_n)$, la valeur correspond au motif si et seulement si tous les bvi peuvent correspondre aux $p_i$. L'environnement est alors l'environnement $\sigma_n$ dans lequel si la conjonction des $b_i$ est vrai, les $v_i$ correspondent aux $p_i$. Comme $\forall i, j, fv(p_i) \neq fv(p_j)$, une variable n'a pas été liée plusieurs fois. Quant au motif $p_1$ when $e_1$, la valeur correspond au motif si et seulement si elle correspond à $p_1$ et $e_1$ s'interprète en une valeur non nulle.

Pour revenir à la sémantique du filtrage de motif, match $e_0$ with $p_1 \rightarrow e_1$ | ... | $p_m \rightarrow e_m$ est interprété de la manière suivante : si le boléen renvoyé par match($\sigma, e_0, p_1$) est vrai, c'est-à-dire si $e_0$ et $p_1$ peuvent correspondre, on évalue $e_1$ dans l'environnement $\sigma'$ dans lequel $e_0$ et $p_1$ correspondent. Sinon, si $m > 1$, on ré-interprète le match en retirant le cas $p_1 \rightarrow e_1$. Enfin, si $m = 1$ et $b_{guard}$ est faux, l'expression ne correspond à aucun motif et une erreur est renvoyée.

Intuitivement donc, l'expression est séquentiellement comparée aux différents motifs ; sitôt que celle-ci correspond à un motif $p_i$, l'expression $e_i$ correspondante est évaluée dans le contexte résultant.

## Annexe B Fonctions de transfert

On détaille ici les fonctions de transfert pour les constructions du langage.

$$
\begin{align*}
\mathbb{E}^{\#}[x](\epsilon, d) &= \epsilon(x), (\epsilon, d) \\
\mathbb{E}^{\#}[n \in \mathbb{Z}]\sigma^{\#} &= n, \sigma^{\#} \\
\mathbb{E}^{\#}[\text{if } e_1 \text{ then } e_2 \text{ else } e_3]\sigma^{\#} &= \mathbb{E}^{\#}[e_2](\mathcal{F}^{\#}[e_1^n]\sigma_1^{\#}) \cup^{\#} \mathbb{E}^{\#}[e_3](\mathcal{F}^{\#}[-e_1^n]\sigma_1^{\#}) \\
&\qquad \text{où } \mathbb{E}^{\#}[e_1]\sigma^{\#} = e_1^n, \sigma_1^{\#} \\
\mathbb{E}^{\#}[\text{let } x = e_1 \text{ in } e_2]\sigma^{\#} &= \mathbb{E}^{\#}[e_2]\sigma_1^{\#}[x \to e^{\#}] \quad \text{où } \mathbb{E}^{\#}[e_1]\sigma^{\#} = e^{\#}, \sigma_1^{\#} \\
\mathbb{E}^{\#}[e_1 \oplus e_2]\sigma^{\#} &= x \oplus y, \sigma_2^{\#}[x \to e_1^n][y \to e_2^n], \quad \text{où } \mathbb{E}^{\#}[e_1]\sigma^{\#} = e_1^n, \sigma_1^{\#}, \mathbb{E}^{\#}[e_2]\sigma_1^{\#} = e_2^n, \sigma_2^{\#} \\
\mathbb{E}^{\#}[\text{assert } e]\sigma^{\#} &= \begin{cases} \{\omega\}, \sigma^{\#} & \text{si } \mathcal{F}^{\#}[e^n]\sigma_0^{\#} \neq \bot, \mathbb{E}^{\#}[e]\sigma^{\#} = e^n, \sigma_0^{\#} \\ \mathbb{E}^{\#}[1]\sigma^{\#} & \text{sinon} \end{cases}
\end{align*}
$$

<caption>Figure 6 – Fonctions de transfert pour les constructions du langage.</caption>

Ainsi, l'interprétation abstraite d'une variable renvoie sa valeur dans l'environnement abstrait ainsi que l'environnement abstrait dans lequel ceci est vrai - en effet, si $x$ est un entier, $\epsilon(x)$ est une variable numérique dont les valeurs possibles sont définies par $d$. L'interprétation de $n$ renvoie l'entier $n$ dans l'environnement inchangé. L'interprétation de if $e_1$ then $e_2$ else $e_3$ est l'union abstraite de l'interprétation de $e_2$ dans un environnement restreint dans lequel l'expression numérique associée à $e_1$ est nécessairement non nulle et de celles de $e_3$ dans un environnement restreint dans elle est nécessairement nulle. Let $x = e_1$ in $e_2$ a comme interprétation abstraite celle de $e_2$ dans l'environnement dans lequel $x$ est assigné à l'interprétation de $\mathbb{E}^{\#}[e_1]\sigma^{\#}$ - par définition
de la notation $\sigma^{\#}[x \to y]$, l'opérateur d'assignation du domaine numérique peut être
utilisé pour ce faire. $e_1 \oplus e_2$ a comme interprétation abstraite l'expression numérique
$x \oplus y$, où $x$ et $y$ sont des variables fraîches, assignées dans l'environnement de retour aux
interprétations de $\mathbb{E}^{\#}[e_1]\sigma^{\#}$ et $\mathbb{E}^{\#}[e_2]\sigma^{\#}$ - ce qui appelle l'assignation numérique. assert
$e$ s'interprète en $\Omega = \{\omega\}$ s'il existe un environnement restreint non vide dans lequel
l'interprétation de $e$ est non vide, 1 sinon.

# Annexe C Définitions

## C.1 Concrétisation

**Définition C.1.** Pour $e \in \mathcal{E}$, $\sigma^{\#} \in \Sigma^{\#}$, en notant $\mathbb{E}^{\#}[e]\sigma^{\#} = (e^{\#}, (\epsilon, d))$, on a :

$$
\gamma(\mathbb{E}^{\#}[e]\sigma^{\#}) = \begin{cases} \{ n \in \mathbb{Z} \mid \exists \delta \in (\mathbb{V} \to \mathbb{Z}), \delta(\epsilon(e)) = n \land \delta \in \gamma_{\mathbb{Z}}(d) \} & \text{si } e : \mathbb{int} \\ \gamma_{\mathbb{T}}(e^{\#}) & \text{sinon} \end{cases}
$$

$$
\text{en notant } \epsilon(e) = \begin{cases} n & \text{si } e = n \in \mathbb{Z} \\ \epsilon(x) & \text{si } e = x \in \mathbb{V}_{\mathbb{Z}} \\ \epsilon(e_1) \oplus \epsilon(e_2) & \text{sinon} \end{cases}
$$

**Définition C.2.** Pour $\sigma \in \Sigma$, $\sigma^{\#} = (\epsilon, d) \in \Sigma^{\#}$, on note $\sigma \in \sigma^{\#} \iff \forall x \in \mathbb{V} \setminus \mathbb{V}_{\mathbb{Z}}, \sigma(x) \in \gamma(\epsilon(x)) \wedge \sigma|_{\mathbb{Z}} \in \gamma_{\mathbb{Z}}(d)$

**Lemme C.1.** Si $\sigma \in \sigma^{\#}$, alors $\forall x, \sigma(x) \in \gamma(\sigma^{\#}(x), \sigma^{\#})$.

Rappelons maintenant que pour $e \in \mathcal{E}$, $\sigma_p \in \mathcal{P}(\Sigma)$, on a $\mathcal{F}[e]\sigma_p = \{ \sigma \in \sigma_P \mid \mathbb{E}[e]\sigma = n \in \mathbb{Z} \wedge n \neq 0 \}$. La définition de la fonction de filtre $\mathcal{F}^{\#}$, la fonction de filtre dans l'abstrait, dépend du domaine choisi pour représenter les entiers et est fournie avec celui-ci. Elle vérifie la propriété :

**Lemme C.2.** Pour $e \in \mathcal{E}$, $\sigma^{\#} \in \Sigma^{\#}$, si $\sigma_p \subseteq \sigma^{\#}$, $\mathcal{F}[e]\sigma_p \subseteq \gamma(\mathcal{F}^{\#}[e^n]\sigma_0^{\#})$, avec $\mathbb{E}^{\#}[e]\sigma^{\#} = e^n$, $\sigma_0^{\#}$.

## C.2 Union abstraite $\cup^{\#}$

Soient $(e_1^{\#}, (s_1, d_1))$, $(e_2^{\#}, (s_2, d_2)) \in \mathcal{V}^{\#} \times \Sigma^{\#}$. Alors :

$$
(e_1^{\#}, (s_1, d_1)) \cup^{\#} (e_2^{\#}, (s_2, d_2)) = \begin{cases} (x, (s_1, d_1)[x \to e_1^{\#}] \cup_{\Sigma^{\#}} (s_2, d_2)[x \to e_2^{\#}]) & \text{si } e_1^{\#}, e_2^{\#} \in \mathcal{E}_{\mathbb{Z}}, \\ e_1^{\#} \cup_{\mathcal{D}} e_2^{\#}, (s_1, d_1) \cup_{\Sigma^{\#}} (s_2, d_2) & \text{sinon} \end{cases}
$$

où $\cup_{\Sigma^{\#}}^{\#}$ est définie comme suit :
$$ (s_1, d_1) \cup_{\Sigma^{\mathbb{H}}} (s_2, d_2) = \begin{cases} x \to x_i, & \text{si } x \in \mathbb{V}_{\mathbb{Z}}, x_i \text{ fraîche} \\ x \to s_1(x) \cup_{\mathcal{D}} s_2(x) & \text{sinon} \end{cases} \quad , d_0[x_i \to v_i] $$
$$ \text{avec } d_0 = d_1 \cup_{\mathcal{D}_{\mathbb{Z}}} d_2 $$

**Lemme C.3.** $\cup^{\mathbb{H}}$ est sûr.

### C.3 Fonction match$^{\mathbb{H}}$

On définit ici match$^{\mathbb{H}}$, utilisé dans la définition de la sémantique abstraite.

$$ \mathbf{match}^{\mathbb{H}}(\cdot, \cdot, \cdot) : \Sigma^{\mathbb{H}} \times \mathcal{V}^{\mathbb{H}} \times \Pi \to \Sigma^{\mathbb{H}} \times \Sigma^{\mathbb{H}} $$

$$ \mathbf{match}^{\mathbb{H}}(\sigma^{\mathbb{H}}, v^{\mathbb{H}}, \_ ) = \sigma^{\mathbb{H}}, \perp $$

$$ \mathbf{match}^{\mathbb{H}}(\sigma^{\mathbb{H}}, v^{\mathbb{H}}, x \in \mathcal{V}) = \sigma^{\mathbb{H}}[x \to v^{\mathbb{H}}], \perp $$

$$ \mathbf{match}^{\mathbb{H}}(\sigma^{\mathbb{H}}, v^{\mathbb{H}}, n_2 \in \mathbb{Z}) = \mathcal{F}^{\mathbb{H}}[[v^{\mathbb{H}}]]\sigma^{\mathbb{H}}, \mathcal{F}^{\mathbb{H}}[\neg v^{\mathbb{H}}]\sigma^{\mathbb{H}} $$

$$ \mathbf{match}^{\mathbb{H}}(\sigma^{\mathbb{H}}, v^{\mathbb{H}}, C_i(p_1, \dots, p_n)) = \sigma_n^{\mathbb{H}}, \sigma_{\neg,n}^{\mathbb{H}} $$

$$ \text{avec} \quad \begin{cases} v^{\mathbb{H}} = (g, \mathscr{C}) \in \mathcal{D}_t \\ C_i \in \mathscr{C}, \sigma_0^{\mathbb{H}} = \sigma^{\mathbb{H}} \\ \forall j \in [[1, n]], \sigma_{j+1}^{\mathbb{H}}, \sigma_{\neg,j+1}^{\mathbb{H}} = \mathbf{match}^{\mathbb{H}}(\sigma_j^{\mathbb{H}}, g_{i,j}, p_j) \end{cases} $$

$$ \mathbf{match}^{\mathbb{H}}(\sigma^{\mathbb{H}}, v^{\mathbb{H}}, p_1 \text{ when } e_1) = \mathcal{F}^{\mathbb{H}}[[e_1^n]]\sigma_1^{\mathbb{H}}, \sigma_{\neg,0}^{\mathbb{H}} $$

$$ \text{avec } \mathbf{match}(\sigma^{\mathbb{H}}, v^{\mathbb{H}}, p) = \sigma_0^{\mathbb{H}}, \sigma_{\neg,0}^{\mathbb{H}}, \mathbb{E}^{\mathbb{H}}[e_1]\sigma_0^{\mathbb{H}} = e_1^n, \sigma_1^{\mathbb{H}} $$

Notons que la fonction de filtre $\mathcal{F}^{\mathbb{H}}$ est fournie par le domaine numérique. Étant donnée une expression numérique et un environnement abstrait, elle restreint cet environnement abstrait de sorte que l'expression numérique en paramètre soit non nulle.

**Lemme C.4.** Pour $\sigma, v, p \in \Sigma \times \mathcal{V} \times \Pi$, $\sigma^{\mathbb{H}} \in \Sigma^{\mathbb{H}}, v^{\mathbb{H}} \in \mathcal{V}^{\mathbb{H}}$ tel que $\sigma \in \sigma^{\mathbb{H}}, v \in \gamma(v^{\mathbb{H}}, \sigma^{\mathbb{H}})$, alors en notant $\mathbf{match}(\sigma, v, p) = \sigma_m$, $b$ et $\mathbf{match}^{\mathbb{H}}(\sigma^{\mathbb{H}}, v^{\mathbb{H}}, p) = \sigma_m^{\mathbb{H}}, \sigma_{\neg,m}^{\mathbb{H}}$, on a $b = \mathbf{true} \implies \sigma_m \in \sigma_m^{\mathbb{H}}$ et $b = \mathbf{false} \implies \sigma_m \in \sigma_{\neg,m}^{\mathbb{H}}$.

*Démonstration.* On procède par récurrence sur la syntaxe des motifs. On ne s'intéressera qu'au cas suivant :

- Si $p = C_l(p_1, \dots, p_n)$.

- Si $b = \mathbf{true}$, alors par définition de match, $v = C_i(v_1, \dots, v_n)$, et comme $v \in \gamma(v^{\mathbb{H}}, \sigma^{\mathbb{H}}) = \gamma_t(v^{\mathbb{H}}, \sigma^{\mathbb{H}})$, $v_i \in \gamma(g_{i,j}, \sigma^{\mathbb{H}})$. Alors en notant $\sigma_0 = \sigma$ et pour $i \in [[1, n]]$, match($\sigma_i, v_i, p_i) = \sigma_{i+1}, b_{i+1}$, et en constatant que $\forall i, b_i = \mathbf{true}$, par une récurrence simple sur $i \in [[1, n]]$, on prouve que $\sigma_i \in \sigma_i^{\mathbb{H}}$ (on applique successivement l'hypothèse de récurrence. Alors en particulier,

- Si $b = \mathbf{false}$, le raisonnement est le même en remplaçant $\sigma_i^{\mathbb{H}}$ par $\sigma_{\neg,i}^{\mathbb{H}}$.

Les autres cas sont plus simples, et utilisent la correction de $\mathcal{F}^{\mathbb{H}}$. $\square$
# Annexe D Preuves

## D.1 Sûreté de $\cup_{\tau}^{\#}$ et $\cap_{\tau}^{\#}$

*Démonstration.* Étant donné un type algébrique $t$, on veut prouver que l'opérateur de $\mathcal{D}_t \cup_{\tau}^{\#}$ est une abstraction sûre de $\cup$, c'est-à-dire :

$$ \forall (g_1, \mathcal{C}_1), (g_2, \mathcal{C}_2) \in \mathcal{D}_t, \gamma_t((g_1, \mathcal{C}_1)) \cup \gamma_t((g_2, \mathcal{C}_2)) \subseteq \gamma_t((g_1, \mathcal{C}_1) \cup_{\tau}^{\#} (g_2, \mathcal{C}_2)) $$

Rappelons que :

$$ (g^1, \mathcal{C}_1) \cup_{\tau}^{\#} (g^2, \mathcal{C}_2) = (g, \mathcal{C}_1 \cup \mathcal{C}_2) \quad \text{avec } g_{i,j} = g_{i,j}^1 \cup_{\mathcal{D}_{i,j}} g_{i,j}^2 $$

Soit maintenant $x \in \gamma_t((\mathcal{C}_1, g_1)) \cup \gamma_t((\mathcal{C}_2, g_2))$. Supposons sans perte de généralité que $x \in \gamma_t((\mathcal{C}_1, g_1))$. Alors remarquons que $\mathcal{C}_1 \subseteq \mathcal{C}_1 \cup \mathcal{C}_2$ et que $\forall i, j, g_{i,j}^1 \leq_{i,j} g_{i,j}^2$. D'où $(\mathcal{C}_1, g_1) \subseteq (\mathcal{C}_1 \cup \mathcal{C}_2, g)$. Donc par croissance de $\gamma_t$, on a bien $\gamma_t((g_1, \mathcal{C}_1)) \cup \gamma_t((g_2, \mathcal{C}_2)) \subseteq \gamma_t((g_1, \mathcal{C}_1) \cup_{\tau}^{\#} (g_2, \mathcal{C}_2))$.

La preuve de sûreté de l'opérateur $\cap_{\tau}^{\#}$ est similaire. $\square$

<figure><img src="image_91.png" /></figure>

## D.2 Sûreté de l'élargissement pour les objets algébriques

*Démonstration.* Étant donné un type $t$, on cherche à prouver que $\nabla_t$ est bien un opérateur d'élargissement pour $\mathcal{D}_t$. Rappelons que :

$$ (\mathcal{C}_1, g_1) \nabla_t (\mathcal{C}_2, g_2) = (g, \mathcal{C}_1 \cup \mathcal{C}_2) \quad \text{avec } g_{i,j} = g_1|_{i,j} \nabla_{\mathcal{D}_{i,j}} g_2|_{i,j} $$

* $\nabla_t$ sur-approxime l'union. On note $X_{\leq h} = \{x \in X \mid h(x) \leq h\}$ avec $h(x)$ la profondeur de $x$. On prouve par récurrence sur $h \mathcal{P}(h)$ : "$\forall (\mathcal{C}_1, g_1), (\mathcal{C}_2, g_2), \gamma_t((\mathcal{C}_1, g_1))_{\leq h} \cup \gamma_t((\mathcal{C}_2, g_2))_{\leq h} \subseteq \gamma_t((\mathcal{C}_1, g_1)\nabla_t \gamma_t((\mathcal{C}_2, g_2))_{\leq h}$". Pour $h = 0$, les ensembles sont vides ou contiennent uniquement des feuilles (aucun champ récursif) et le raisonnement du cas $ti, j \neq t$ ci-dessous s'applique.

Soit $h \in \mathbb{N}$, $(g_1, \mathcal{C}_1), (g_2, \mathcal{C}_2) \in \mathcal{D}_t$. Soit $x \in \gamma_t(((g_1, \mathcal{C}_1))_{\leq h+1} \cup \gamma_t((g_2, \mathcal{C}_2))_{\leq h+1})$.

Supposons sans perte de généralités que $x \in \gamma_t(((g_1, \mathcal{C}_1))_{\leq h+1})$.

Alors $x = C_i(x_{i,1}, \dots, x_{i,n_i})$, avec $C_i \in \mathcal{C}_1$, et $h(x) \leq h + 1$.

* Supposons $ti, j \neq t$. On a $x_{i,j} \in \gamma_{\tau_{i,j}}(g_{1,i,j})$. Comme $\nabla_{\mathcal{D}_{i,j}}$ est un opérateur d'élargissement, on a $\gamma_{\tau_{i,j}}(g_{1,i,j}) \cup_{i,j} \gamma_{\tau_{i,j}}(g_{2,i,j}) \subseteq \gamma_{\tau_{i,j}}(g_{1,i,j} \nabla_{i,j} g_{2,i,j})$, donc $\gamma_{\tau_{i,j}}(g_{1,i,j}) \subseteq \gamma_{\tau_{i,j}}(g_{1,i,j} \nabla_{i,j} g_{2,i,j})$. On en déduit : $x_{i,j} \in \gamma_{\tau_{i,j}}(g_1[i, j] \nabla_{\mathcal{D}_{i,j}} g_2[i, j]) = \gamma_{\tau_{i,j}}(g_{1,i,j})$.

* Supposons $ti, j = t$. On a alors $x_{i,j} \in \gamma_t(g_1, g_{1,i,j})_{\leq h}$. Par hypothèse de récurrence, on a $\gamma_t((\mathcal{C}_1, g_1))_{\leq h} \cup \gamma_t((\mathcal{C}_2, g_2))_{\leq h} \subseteq \gamma_t((\mathcal{C}_1, g_1)\nabla_t \gamma_t((\mathcal{C}_2, g_2))_{\leq h}$, d'où $\gamma_t((\mathcal{C}_1, g_1))_{\leq h} \subseteq \gamma_t((\mathcal{C}_1, g_1)\nabla_t \gamma_t((\mathcal{C}_2, g_2))_{\leq h}$, donc $x \in \gamma_t((g, \mathcal{C}_1 \cup \mathcal{C}_2))_{\leq h}$.

Ainsi, $\mathcal{P}(h+1)$ est vrai. Cela prouve donc la propriété pour tout $h \in \mathbb{N}$. Alors on a bien $\nabla_t$ sur-approxime l'union : $\gamma_t((\mathcal{C}_1, g_1)) \cup \gamma_t((\mathcal{C}_2, g_2)) \subseteq \gamma_t((\mathcal{C}_1, g_1)\nabla_t \gamma_t((\mathcal{C}_2, g_2))$
* $\nabla_t$ assure la convergence en temps fini. Considérons la suite $((g_n, \mathscr{C}_n))_{n \in \mathbb{N}}$. On cherche à prouver que la suite

$$((g_n^{\nabla}, C_n^{\nabla}))_{n \in \mathbb{N}} : \begin{cases} (g_0^{\nabla}, C_0^{\nabla}) = (g_0, \mathscr{C}_0) \\ (g_{n+1}^{\nabla}, C_{n+1}^{\nabla}) = (g_n^{\nabla}, C_n^{\nabla}) \nabla_t (g_{n+1}, \mathscr{C}_{n+1}) \end{cases}$$

est stationnaire.

Pour $i, j$, on remarque que $g_n^{\nabla}|_{i,j} = \nabla_{i,j} g_l|_{i,j}$. Or $\nabla_{i,j}$ est un opérateur d'élargissement, donc cette suite est stationnaire. Soit $n_{i,j}$ l'indice à partir duquel cette suite est stationnaire. Notons $n_g = \max_{i,j} n_{i,j}$. Alors à partir du rang $n_g$, toutes les suites $(g_n^{\nabla}|_{i,j})_{n \in \mathbb{N}}$ sont stationnaires. Cela implique que la suite $(g_n^{\nabla})_{n \in \mathbb{N}}$ est stationnaire à partir du rang $n_g$. Enfin, $\cup$ est un opérateur d'élargissement dans $\mathcal{P}(\mathscr{C}_t)$ donc il existe un rang $n_C$ à partir duquel $(\mathscr{C}_n^{\nabla})_{n \in \mathbb{N}}$ est stationnaire. Ainsi, à partir du rang $N = \max(n_h, n_C)$, $((g_n^{\nabla}, C_n^{\nabla}))_{n \in \mathbb{N}}$ est stationnaire.

Donc $\nabla_t$ est bien un widening.

□

## D.3 Sûreté de la sémantique abstraite

*Démonstration.* On cherche à prouver la sûreté de la sémantique abstraite $\mathscr{S}^{\sharp}$, c'est-à-dire

$$\forall \sigma \in \Sigma, \forall e \in \mathcal{E}, \sigma \in \sigma^{\sharp} \implies \mathbb{E}[e]\sigma \in \gamma(\mathbb{E}^{\sharp}[e]\sigma^{\sharp}) \wedge \sigma \in \sigma_0^{\sharp} \quad \text{avec } \mathbb{E}^{\sharp}[e]\sigma^{\sharp} = e^{\sharp}, \sigma_0^{\sharp}$$

On effectue la preuve par récurrence sur la syntaxe de $e \in \mathcal{E}$.

* Soit $e$ une expression telle qu'une sous-expression $e_0$ renvoie une erreur. Par hypothèse sur la sémantique abstraite, on a aussi $\mathbb{E}^{\sharp}[e]\sigma^{\sharp} = \Omega$. On suppose l'expression bien typée, donc les seules erreurs proviennent des échecs de filtrage et des échecs d'assertion. Par hypothèse de récurrence, $\mathbb{E}[e_0]\sigma \in \gamma(\mathbb{E}^{\sharp}[e_0]\sigma^{\sharp}) = \gamma(\Omega) = \{\omega\}$, l'interprétation de $e_0$ renvoie une erreur, donc l'interprétation concrète de $e$ renvoie une erreur. On a donc bien $\mathbb{E}[e]\sigma \in \gamma(\mathbb{E}^{\sharp}[e]\sigma^{\sharp})$, et $\sigma \in \sigma_0^{\sharp} = \sigma^{\sharp}$. Par la suite, on supposera donc qu'aucune sous-expression ne renvoie d'erreur.

* Si $e = x$, alors $\mathbb{E}[e]\sigma = \sigma(x)$, et comme $\sigma \in \sigma^{\sharp}$, on a $\sigma(x) \in \gamma(\sigma^{\sharp}(x), \sigma^{\sharp}) = \gamma(\mathbb{E}^{\sharp}[x]\sigma^{\sharp})$ et $\sigma \in \sigma_0^{\sharp} = \sigma^{\sharp}$.

* Si $e = z \in \mathbb{Z}$, alors $\mathbb{E}[e]\sigma = z$. On a $\mathbb{E}^{\sharp}[z \in \mathbb{Z}](\epsilon, d) = z, (\epsilon, d)$. Or, $\gamma(n, (\epsilon, d)) = \{n \in \mathbb{Z} \mid \exists \delta \in \mathcal{P}(\mathbb{V} \to \mathbb{Z}), \delta(z) = n \wedge \delta \in \gamma_{\mathbb{Z}}(d_0) \} = \{z\}$. D'où $\mathbb{E}[z \in \mathbb{Z}]\sigma \in \gamma(\mathbb{E}^{\sharp}[z \in \mathbb{Z}]\sigma^{\sharp})$ et $\sigma \in \sigma_0^{\sharp} = \sigma^{\sharp}$.
* Si $e = e_1 \oplus e_2$, on a $\mathbb{E}^{\#}[e_1 \oplus e_2]\sigma^{\#} = x \oplus y, \sigma_2^{\#}[x \to e_1^n][y \to e_2^n] = e^{\#}, \sigma^{\#}$, avec
$$ \begin{cases} \mathbb{E}^{\#}[e_1]\sigma^{\#} = e_1^n, \sigma_1^{\#} \\ \mathbb{E}^{\#}[e_2]\sigma_1^{\#} = e_2^n, (e_2, d_2) \end{cases} $$
Alors $\gamma(\mathbb{E}^{\#}[e_1 \oplus e_2]\sigma^{\#}) = \{n \in \mathbb{Z} \mid \exists \delta \in \mathcal{P}(\mathbb{X}^n), \delta(v_x) \oplus \delta(v_y) = n \wedge \delta \in \gamma_{\mathbb{Z}}(d)\}$.

Par hypothèse de récurrence,
$$ \begin{cases} \mathbb{E}[e_1]\sigma \in \gamma(\mathbb{E}^{\#}[e_1]\sigma^{\#}) \wedge \sigma \in \sigma_1^{\#} \\ \mathbb{E}[e_2]\sigma \in \gamma(\mathbb{E}^{\#}[e_2]\sigma^{\#}) \wedge \sigma \in \sigma_2^{\#} \end{cases}. $$

On en déduit que $\sigma|_{\mathbb{Z}} \in \gamma_{\mathbb{Z}}(d_2)$. Enfin, par correction de l'assignation, on a $\sigma' = \sigma|_{\mathbb{Z}}[v_x \to \sigma(e_1^n)][v_y \to \sigma(e_2^n)] \in \sigma_2^{\#}[x \to e_1^n][y \to e_2^n] = (\epsilon, d)$. Donc $\sigma' \in \gamma_{\mathbb{Z}}(d)$, $\sigma' \in \mathbb{V} \to \mathbb{Z}$ et $\sigma'(v_x \oplus v_y) = \sigma'(v_x) \oplus \sigma'(v_y) = \sigma'(x) + \sigma'(y) = \mathbb{E}[e_1]\sigma \oplus \mathbb{E}[e_2]\sigma$. D'où $\mathbb{E}[e_1 \oplus e_2]\sigma = \mathbb{E}[e_1]\sigma \oplus \mathbb{E}[e_2]\sigma \in \mathbb{E}^{\#}[e_1 \oplus e_2]\sigma^{\#}$. Enfin, comme $\forall i, \sigma \in \sigma_i^{\#}$, $\sigma \in \sigma_0^{\#} \subseteq \sigma_0^{\#}[r.i.j \to h_{i,j}$. Enfin, $\sigma \le \sigma' \in \sigma_0^{\#}$.

* Si $e = C_l(e_1, \dots, e_n)$, on a $\mathbb{E}[e]\sigma = C_l(\mathbb{E}[e_1]\sigma, \dots, \mathbb{E}[e_n]\sigma)$ (puisque l'expression est bien typée par hypothèse). Rappelons que :

$$ \mathbb{E}^{\#}[C_l(e_1, \dots, e_n)]\sigma^{\#} = (g, \{C_l\}), \sigma_0^{\#}[r.i.j \to h_{i,j}] \\ \text{avec } \left\{ \begin{array}{ll} \mathbb{E}^{\#}[e_i]\sigma^{\#} = v_i, \sigma_i^{\#}, (s, \mathscr{C}) = \bigcup_{e_i:t} v_i, \sigma_0^{\#} = \bigcup_i^{\#} \sigma_i^{\#} \\ h_{i,j} = \begin{cases} s_{l,j} \cup_{D_{l,j}} v_j & \text{si } i = l \wedge \neg(\tau_{l,j} : t) \\ s_{i,j} & \text{sinon} \end{cases} \\ g_{i,j} = \begin{cases} r.i.j & \text{si } \tau_{i,j} : \text{int} \\ h_{i,j} & \text{sinon} \end{cases} \end{array} \right. $$

On a $C_l \in \{C_l\}$. Remarquons que si $ti, j = \text{int}$, on a $\gamma(g_{i,j}, \sigma^{\#}) = \gamma(r.i.j, \sigma^{\#}) = \gamma(h_{i,j}, \sigma^{\#})$ par correction de l'assignation, on peut sans perte de généralités considérer $g_{i,j} = h_{i,j}$ dans la suite. Procédons maintenant par disjonction de cas.

- Soit $j \in [1, n_l]$ tels que $t1, j \neq t$. Par hypothèse de récurrence, on sait que $\mathbb{E}[e_j]\sigma \in \gamma(\mathbb{E}^{\#}[e_j]\sigma^{\#})$. Or, on sait que $g_{l,j} = s_{l,j} \cup_{D_{l,j}} \mathbb{E}[e_j]\sigma$, d'où $g_{i,j} \subseteq \mathbb{E}^{\#}[e_j]\sigma^{\#}$, d'où par croissance de $\gamma_t$, $\gamma_t(g_{i,j}) \subseteq \gamma_t(\mathbb{E}^{\#}[e_j]\sigma^{\#})$. On obtient donc $\mathbb{E}[e_j]\sigma \in \gamma_{l,j}(g_{l,j})$.

- Soit $i \in [1, n_l]$ tels que $ti, j = t$. On a toujours $\mathbb{E}[e_j]\sigma \in \gamma(\mathbb{E}^{\#}[e_j]\sigma^{\#})$. Notons $(C_j, s_j) = \mathbb{E}^{\#}[e_j]\sigma^{\#}$. Remarquons alors que $s_j \subseteq s \subseteq g$ On a alors $(C_j, s_j) \subseteq (g_{i,j}, g)$, donc par croissance de $\gamma_t$, $\gamma_t((C_j, s_j)) \subseteq \gamma_t((g_{i,j}, g))$, c'est-à-dire $\gamma(\mathbb{E}^{\#}[e_j]\sigma^{\#}) \subseteq \gamma_t((g_{i,j}, g))$, d'où $\mathbb{E}[e_j]\sigma \in \gamma_t((g_{i,j}, g))$.

On a donc bien $C_l(\mathbb{E}[e_1]\sigma, \dots, \mathbb{E}[e_n]\sigma) \in \gamma(\mathbb{E}^{\#}[e]\sigma^{\#})$. De plus, $\forall i, \sigma \in \sigma_i^{\#} \subseteq \sigma_0^{\#} \subseteq \sigma_0^{\#}[r.i.j \to h_{i,j}]$

* Si $e$ = if $e_1$ then $e_2$ else $e_3$, on a :

$$ \mathbb{E}[\text{if } e_1 \text{ then } e_2 \text{ else } e_3]\sigma = \begin{cases} \mathbb{E}[e_2]\sigma & \text{si } \mathbb{E}[e_1]\sigma = 0 \\ \mathbb{E}[e_3]\sigma & \text{si } \mathbb{E}[e_1]\sigma = z \in \mathbb{Z} \wedge z \neq 0 \end{cases} $$
Par disjonction de cas :

- Supposons $\mathbb{E}^{\#}[e_1]\sigma = n \in \mathbb{Z}$ et $n \neq 0$, notons $\mathbb{E}^{\#}[e_1]\sigma^{\#} = e^n, \sigma_1^{\#}$. Alors par le lemme C.2, $\sigma \in \mathcal{F}[e]\{\sigma\} \subseteq \gamma(\mathcal{F}^{\#}[e^n]\sigma_1^{\#})$. Donc par hypothèse de récurrence, en notant $\mathbb{E}^{\#}[e_2](\mathcal{F}^{\#}[e^n]\sigma_1^{\#}) = e_2^{\#}, \sigma_2^{\#}$ et $\mathbb{E}[e_2]\sigma \in \gamma(e_2^{\#}, \sigma_2^{\#})$, d'où par croissance de $\gamma$, $\mathbb{E}[e_2]\sigma \in \gamma(\mathbb{E}^{\#}[\text{if } e_1 \text{ then } e_2 \text{ else } e_3]\sigma^{\#})$, et par définition de $\cup^{\#}$, $\sigma \in \sigma_2^{\#} \subseteq \sigma_0^{\#}$

- Si $\mathbb{E}[e_i] = 0$, en remplaçant $e_1$ par $\neg e_1$, le raisonnement est identique.

* Le cas du assert est identique à celui du if.

* Si $e$ = match $e_0$ with $p_1 \to e_1 | \dots | p_m \to e_m$, alors notons match($\sigma, \mathbb{E}[e_0]\sigma, p_1$) = ($\sigma', b_{guard}$) et

match$^{\#}$(σ$^{#}$, E$^{#}$[e$_0$]σ$^{#}$, p) = σ$^{#}$$_m$, σ$^{#}$$_{,m}$. Procédons par disjonction de cas :

- Si $b_{guard}$ = **true**, alors $\mathbb{E}[e]\sigma = \mathbb{E}[e_1]\sigma'$. Or, d'après le lemme C.4, $\sigma' \in \sigma_m^{\#}$. Donc $\mathbb{E}[e_1]\sigma' \in \mathbb{E}^{\#}[e_1]\sigma_m^{\#}$ par hypothèse de récurrence, et comme $\sigma_m^{\#} \neq \emptyset$ (il contient $\sigma$), on a $\mathbb{E}^{\#}[e_1]\sigma_m^{\#} \subseteq \mathbb{E}^{\#}[e_1]\sigma_m^{\#} \cup \mathbb{E}^{\#}[e'_1]\sigma_{,m}^{\#} = \mathbb{E}^{\#}[e]\sigma^{\#}$, on a bien $\mathbb{E}[e]\sigma \in \gamma(\mathbb{E}^{\#}[e]\sigma^{\#})$. Toujours par définition de $\cup^{\#}$, on a bien $\sigma \in \sigma_0^{\#}$.

- Sinon, si $b_{guard}$ = **false** et $m > 1$, alors par le lemme C.4, $\sigma' \in \sigma_{,m}^{\#}$. Alors par hypothèse de récurrence, en notant $e'_1$ = match $e_0$ with $p_2 \to e_2 | \dots | p_m \to e_m$, on a $\mathbb{E}[e'_1]\sigma \in \gamma(\mathbb{E}^{\#}[e'_1]\sigma^{\#})$ et comme $m > 1$, on a bien : $\mathbb{E}^{\#}[e'_1]\sigma_m^{\#} \subseteq \mathbb{E}^{\#}[e_1]\sigma_m^{\#} \cup \mathbb{E}^{\#}[e'_1]\sigma_{,m}^{\#} = \mathbb{E}^{\#}[e]\sigma^{\#}$. De même, $\sigma \in \sigma_0^{\#}$.

- Enfin, si $b_{guard}$ = **false** et $m = 1$, alors $\sigma' \in \sigma_{,1}^{\#}$, donc $\sigma_{,1}^{\#} \neq \emptyset$, donc on appelle récursivement lanalyce avec $m = 0$ d'où $\mathbb{E}^{\#}[e]\sigma^{\#} \subseteq \Omega$ donc on a bien $\omega \in \Omega$.

* Si $e$ = let $x = e_1$ in $e_2$, alors en notant $\mathbb{E}^{\#}[e_1]\sigma^{\#} = e^{\#}, \sigma^{\#}$, puisque $\mathbb{E}[e_1]\sigma \in \gamma(\mathbb{E}^{\#}[e_1]\sigma^{\#})$ et $\sigma \in \sigma^{\#}$, on a $\sigma[x \to \mathbb{E}[e_1]\sigma] \in \sigma^{\#}[x \to e^{\#}]$ par correction de l'assignation, donc par hypothèse de récurrence, $\mathbb{E}[e_2]\sigma[x \to \mathbb{E}[e_1]\sigma] \in \gamma(\mathbb{E}^{\#}[e_2]\sigma^{\#}[x \to e^{\#}])$ et $\sigma[x \to \mathbb{E}[e_1]\sigma] \subseteq \sigma^{\#}[x \to e^{\#}]$, d'où $\mathbb{E}[e]\sigma \in \mathbb{E}^{\#}[e]\sigma^{\#}$ et $\sigma \in \sigma_0^{\#}$.

* Si $e = e_0 \dots e_n$. Comme $e$ est bien typé, $\mathbb{E}^{\#}[e_0]\sigma^{\#} = (x_1, \dots, x_n, e^{\#}, \sigma_0^{\#})$. Notons que par hypothèse de récurrence et par construction de l'abstraction de fun, $\sigma \in \sigma_0^{\#}$. Notons $\mathbb{E}^{\#}[e_i]\sigma^{\#} = e_i^{\#}, \sigma_i^{\#}$. Par hypothèse de récurrence, on a également $\forall i, \mathbb{E}[e_i]\sigma^{\#} \in \gamma(e_i^{\#}, \sigma_i^{\#})$. Or, par hypothèse de récurrence, $f = \mathbb{E}[e_0]\sigma \in \gamma(\mathbb{E}^{\#}[e_0]\sigma^{\#})$, par définition de la concrétisation pour les abstractions de fonction, on en conclut que $\mathbb{E}[e] = f(\mathbb{E}[e_1]\sigma, \dots, \mathbb{E}[e_n]\sigma) \in \gamma(e^{\#}, \sigma_0^{\#}[x_i = e_i^{\#}]) = \gamma(\mathbb{E}^{\#}[e]\sigma^{\#})$. Comme $x_i \notin \sigma$, on a également $x_i \in \sigma_0^{\#}[x_i = e_i^{\#}]$.

* Si $e$ = fun $x_1 \dots x_n \to e_0$. On a $\mathbb{E}^{\#}[e]\sigma^{\#} = (x_1, \dots, x_n, \mathbb{E}^{\#}[e_0]\sigma^{\#}[x_1 \to \top, \dots, x_n \to \top]$
⊤)], σ$^{‡}$) et $\mathbb{E}[e]\sigma = \lambda a_1 \dots a_n \mathbb{E}[e_0]\sigma[x_i \to a_i]$. Soit $a_1 : \tau_1, \dots, a_n : \tau_n$ et $v_1 \in D_1, \dots, v_n \in D_n$ tels que $a_i \in \gamma(v_i, \sigma_i^\sharp)$. On a $f(a_1, \dots, a_n) = \mathbb{E}[e_0]\sigma[x_i \to a_i]$. On note $\mathbb{E}^\sharp[e_0]\sigma^\sharp[x_i \to \top]) = e^\sharp, \sigma_1^\sharp$. Remarquons que $\sigma[x_i \to a_i] \in \sigma^\sharp[x_i \to \top]$. Alors par hypothèse de récurrence $\mathbb{E}[e_0]\sigma[x_i \to a_i] \in \gamma(\mathbb{E}^\sharp[e_0]\sigma^\sharp[x_i \to \top]) = \gamma(e^\sharp, \sigma_1^\sharp)$ et $\sigma[x_i \to a_i] \in \sigma_1^\sharp$, que $a_i \in \gamma(v_i, \sigma_i^\sharp)$, on a $\sigma[x_i \to a_i] \in \sigma_1^\sharp[x_i = v_i]$, donc on conclut que $\mathbb{E}[e_0]\sigma[x_i \to a_i] \in \gamma(e^\sharp, \sigma_1^\sharp[x_i = v_i])$. On obtient donc bien $f \in \gamma(\mathbb{E}^\sharp[e]\sigma^\sharp)$. On a $\sigma \in \sigma_0^\sharp = \sigma^\sharp$.

* Si $e = \text{let rec } x_f = e_1$ in $e_2$. On a :

$$ \mathbb{E}[\text{let rec } x_f = e_1 \text{ in } e_2]\sigma = \begin{cases} \mathbb{E}[e_2]\sigma[x_f \to \text{lfp}(F_{x_f,x,g})] & \text{si } \mathbb{E}[e_1]\sigma = \lambda x_1 \dots x_n g \\ \omega & \text{sinon} \end{cases} \\ \text{avec } F_{x_f,x,g}(\phi) = \lambda y \cdot \mathbb{E}[g]\sigma[x \to y, x_f \to \phi] $$

On sait que $\text{lfp}(F_{x_f,x,g})$ vaut $\bigcup_{n \in \mathbb{N}} (F_{x_f,x,g}^n(\bot))$. Remarquons qu'on peut écrire $\lambda y.\mathbb{E}[g]\sigma[x \to y, x_f \to \phi] = \mathbb{E}[e_1]\sigma[x_f \to \phi]$. Alors étant donné $v$, par hypothèse de récurrence, pour $v \in \gamma(v^\sharp)$, on a $F_{x_f,x,g}(v) = \mathbb{E}[e_1]\sigma[f \to v] \in \gamma(\mathbb{E}^\sharp[e_1]\sigma^\sharp[x_f \to v^\sharp]) = \gamma(F^\sharp(v^\sharp))$.

En conséquence, en remarquant que $(x_1, \dots, x_n, \bot, \sigma^\sharp[x_1, \dots, x_n]) = \bot$ dans le domaine des fonctions, on a bien $\bigcup_{n \in \mathbb{N}} (F_{x_f,x,g}^n(\bot)) \in \gamma(\bigcup_{n \in \mathbb{N}} ((F^\sharp)^n(\bot)))$ par sûreté de $\cup^\sharp$. Comme $\nabla$ est un opérateur d'élargissement, donc cette opération converge et sur-approxime $\cup^\sharp$, on a donc $\text{lfp}(F_{x_f,x,g}) \in \gamma(\nabla_{n \in \mathbb{N}}^\sharp((F^\sharp)^n(\bot)))$.

D'où $\sigma[x_f \to \text{lfp}(F_{x_f,x,g})] \in \sigma^\sharp[x_f \to \nabla_{n \in \mathbb{N}}^\sharp((F^\sharp)^n(\bot))]$. Le raisonnement qui suit est similaire à celui du let.

□

# Annexe E Correspondance de Galois

**Définition E.1.** Si $\forall i, j, \mathcal{T}_{ti,j} \stackrel{\gamma_{\tau_{i,j}}}{\longleftarrow} \mathcal{D}_{i,j}$, on peut définir $\alpha$ récursivement de la manière suivante :

$$ \alpha(\mathrm{Ci}(x_{i,1}, \dots, x_{i,n_i})) = \left( \begin{array}{ll} \times & \left\{ \begin{array}{ll} \alpha_{i,j}(x_{i,j}) & \text{si } i' = i \land \mathrm{ti}, j \neq t \\ \bot & \text{sinon} \end{array} \right\} \\ \bigcap_{\substack{1 \le i' \le n \\ 1 \le j \le n_i}} & \bigcup_{\mathrm{ti}, j \neq t} \alpha(x_{i,j}) \end{array} \right) $$

On a alors la correspondance de Galois $\mathcal{T} \stackrel{\gamma}{\longleftarrow} \mathcal{D}_t$.
# Annexe F Listings des benchmarks

```hml
let x = Cons(1, Cons(2, Cons(3, Nil))) in
let y = Nil in
let z = Cons(4, x) in
```

```
x : { Cons }      x_1,1 : [1, 3]      x_1,2 : { Nil, Cons }
y : { Nil }       y_1,1 : [1, 4]      y_1,2 : { Nil, Cons }
z : { Cons }       z_1,1 : [1, 4]      z_1,2 : { Nil, Cons }
```

<caption>Listing 1: list.ml</caption>

```hml
type tree = Node of tree * int * tree | Leaf of int
let x = Node(Node(Leaf(250), 100, Leaf(251)), 1, Leaf(252)) in
```

```
x: { Node }   x_1,1: { Node, Leaf }   x_1,2: [1, 100]   x_1,3 {Leaf}
              x_2,1: [250,252]
```

<caption>Listing 2: tree.ml</caption>

```hml
let x = match Cons(1, Nil) with
  | Cons(h,q) -> h
;;
assert (x = 1)
```

```
x : [1,1]
```

<caption>Listing 3: match.ml</caption>

```hml
let x = match Cons(1,Cons(2, Nil)) with
  | Cons(h,q) -> h
;;
assert (x < 3)
```

```
x : [1,2]
```

<caption>Listing 4: match2.ml</caption>
```h
let x = match Cons(1, Cons(2, Nil)) with
  | Cons(h, q) -> h
;;
assert (x = 1)
```

```
x : [1,2]
Warning : assertion failure
```

<caption>Listing 5: match-alarm.ml</caption>

L'abstraction de $x$ est identique, mais renvoie cette fois : `Warning: assertion failure`. En effet, comme $x : [1,2]$, si $x=1$, il s'agit d'une fausse alarme - c'est effectivement le cas ici.

```h
let x = match Cons(1, Cons(2, Nil)) with
  | Cons(h, q) -> h
;;
assert (x = 3)
```

```
x : [1,2]
Error : assertion failure
```

<caption>Listing 6: match_error.ml</caption>

L'abstraction de $x$ est identique, mais renvoie cette fois : `Error: assertion failure`. En effet, puisque l'intersection entre $[1,2]$ et $[3,3]$ est vide, il s'agit effectivement d'une erreur.

```h
let f x y = x + y ;;
let z = f 1 2 ;;
assert (z = 3)
```

```
z : [3,3]
```

<caption>Listing 7: add.ml</caption>
# Vérification symbolique de protocoles cryptographiques en F*: application au sous-protocole TreeSync de MLS

Théophile Wallez

Inria Paris

## Résumé

TreeSync est un sous-protocole d'authentification pour MLS, un protocole de message-rie de groupe sécurisé en cours de standardisation à l'IETF. Nous formalisons MLS en F*, et présentons un théorème de sécurité pour TreeSync à l'aide du cadriciel de cryptographie symbolique DY*. Afin de comprendre les hypothèses clés qui permettent d'exprimer un tel théorème, nous présentons en détail le fonctionnement interne de DY*. Au cours de notre analyse, nous avons proposé plusieurs changements à TreeSync qui ont été intégrés à MLS, et avons développé de nouvelles méthodes de preuves pour passer à l'échelle avec DY* afin de pouvoir s'attaquer à un gros protocole comme MLS, par exemple, un mécanisme permettant à la fois l'exécution concrète et symbolique du protocole, la génération auto-matique de parseurs et sérialiseurs binaires vérifiés, ou encore la génération d'invariants globaux du protocole à partir d'invariants locaux.

## 1 Introduction

**Messagerie de groupe sécurisée.** Que ce soit WhatsApp, Signal, Facebook Messenger ou Wire, toutes les applications de messagerie moderne exposent le chiffrement de bout-en-bout comme l'une de leurs fonctionnalités phare, ce qui confirme que la communication privée et sé-curisée est maintenant un aspect important pour les utilisateurs. Contrairement aux connexions HTTPS de courte durée, les conversations peuvent s'étaler sur des années, donc les garanties de sécurité des messageries doivent prendre en compte la possibilité réaliste qu'un des appareils se fasse voler ou compromettre pendant la durée de vie de la conversation. Si un adversaire compromet un appareil, il pourra bien sûr lire les messages récents et envoyer de nouveaux messages, mais nous voulons protéger les messages envoyés dans le passé lointain (*confidentia-lité persistante*), ainsi que les messages envoyés ou reçus dans le futur après une période de guérison (*sécurité après compromission*).

Entre deux personnes, ces messageries utilisent le protocole Signal [22] qui possède toutes les propriétés de sécurité requises. Les conversations de groupes sont fondamentalement différentes : des participants peuvent entrer et partir de la conversation à n'importe quel moment, il faut donc qu'un participant enlevé d'un groupe ne puisse plus lire les messages envoyés après, propriété que l'on peut obtenir grâce à la sécurité après compromission. Les protocoles actuellement utilisés pour les conversations de groupe ayant la propriété de sécurité après compromission dépendent de $n^2$ canaux Signal (un pour chaque paire de participants), ce qui n'est pas efficace.

**Messaging Layer Security (MLS).** Le groupe de travail IETF MLS a pour but de concevoir un protocole de messagerie de groupe efficace ayant les propriétés de confidentialité persistante et de sécurité après compromission [6]. MLS peut se découper en trois sous-protocoles : Tree-KEM se charge de calculer un secret partagé entre tous les membres d'un groupe à un instant donné, TreeDEM se charge de chiffrer les messages à partir du secret de groupe, et TreeSync se charge d'authentifier l'appartenance au groupe. L'authentification est un composant crucial : avant de dire que les communications sont confidentielles, il faut d'abord savoir entre qui elles pourraient être déclarées comme telles.
**Preuve de protocole assistée par ordinateur.** Nous avons pour objectif de faire une preuve formelle de sécurité pour MLS, c'est-à-dire une preuve vérifiée avec un assistant de preuve ou un outil dédié. Plusieurs méthodologies existent. Les preuves de sécurité calculatoires, en utilisant des outils comme Squirrel [5], EasyCrypt [7] ou CryptoVerif [12], utilisent des jeux cryptographiques pour borner la probabilité qu'un attaquant puisse casser un protocole cryptographique. Les preuves de sécurité symboliques, en utilisant des outils comme ProVerif [13], Tamarin [25] ou DY* [9], supposent que les primitives cryptographiques sont parfaites.

Nous choisisons ici d'utiliser le modèle symbolique, parce que les preuves sont moins complexes qu'avec le modèle calculatoire, ce qui permet d'étudier des protocoles gros et complexes comme MLS.

**Contributions.** Nous présentons un théorème de sécurité pour TreeSync prouvé dans le modèle symbolique en F* [31] à l'aide du cadriciel DY* [9], sous des hypothèses raisonnables sur TreeKEM et TreeDEM. Durant notre analyse, nous avons trouvé une attaque exploitant les interactions entre TreeSync et TreeDEM, et montré que les garanties de TreeSync n'étaient pas aussi fortes qu'initialement espérées. Nous avons proposé des modifications du protocole résolvant ces problèmes, qui sont depuis intégrées à MLS. Notre spécification est précise à l'octet près et est interopérable avec d'autres implémentations. La description complète du protocole et de sa preuve font l'objet d'un autre article [38].

Afin de bien comprendre la signification d'un tel théorème, nous expliquons en détail le fonctionnement interne de DY*, afin de saisir quelles sont les hypothèses clés qui font tenir l'édifice. Au cours de notre analyse, nous avons développé de nouveaux outils et méthodes de preuves afin de passer à l'échelle et accomplir la preuve d'un protocole de cette taille en DY*.

**Sommaire.** Nous commençons par une introduction à la preuve de protocole symbolique (§2) avant d'expliquer comment DY* permet de réaliser de telles preuves (§3), puis montrons les nouvelles méthodes de preuve que nous avons développées (§4) pour étudier le protocole TreeSync et décrivons l'impact qu'a eu notre travail sur MLS (§5), et concluons avec les travaux connexes (§6).

# 2 Analyse symbolique de protocoles

## 2.1 Modélisation de l'attaquant

**L'attaquant.** On se place dans le pire cas et on suppose que le monde entier cherche à casser notre protocole. Si le protocole est sécurisé malgré tous ces efforts, alors il sera aussi sécurisé dans un cas plus réaliste. Ainsi, on considère que l'attaquant représente tout ce qui est extérieur aux participants honnêtes du protocole, qu'il a un contrôle total du réseau et peut donc lire tous les messages envoyés, les modifier ou décider qu'ils ne soient pas livrés, envoyer des messages en se faisant passer pour d'autres personnes, et enfin faire des manipulations cryptographiques avec les données qu'il connaît.

**Cryptographie symbolique.** L'analyse symbolique de protocole, à la Dolev-Yao [18], abstrait les primitives cryptographiques en supposant qu'elles sont parfaites : par exemple, une fonction de hachage n'est pas inversible et est sans collision, ou encore le chiffrement symétrique d'un message à l'aide d'une clé ne peut se déchiffrer qu'à partir de la même clé.

Dans des outils d'analyse symbolique comme Tamarin [25], Proverif [13] ou DY* (§3.1), cela se modélise via des constructeurs et des règles de réduction : par exemple le chiffrement symétrique se modélise avec le constructeur SymEnc(cle, msg) et se détruit avec la règle de
<figure><img src="image_92.png" /><figcaption>FIGURE 1 – Un premier essai pour MiniTLS. PkEnc(pk, msg) est le chiffrement de msg pour la clé publique de chiffrement pk, et SymEnc(key, msg) est le chiffrement de msg pour la clé symétrique key.</figcaption></figure>

réduction SymDec(cle, SymEnc(cle, msg)) = msg. Sans autre règle de réduction, cela capture bien l'idée que SymEnc(cle, msg) ne peut se déchiffrer qu'avec la clé cle.

## 2.2 Cas d'étude : MiniTLS

Un protocole utilisé au quotidien est celui qui sécurise les connexions entre les navigateurs web et les sites web : il se nomme TLS. Essayons de construire un protocole ayant un cas d'usage similaire, que nous appellerons MiniTLS malgré les différences flagrantes qu'il a avec TLS : en effet, TLS dispose de nombreuses fonctionnalités dont nous ne nous soucierons pas ici ; MiniTLS est un protocole jouet qui n'a pas vocation à être utilisé dans la vie courante. Afin de rester dans la tradition, on appellera le navigateur web Alice et le site web Bob. Mallory essayera par la suite d'écouter la conversation.

Le chiffrement asymétrique étant en général moins efficace que le chiffrement symétrique, on l'utilise pour se mettre d'accord sur une clé symétrique (*sym_key*), qui est ensuite utilisée pour échanger les messages. Une première tentative basée sur ce principe est décrite Figure 1 : Alice envoie une clé publique de chiffrement à Bob, celui-ci génère *sym_key*, la chiffre avec la clé publique de chiffrement d'Alice et la lui envoie. Alice et Bob peuvent ensuite communiquer en chiffrant symétriquement avec *sym_key*.

Ce protocole n'est pas sécurisé. En effet, Mallory (un attaquant Dolev-Yao) peut effectuer une attaque dite de l'« homme du milieu » pour obtenir le message confidentiel, comme décrit dans la Figure 2 : Mallory intercepte pkA, envoie sa propre clé pkM à Bob. Ensuite Mallory déchiffre le message de Bob et récupère *sym_key* avant de le chiffrer pour Alice. Mallory peut donc lire tous les messages *msg* par la suite.

Pour réparer ce protocole et obtenir la version finale de MiniTLS décrite dans la Figure 3, on ajoute une signature de la part de Bob (que Mallory ne peut pas falsifier), qu'Alice vérifie par la suite avec la clé publique de vérification de signature de Bob.

Un problème subsiste : comment Alice peut-elle faire le lien entre l'identité de Bob et la clé de publique de vérification de signature de Bob ? Ce lien est crucial, sinon Alice pourrait utiliser la clé publique de vérification de signature de Mallory à la place de celle de Bob sans le savoir, et une attaque très similaire à celle décrite Figure 2 serait possible.

Ce problème ne se résout usuellement pas à l'aide de la cryptographie. Par exemple, HTTPS résout ce problème en le déléguant à un tiers de confiance [30, C.2] : les autorités de certifications sont responsables de faire le lien entre identité et clé publique, et fournissent des certificats que
<figure><img src="image_93.png" /><figcaption>FIGURE 2 – Une attaque sur le premier essai de MiniTLS décrit dans la Figure 1. L’attaquant Dolev-Yao nommé « Mallory » obtient $sym\_key$ et peut déchiffrer tous les messages suivants.</figcaption></figure>

<figure><img src="image_94.png" /><figcaption>FIGURE 3 – Une version corrigée et sécurisée de MiniTLS. Une signature est rajoutée par rapport au premier essai décrit dans la Figure 1. $Sign(sk, msg)$ est la signature de $msg$ avec la clé de signature sk, et [a; b] représente une concaténation non-ambigue de a et b.</figcaption></figure>

les navigateurs peuvent vérifier. Les navigateurs possèdent une liste d'autorités de certification dignes de confiance, et rejettent les certificats n'émanant pas de cette liste. Signal propose une autre solution à ce problème [23, 4.1] et les utilisateurs doivent vérifier leur identité via un autre canal. C'est un problème qu'on ne traitera pas dans cette étude de cas.

**Sécurité de MiniTLS.** Une première chose à remarquer avant d'énoncer un théorème de sécurité sur MiniTLS, est qu'Alice sait qui est Bob, mais Bob ne sait pas qui est Alice. Ainsi on ne peut pas garantir qu'un message envoyé par Bob est confidentiel entre Alice et Bob, on ne pourra que prouver qu'il est confidentiel entre Bob et les personnes connaissant la clé privée associée à pkA.

Le théorème de sécurité que nous allons énoncer est informel, et nous ne couvrirons que dans les grandes lignes sa preuve, informelle elle aussi. Le théorème sera plus tard formalisé précisément en F* à l'aide du cadriciel DY* (§3.4), et la preuve formelle sera similaire à la preuve informelle ci-dessous.

Au cours de la preuve, nous allons parfois dire qu'une donnée « ne peut être connue que de A et B », cela veut dire que par la suite nous vérifierons que cette donnée ne peut pas fuiter et être connue (par exemple) de C.

**Théorème.** Pour chaque message $msg$ transféré dans la dernière phase du protocole, si, du point de vue d'Alice, $msg$ ne peut être connu que d'Alice et Bob, ou du point de vue de Bob, $msg$ ne peut être connu que de Bob et des personnes connaissant la clé privée associée à pkA, alors
<figure><img src="image_95.png" /><figcaption>FIGURE 4 – Protocole SigneTout.</figcaption></figure>

le chiffrement de msg avec sym_key et l'envoi sur le réseau comme fait dans la dernière phase du protocole ne fait pas fuiter d'information.

Esquisse de preuve de la sécurité de msg. Il suffit de prouver que sym_key, du point de vue d'Alice, ne peut être connu que d'Alice et Bob, ou du point de vue de Bob, ne peut être connu que de Bob et des personnes connaissant la clé privée associée à pkA. En effet, pour des messages msg vérifiant les conditions ci-dessus, chiffrer msg avec sym_key et le diffuser sur le réseau implique que msg sera divulgué aux personnes connaissant sym_key, ce qui correspond aux personnes qui ont le droit de connaître msg donc cela ne fait pas fuiter d'information. ☐

Esquisse de preuve de la sécurité de sym_key. Prouvons maintenant la propriété pour sym_key.

Alice commence par générer une paire de clés de chiffrement asymétrique, la clé privée ne pouvant être connue que d'elle-même et la clé publique étant publique. Alice envoie la clé publique pkA sur le réseau, ce qui ne fait pas fuiter d'informations puisqu'elle est publique.

Bob reçoit pkA, une clé publique de chiffrement. Bob génère sym_key avec l'intention que cela ne puisse être connu que de lui-même et des personnes connaissant la clé privée associée à pkA. Bob effectue sa signature sur [pkA; sym_key], et chiffre avec la clé publique de chiffrement pkA un message contenant sym_key ainsi que la signature, avant de l'envoyer sur le réseau. Divulguer ce chiffrement au réseau de fait pas fuiter d'informations : seules les personnes connaissant la clé privée associée à pkA peuvent déchiffrer le message, et le contenu du message pouvant en effet être connu de ces personnes.

Alice reçoit le message, déchiffre et vérifie la signature. Puisque la clé de signature de Bob skB n'est connue que de Bob, Alice sait que c'est bien Bob qui a fait la signature et pas un attaquant. Lorsque Bob a fait la signature, la propriété suivante était vraie (c'est un invariant pour toutes les signatures du protocole) : sym_key peut être connue exactement par Bob et par les personnes connaissant la clé privée associée à pkA. Alice sait qu'elle seule connaît la clé privée associée à pkA, elle en déduit donc que sym_key n'est connu que d'elle-même et Bob. ☐

Un argument récurrent au cours de la preuve est qu'on ne chiffre un message que lorsque celui-ci est moins secret que la clé qui permet déchiffrer le message (que ce soit dans le cas symétrique ou asymétrique). De plus, la preuve repose sur un invariant sur les signatures : l'invariant est vrai lorsque Bob effectue la signature, plus tard quand Alice vérifie la signature elle sait que l'invariant est vrai. Ces techniques de preuves seront plus tard utilisées en F* (§3.2).

## 2.3 Modularité des protocoles

Nous étudions la sécurité de MLS en le décomposant en trois sous-protocoles (TreeSync, TreeKEM et TreeDEM). Cependant, la sécurité des protocoles cryptographiques ne se compose pas bien.
En effet, considérons le protocole SigneTout décrit Figure 4, qui signe n'importe quel message qu'on lui envoie. Si en parallèle de MiniTLS, nous exécutons le protocole SigneTout avec la même clé de signature, alors MiniTLS n'est plus sécurisé : en effet la signature dans le deuxième message de MiniTLS est obtenable par Mallory en utilisant le protocole SigneTout avec `msg = [pkA; sym_key]`. Ainsi, l'attaque de l'homme du milieu décrite dans la Figure 2 est à nouveau réalisable.

Une façon de composer les protocoles est de prouver qu'ils n'interfèrent pas entre eux : par exemple s'ils utilisent des clés de signature différentes, où s'ils signent des ensembles de messages disjoints. Cette dernière possibilité peut être réalisée en incluant un tag dans le message signé : par exemple MiniTLS signera le message `"MiniTLS"; pkA; sym_key` et SigneTout signera le message `"SignTout"; msg`, rendant ainsi toute signature réalisée dans un des protocoles inutilisable dans l'autre protocole.

Nous avons trouvé une attaque exploitant l'interférence entre les signatures de TreeSync et TreeDEM, que nous avons corrigée en ajoutant un tag de façon systématique dans toutes les signatures de MLS (§5).

## 3 Preuve symbolique de protocoles cryptographiques avec DY*

Nous allons décrire ici le fonctionnement interne de DY* [9], un cadriciel de vérification de protocole contre un attaquant Dolev-Yao (§2.1), écrit en F* [31].

Les analyseurs de protocole symbolique comme ProVerif [13] ou Tamarin [25] sont complètement automatisés : à partir d'une description de protocole, ils prouvent la sécurité du protocole dans le modèle symbolique ou exhibent une attaque, ceci sans interaction supplémentaire de la part de l'utilisateur. Les preuves en DY* sont beaucoup plus manuelles, ce qui en contrepartie donne certains avantages : si les analyseurs automatiques brillent sur des protocoles avec quelques échanges de message (comme TLS [10]), DY* peut s'attaquer à des protocoles beaucoup plus gros, comme une preuve de Signal avec un nombre non borné de messages [9, §4], ou encore MLS (nombre non-borné de messages et de participants), l'objectif de cet article. De plus, la façon dont les preuves sont faites en DY* est compréhensible par un humain, et ressemble dans les grandes lignes à la preuve de MiniTLS (§2.2).

Le fonctionnement décrit par la suite est simplifié : DY* permet de modéliser un attaquant qui compromet dynamiquement l'état (secret) des participants du protocole au cours du temps, ainsi la plupart des prédicats de DY* sont paramétrés par le temps. Nous omettons ceci dans la description qui suit.

### 3.1 Bytes symboliques et pouvoir de l'attaquant

**Constructeurs.** La modélisation des primitives cryptographiques se fait à l'aide de constructeurs et de règles de réduction (§2.1). Nous modélisons les suites d'octets à l'aide d'un type inductif appelé bytes, où les constructeurs de bytes correspondent aux constructeurs des primitives cryptographiques.

En F*, cela ressemble à :

type bytes =

| PublicVal: public_bytes → bytes // Donnée publique

| Rand: len:nat → timestamp → label → bytes // Aléatoire

| Concat: lhs:bytes → rhs:bytes → bytes // Concaténation
Hash: bytes → bytes // Fonction de hachage

Pk: sk:bytes → bytes // Clé publique de chiffrement à partir de clé privée de déchiffrement

PkEnc: pk:bytes → msg:bytes → bytes // Chiffrement à clé publique

SymEnc: key:bytes → msg:bytes → bytes // Chiffrement symétrique

Vk: sk:bytes → bytes // Clé publique de vérification à partir de clé privée de signature

Sign: sk:bytes → msg:bytes → bytes // Signature d'un message

... // Insérer ici tous les autres constructeurs à considérer (MAC, KDF, DH, ...)

val length: bytes → nat // On dispose d'une fonction de longueur

Le type bytes modélise des suites d'octets que l'on peut concaténer, hacher, signer, chiffrer symétriquement et asymétriquement.

Les suites d'octets publiques sont représentées par le constructeur `PublicVal`, et les suites d'octets aléatoires fraîchement générées sont représentées par le constructeur `Rand`. Les suites d'octets aléatoires possèdent une longueur afin de pouvoir définir la fonction `length` dessus. La fraîcheur est modélisée par le timestamp, ce champ n'étant pas choisi par l'utilisateur de DY\*: ce dernier ne peut construire des données aléatoires qu'à travers un effet (décrit dans §3.3) qui donne la garantie que tous les timestamps sont différents. Les personnes ayant le droit de connaître une donnée aléatoire doivent être choisies dès sa génération : c'est ce à quoi correspond le type label dans le constructeur `Rand`, qui sera décrit plus tard dans cette section.

En pratique, le type `bytes` est totalement opaque pour le code utilisant DY\*. Ainsi les constructeurs sont cachés derrière des fonctions :

let concat (lhs:bytes) (rhs:bytes): bytes = Concat lhs rhs

let hash (msg:bytes): bytes = Hash bytes

// ...

Un utilisateur de DY\* ne peut donc pas inspecter la façon dont un `bytes` a été construit, à part à travers les règles de réduction.

**Règles de réduction.** Les règles de réduction sont implémentées à l'aide de fonctions en F\* qui opèrent sur le type `bytes`. Par exemple, un déchiffrement asymétrique réussit uniquement lorsque la suite d'octets est un chiffrement asymétrique avec une clé publique associée à la bonne clé privée.

let pk_dec (sk:bytes) (msg_chiffre:bytes): option bytes =

match msg_chiffre with

| PkEnc (Pk sk') msg_clair →
  if sk = sk' then Some msg_clair

else None // Pas la bonne clé

| _ → None // Pas un chiffré

De la même manière, on peut séparer une suite d'octets en deux uniquement lorsque la suite d'octets est une concaténation, et que l'indice auquel la séparation s'effectue se situe exactement entre les deux suites d'octets concaténées.

let split (i:nat) (msg:bytes): options bytes =

match msg with

| Concat lhs rhs →
  if i = length lhs then

Some (lhs, rhs)
else None // Pas le bon indice

| _ → None // Pas une concaténation
**Pouvoir de l'attaquant.** On modélise le pouvoir de l'attaquant Dolev-Yao (§2.1) avec le prédicat `attacker_knows`: l'attaquant connaît les valeurs publiques, les messages envoyés sur le réseau, et peut appliquer les fonctions cryptographiques sur les valeurs déjà connues.

La modélisation de la connaissance des messages envoyés sur le réseau se fait via un effet (décrit dans §3.3). Comme cet effet modélise un état croissant (un journal d'évènements, stockant entre-autres les messages envoyés sur le réseau), nous pouvons utiliser les fonctionnalités de témoin [1] de F*, et ainsi définir le prédicat `msg_sent_on_network` comme témoin de l'existence du message dans le journal.

```pascal
let attacker_knows (b:bytes): prop =
  (msg_sent_on_network b) ∨
  (∃ public_bytes. b == PublicVal public_bytes) ∨
  (∃ b1 b2. attacker_knows b1 ∧ attacker_knows b2 ∧ b == concat b1 b2) ∨
  (∃ pk msg. attacker_knows pk ∧ attacker_knows msg ∧ b == pk_enc pk msg) ∨
  (∃ sk msg. attacker_knows sk ∧ attacker_knows msg ∧ Some b == pk_dec sk msg) ∨
  ...
```

Ce prédicat est crucial dans la modélisation du pouvoir de l'attaquant, et fait partie de la base de confiance de DY*. On ne peut pas prouver que rien n'a été oublié lors de sa définition, mais on peut s'en convaincre, par exemple en instanciant la classe de type permettant de faire des opérations cryptographiques (§4.2) sur le type `bytes` raffiné avec la propriété `attacker_knows`. Si une propriété manquait dans le `attacker_knows`, alors cela se remarquerait lors de la définition de la fonction associée dans la classe de type.

**Labels.** De la même façon qu'il est courant de renforcer un théorème pour pouvoir le prouver par induction, le prédicat `attacker_knows` est trop peu précis pour faire des preuves de sécurité. Nous introduisons un treillis de labels, permettant de décrire l'ensemble des personnes connaissant une donnée. Les labels permettent de décrire des choses comme « cette donnée n'est connue que d'Alice et Bob », ou encore « cette donnée n'est connue que de Bob et des personnes qui connaissent la clé privée associée à une clé publique », comme nous l'avons fait dans la preuve de sécurité de MiniTLS (§2.2).

Les labels formant un treillis, on peut comparer deux labels et dire qu'un label est moins sécurisé qu'un autre : toute personne pouvant connaître les données associées au label plus sécurisé peut connaître les données associées au label moins sécurisé. Cela permet de modéliser le fait que quelqu'un, par exemple Alice, a le droit de connaître une certaine donnée, en disant que le label de la donnée est moins sécurisé que le label « connu que d'Alice ». Ce treillis n'est pas total, par exemple le label « connu que d'Alice » et le label « connu que de Bob » ne sont pas comparables.

```pascal
// Opérations de treillis
val (<#>: l1:label → l2:label → prop // Relation d'ordre : l1 est moins secret que l2
val union: label → label → label // Borne inférieure
val intersection: label → label → label // Borne supérieure
```

```pascal
val public: label // Donnée connue par tout le monde : c'est un minimum global du treillis
val readers: list identity → label // Donnée connue que par la liste d'identités
```

Pour chaque suite d'octets, on peut obtenir son label :

```pascal
let get_label (b:bytes): label =
  match b with
  | PublicVal _ → public
```
```
Rand len lab -> lab
//...
Hash b -> get_label b
Pk sk -> public
PkEnc sk msg -> public
SymEnc sk msg -> public
//...
```

**Lien entre attaquant et label.** On prouve le théorème suivant : si une donnée est associée à un label secret, alors l'attaquant ne peut pas connaître cette donnée.

```
val attacker_dont_know_secret_values:
b:bytes -> identities:List<identity> ->
Lemma (get_label b == readers identities =\> ¬(attacker_knows b))
```

Ce théorème se déduit à partir de deux théorèmes plus bas niveau. Le premier dit que si un attaquant connaît une donnée, alors le label associé à cette donnée est moins sécurisée que public, et le second dit que le label readers identities n'est pas moins sécurisé que le label public.

## 3.2 Propriété clé des messages circulant sur le réseau

Dans les analyseurs de protocole symbolique automatiques comme ProVerif ou Tamarin, l'analyseur dispose de la spécification complète du protocole, et connaît donc toutes les utilisations de la cryptographie faites par les personnes honnêtes : ils peuvent raisonner sur le protocole dans sa globalité. Par exemple, ils peuvent raisonner sur l'ensemble des signatures effectuées dans un protocole, et prouver qu'elles n'interfèrent pas entre elles. Ce n'est pas le cas dans un assistant de preuve générique comme F\*, qui ne peut raisonner qu'à une échelle plus locale, sur un ensemble fixé de fonctions effectuant de la cryptographie. C'est en fait un problème similaire à la composition de la sécurité des protocoles (§2.3), si nous prouvons qu'une certaine fonction fait des opérations sécurisées avec une clé de signature, rien ne nous empêche d'écrire après-coup une autre fonction qui signe n'importe quel message.

**Invariant clé des messages circulant sur le réseau.** Nous imposons donc que les participants honnêtes d'un protocole obéissent à certaines règles. Par exemple, ils ne peuvent envoyer sur le réseau que des données publiques (c'est-à-dire, dont le label est moins sécurisé que public). De plus, on impose une certaine discipline sur les opérations cryptographiques exécutées : par exemple, on autorise à chiffrer un message avec une clé uniquement lorsque le message est moins secret que la clé. Cela empêche par exemple le cas où Alice chiffrerait une donnée connue que par Alice et Bob avec une clé connue de Charlie, sinon Charlie pourrait déchiffrer ces données confidentielles et apprendre des choses qu'il n'est pas censé savoir. Cet argument est utilisé plusieurs fois dans la preuve de sécurité de MiniTLS (§2.2).

Toutes ces règles de discipline que les participants honnêtes doivent respecter sont encodées dans un prédicat dit de validité, et on impose aux participants honnêtes de n'envoyer sur le réseau que des messages publics et valides. En contrepartie, lorsque un participant reçoit un message sur le réseau, ce dernier sait que ce message est valide et est publique.

**Validité des suites d'octets.** Le prédicat de validité est au cœur des preuves de sécurité en DY\*. Il doit prendre en compte les utilisations honnêtes de la cryptographie (comme brièvement décrit ci-dessus), mais aussi les utilisations malhonnêtes. En effet, puisqu'un attaquant peut envoyer des messages sur le réseau, si nous voulons la garantie que les messages reçus sur le réseau sont valides, il faut donc que les messages construits par l'attaquant soient valides.
Voici par exemple la règle de validité dans le cas du chiffrement symétrique :

```h
let is_valid ... (b:bytes): prop =
match b with
...
| SymEnc key msg →
  is_valid key ∧ is_valid msg ∧ ( // key et msg sont récursivement valides
    ((get_label msg) <# (get_label key)) ∨ // cas honnête : msg est moins secret que key
    // cas malhonnête : b est construit par l'attaquant, qui connaît donc key et msg
    ((get_label key) <# public ∧ (get_label msg) <# public)
  )
...
```

Concernant les signatures, il n'y a pas de façon évidente de restreindre leur utilisation de façon générique comme nous le faisons avec les chiffrements. Chaque protocole définit un prédicat de signature, qui doit être vrai pour toutes les suites d'octets signées. Ce prédicat de signature fait partie d'une liste de prédicats globaux, spécifique au protocole. Ces prédicats sont au cœur de la preuve, c'est à partir d'eux que découlent toutes les propriétés de sécurité que l'on peut prouver, comme nous l'avons vu avec MiniTLS (§2.2).

```h
let is_valid (preds:global predicates) (b:bytes): prop =
match b with
...
| Sign sk msg →
  // sign sk msg est valide lorsque
  is_valid sk ∧ is_valid msg ∧ ( // sk et msg sont récursivement valides
    (preds.sign_pred (Vk sk) msg) ∨ // cas honnête : le prédicat est vrai
    // cas malhonnête : b est construit par l'attaquant, qui connaît donc sk et msg
    ((get_label sk) <# public ∧ (get_label msg) <# public)
  )
...
```

Quand une signature est valide, cela permet de savoir que soit la clé privée de signature associée à la clé publique de vérification est connue de l'attaquant, soit le prédicat de signature est vrai sur le message signé.

```h
val verify_lemma:
preds:global predicates →
verification_key:bytes → msg:bytes → signature:bytes →
Lemma
(requires
  // si tous les arguments sont valides
  is_valid preds verification_key ∧ is_valid preds msg ∧ is_valid preds signature ∧
  // et que la signature est valide
  verify verification_key msg signature
)
(ensures
  ( // alors soit elle a été construite par un participant honnête et le prédicat de signature est vrai
    preds.sign_pred verification_key msg
  ) ∨ ( // soit la signature a été construite par l'attaquant
    (get_label msg <# public) ∧
    // (get_signkey_label récupère le label de la clé de signature associée à verification_key)
    (get_signkey_label verification_key) <# public
  )
)
```
)

## 3.3 Modélisation des effets de bord avec un effet de journal

Les protocoles cryptographiques ont besoin de faire des opérations impures : envoi et réception de messages sur le réseau, stockage d'état, génération de données aléatoires.

Cette impureté est encodée dans un journal d'effets de bord, qui grandit au fur et à mesure que les participants du protocole ont des effets de bord. Ainsi, les messages envoyés sur le réseau sont ajoutés au journal, et les messages sont par la suite réceptionnés en regardant parmi les messages envoyés dans le journal. D'une façon similaire, un participant qui veut stocker son état l'ajoute au journal, et pourra par la suite récupérer son état en le cherchant dans le journal. Chaque génération de données aléatoires est ajoutée dans le journal afin de permettre de garantir leur fraîcheur, comme discuté dans la description du constructeur `Rand` du type `bytes` (§3.1).

De la même façon que les protocoles définissent des invariants de signature que les participants honnêtes se doivent de respecter (§3.2), les protocoles peuvent définir des invariants sur le journal. Par exemple on peut imposer un certain prédicat à être vrai sur tous les états que l'on stocke, en contrepartie lorsque l'on récupère un état, on sait que le prédicat est vrai.

Ce journal d'effets de bord est modifié avec une monade d'état monotone encodée comme un effet $F^*$ [29]. Comme le journal ne fait que grandir, si à un instant donné on a la propriété « un certain effet de bord existe dans le journal », alors cette propriété restera vraie lorsque le journal grandira. Cela permet d'utiliser les fonctionnalités de témoin de $F^*$ [1] et de définir des prédicats comme `msg_sent_on_network` (§3.1).

## 3.4 Application au protocole MiniTLS

Nous utilisons $DY^*$ pour prouver la sécurité de MiniTLS (§2.2), et allons présenter une petite partie de la preuve de sécurité, à savoir les garanties qui sont offertes par la signature.

Le message à signer est représenté par le type `respond_handshake_tbs`. Un parser et sérialiseur, prouvés inverses l'un de l'autre, sont automatiquement générés à l'aide de la bibliothèque `Comparse` (§4.3).

```typescript
type respond_handshake_tbs = {
    pk_a: bytes;
    sym_key: bytes;
}
```

// génère le parser et sérialiseur automatiquement avec un métaprogramme de Comparse
%splice (gen_parser ('respond_handshake_tbs'))

Le code de vérification de signature s'écrit alors de la façon suivante :

```pascal
let verifyrespond_handshake (verif_key:bytes) (pk_a:bytes) (sym_key:bytes) (signature:bytes): bool =
let tbs = {
    pk_a = pk_a;
    sym_key = sym_key;
} in
verify verif_key (serialized tbs) signature
```

Nous écrivons ensuite l'invariant de signature : on ne signe que des sérialisations de `respond_handshake_tbs`, de plus son champ `sym_key` n'est connu que des personnes connaissant
la clé privée de déchiffrement associée à pk\_a ainsi que des personnes connaissant la clé privée de signature associée à clé publique de vérification de signature vk.

```h
let sign_pred(vk:bytes) (msg:bytes) =
  match parse msg with
    | None -> ⊥
    | Some tbs -> get_label tbs.sym_key == union (get_sk_label tbs.pk_a) (get_signkey_label vk)
```

On peut alors prouver un lemme de sécurité donnant les garanties de la vérification de signature : si la signature est bien authentique et provient de Bob, et que toutes les suites d'octets que l'on considère vérifient les invariants des messages qui passent sur le réseau (§3.2), alors on peut en déduire le label de sym\_key.

```h
val verifyrespond_handshake lemma:
  a:identity -> b:identity ->
  verif_key:bytes -> pk_a:bytes -> sym_key:bytes -> signature:bytes ->
  Lemma
  (requires
    verifyrespond_handshake verif_key pk_a sym_key signature ∧ // la signature est authentique
    // verif_key provient de Bob et toutes les suites d'octets obéissent aux invariants du réseau (§3.2)
    get_signkey_label verif_key == readers [b] ∧ is_valid preds verif_key ∧
    is_valid preds pk_a ∧ is_valid preds sym_key ∧ is_valid preds signature
  )
  // alors on en déduit le label de sym_key
  (ensures get_label sym_key == union (get_sk_label pk_a) (readers [b]))
```

En combinant de tels lemmes de sécurité pour toutes les sous-fonctions du protocole, et en modélisant l'exécution complète du protocole avec ses effets de bord (§3.3), nous obtenons une preuve de sécurité pour MiniTLS avec DY*.

# 4 Techniques de preuve modulaires pour DY*

Maintenant que nous avons vu les outils fournis par DY* pour exprimer des théorèmes de sécurité sur un protocole cryptographique, nous pouvons nous intéresser à la façon précise dont nous allons spécifier le protocole, énoncer le théorème, et effectuer les preuves. Pour cela, il y a de multiples choix techniques à effectuer, et chacun de ces choix aura un impact sur la façon dont seront structurées les preuves. L'ensemble de ces choix techniques constitue donc une méthode qui permet de s'attaquer à la preuve de sécurité d'un protocole. Même si n'importe quelle méthode permet de prouver des petits protocoles avec suffisamment de travail, il convient d'adopter une méthode adéquate afin de s'attaquer à un protocole conséquent comme MLS.

## 4.1 Idiomes utilisés dans les exemples DY*

Les exemples fournis avec DY* ont tous une façon idiomatique d'être définis, qui fonctionne bien sur des protocoles de taille similaire à MiniTLS, et que nous documentons dans cette section. Il nous était difficile d'envisager d'utiliser ces idiomes pour un protocole aussi gros et complexe que MLS, nous présenterons alors d'autres techniques que nous avons utilisées pour prouver TreeSync (§5), un sous-protocole de MLS dédié à l'authentification.

**Exécution symbolique et exécution concrète.** DY* est une bibliothèque de cryptographie symbolique pour faire des preuves de sécurité, qui n'a donc pas vocation à s'exécuter sur des
suites d'octets concrètes. Cependant elle supporte l'exécution concrète des fonctions cryptographiques d'une façon détournée : la définition du type des suites d'octets et l'implémentation des opérations dessus sont cachées derrière un fichier interface, ce qui fait qu'on peut choisir, à la compilation, d'utiliser une implémentation symbolique des suites d'octets, ou d'utiliser une implémentation concrète qui encapsule HACL* [39], une bibliothèque d'impléments de primitives cryptographiques vérifiées avec F*. Cette façon de faire implique que ce choix entre exécution concrète et symbolique se fait à la compilation, et implique que les théorèmes vrais seulement dans le monde symbolique (par exemple l'injectivité des fonctions de hachage) doivent être admis dans le cas concret. De plus, nous n'avons pas le choix sur les primitives cryptographiques choisies. Nous résolvons ce problème en utilisant des classes de types (§4.2), que nous instancions séparément avec DY* comme bibliothèque de cryptographie symbolique et HACL* comme bibliothèque de cryptographie concrète.

**Parseurs et sérialiseurs pour les messages et l'état.** Les messages envoyés sur le réseau ainsi que l'état stocké ont le type *bytes*, une première étape consiste donc à définir des convertisseurs entre *bytes* et des types plus haut niveau, communément appelés parseurs et sérialiseurs. Les parseurs et sérialiseurs sont écrits à la main, avec des preuves manuelles d'inversion (e.g., sérialiser puis parser donne l'objet de départ). Ceci est possible parce qu'il y a peu de structures en jeu (en général, un type pour le message et un type pour l'état), et parce que le protocole est un modèle qui n'a pas vocation à être interopérable : le format des messages peut être choisi de façon à simplifier les preuves. La spécification du protocole MLS [6] possède plus de cinquante structures binaires, qui doivent toutes être parsés et sérialisés d'une façon précise. Nous résolvons ce problème en développant une nouvelle bibliothèque de parseurs et sérialiseurs binaires vérifiés en F*, appelé Compare (§4.3).

**Style intrinsèque.** Afin de respecter la discipline que les participants honnêtes doivent suivre (§3.2), une interface à la bibliothèque cryptographique raffinée est mise à disposition par DY*. Dans cette interface, avant de chiffrer un message avec une clé symétrique, il faut prouver que le message est moins secret que la clé. Ou encore, avant d'effectuer une signature, il faut prouver que l'invariant de signature est vrai sur le contenu signé. Cela a pour conséquence que la définition du protocole est mélangée avec les preuves de sécurité, ce qui pose plusieurs problèmes : cela rend la définition du protocole moins lisible (et donc auditable) ; ces obligations de preuve n'ont pas lieu d'être dans une exécution concrète du protocole ; et cela fait que toutes les preuves de sécurité d'une fonction doivent être faites simultanément. Nous utilisons un style extrinsèque qui consiste à totalement séparer code et preuves, ce qui permet de mieux modulariser les preuves et garder une définition du protocole lisible et indépendante des preuves (§4.4).

**Des prédicats de sécurité globaux.** Les différents prédicats de sécurité décrivant les invariants, comme le prédicat de signature (§3.2) ou les prédicats d'état (§3.3), sont définis de façon globale et sont référencés explicitement tout le long de la preuve de sécurité. Cela ne fonctionne pas pour prouver les protocoles de façon modulaire comme nous voulons le faire sur MLS : si un sous-protocole est prouvé en DY* avec ses prédicats définis de façon globale, et que par la suite nous voulons prouver un nouveau sous-protocole qui s'exécutera en parallèle, dans ce cas il faudrait modifier les prédicats globaux, ce qui risquerait certainement de casser les preuves du premier sous-protocole. Nous résolvons ce problème en définissant des prédicats globaux à partir de multiples prédicats locaux (§4.5).
## 4.2 Classes de types pour les suites d'octets

**Exécution concrète et symbolique.** Nous paramétrons le protocole par une classe de type sur les suites d'octets, d'une façon similaire à ce qu'on pourrait faire avec une **Section** en Coq, ou un foncteur en OCaml. Cette classe de type est construite en deux étages. Une première classe de type `bytes_like` permet de faire des opérations non-cryptographiques sur les suites d'octets, comme la concatenation ou le calcul de longueur. Une seconde classe de type `crypto`, dépendant d'une instance de `bytes_like` permet d'effectuer des opérations cryptographiques sur les suites d'octets.

**Conséquences techniques.** D'une part, à partir d'une unique description du protocole, l'instance de la classe de type permet de choisir entre exécution concrète (pour réellement exécuter le protocole) et exécution symbolique (pour faire des preuves de sécurité), d'autre part, plusieurs instances concrètes permettent de choisir les primitives cryptographiques utilisées par le protocole. De plus, les preuves de sécurité se font sur l'instance symbolique de la classe de type, on peut donc utiliser des propriétés vraies seulement dans les preuves symboliques, comme l'injectivité des fonctions de hachages, sans avoir à les admettre sur les instances concrètes.

**Importance de l'exécution concrète.** Pouvoir exécuter l'instance concrète du protocole permet de tester que la spécification du protocole est opérable avec d'autres implémen-tations, et ainsi s'assurer que les preuves sont faites sur la spécification précise du protocole, jusqu'à la façon dont les données haut-niveau sont sérialisées en suites d'octets, et pas seule-ment sur un modèle approximatif. Ainsi les théorèmes de sécurité ne sont pas déconnectés de la réalité : l'intéropérabilité de la spécification du protocole renforce la confiance dans le fait que celle-ci est une implémentation correcte du standard étudié. Cette façon de faire a par exemple permis de trouver l'attaque exploitant l'ambiguité des signatures dans MLS (§5), qui ne peut se trouver en faisant la preuve que lorsque celle-ci raisonne sur la façon dont les contenus des différentes signatures sont sérialisés en suites d'octets.

## 4.3 Compare : bibliothèque pour parseurs et sérialiseurs vérifiés

Nous avons développé une nouvelle bibliothèque appelée « Compare » qui permet d'obtenir des parseurs et sérialiseurs binaires vérifiés, interopérables, adaptés à la preuve symbolique, le tout de façon automatique.

**Fonctionnalités de Compare.** Les parseurs et sérialiseurs produits par Compare sont prouvés inverses l'un de l'autre. Compare fournit des parseurs et sérialiseurs pour des types de base, et un métaprogramme écrit en Meta-F* [24] permet de générer des parseurs et sérialiseurs pour des types algébriques à partir de leur définition, lorsqu'ils sont construits à partir de types déjà connus de Compare. De plus, des annotations permettent de contrôler la façon dont le type est sérialisé afin d'être conforme à un format binaire précis. Nous arrivons ainsi à définir automatiquement des parseurs et sérialiseurs vérifiés pour de nombreux types, dont les plus de cinquante décrits dans la définition du protocole MLS [6].

**Suites d'octets concrètes et symboliques.** La classe de type `bytes_like` axiomatise de façon minimale les suites d'octets : existence d'une suite d'octets vide, d'une longueur, d'une concatenation, d'une séparation, et de conversions depuis et vers les entiers de taille bornée, ainsi que de lemmes de compatibilité des différentes opérations. Par exemple, on ne suppose pas l'existence de lemme sur l'associativité de la concatenation, ni même de l'unicité de la suite d'octets de taille nulle ! En effet, ces propriétés ne sont pas vérifiées sur les `bytes` symboliques de DY* (§3.1).
**Propriétés de sécurité.** Des théorèmes sur les combinateurs et les types de base permettent de prouver des théorèmes utiles à la preuve symbolique, par exemple si un type algébrique ne contient que des données secrètes pour un label donné, alors sa sérialisation est elle aussi secrète pour ce label, et inversement.

**Fonctionnement interne de Compare.** Les parseurs et sérialiseurs sont générés à l'aide d'un type intermédiaire qui se prête mieux à la composition, sur lequel nous disposons de quelques instances pour des types de base, ainsi que de quelques combinateurs. Un premier combinateur crée une instance pour une paire dépendante, un second combinateur crée une instance pour un type isomorphe à un autre type qui possède une instance. Ainsi, si un type est isomorphe à un embriquement de paire dépendantes de type de base (ce qui est le cas des types algébriques) alors il est possible de définir un parseur et sérialiseur pour ce type.

## 4.4 Utilisation du style extrinsèque

Dans la preuve de TreeSync, nous séparons la définition du protocole, les preuves de théorèmes vrais quelle que soit l'instance des suites d'octets, les preuves de théorèmes vrais sur l'instance symbolique des suites d'octets, et la gestion de l'état interne du protocole. Ce style a été montré dans la preuve de MiniTLS en DY* (§3.4).

Ce style est plus verbeux, mais a des avantages : la définition du protocole n'est pas entrelacée avec des obligations de preuve ce qui permet de préserver sa lisibilité, de plus les différentes propriétés de sécurité peuvent être prouvées séparément, augmentant ainsi la lisibilité des preuves.

## 4.5 Prédicats globaux à partir de prédicats locaux

**Prédicats globaux dans DY\*.** Nous avons vu (§3.2 et §3.3) que les preuves en DY\* reposent sur des prédicats globaux, par exemple sur les signatures ou sur l'état. Ces prédicats doivent être prouvés lors de la signature ou lorsque l'on met à jour l'état, en contrepartie on obtient que le prédicat est vrai lorsque l'on vérifie une signature ou que l'on récupère l'état. Étudions plus spécifiquement les signatures ; la gestion de l'état possède un problème similaire qui se traite aussi de façon similaire.

Le prédicat de signature est un prédicat sur le message signé, ainsi que la clé publique de vérification de signature utilisée (comme vu dans §3.2). Une difficulté arrive lorsqu'il existe plusieurs types de signatures dans le protocole. Le prédicat de signature doit disposer d'un moyen de différencier les différents types de signatures (comme discuté dans §2.3), que ce soit en raisonnant sur la clé de vérification ou sur le message signé. Le prédicat global de signature doit donc procéder en deux étapes : (1) déduire de la clé de vérification ou du message le type de signature dont il s'agit, (2) appeler le prédicat local correspondant à ce type de signature.

**Stabilité des preuves.** Une preuve de sécurité qui exploite la définition du prédicat global est fragile : si le prédicat global est modifié (par exemple pour inclure un nouveau prédicat local), alors les preuves qui en dépendent risquent de casser. De plus, de multiples prédicats doivent être définis lors d'une preuve avec DY\*, ce qui invite à résoudre ce problème une fois pour toute.

Nous introduisons une façon générique de construire un prédicat global à partir d'une liste de prédicats locaux, dont nous présentons ici une version simplifiée. Par la suite, les preuves de sécurité ne dépendront pas directement du prédicat global (et de la façon dont il a été défini), elles dépendront seulement du fait qu'un quelconque prédicat global contient un certain prédicat local.
**Construction d'un prédicat global.** Étant donné un type de donnée *data*, un type de catégorie *category* et une fonction qui déduit la catégorie associé à une donnée, nous construisons un prédicat global à partir d'une liste de catégories et de prédicats locaux. Ce prédicat global est prouvé correct, c'est-à-dire qu'il est équivalent à chacun des prédicats locaux sur les données ayant la catégorie correspondante.

val data: Type // le type sur lequel nous voulons construire un prédicat

val category: Type // le type décrivant la catégorie à laquelle appartient une donnée

val get_category: data → option category // une fonction de désambiguation

val mk_global_pred: list (category & (data → prop)) → (data → prop)

let global_pred_has_local_pred (global_pred:data → prop) (cat:category) (local_pred: data → prop) =
∀(x: data). get_category x == Some cat =⇒ (global_pred x ⇐⇒ local_pred x)

val mk_global_pred correct:

local:preds list (category & (data → prop)) → cat:category → local pred:(data → prop) →

Lemma

(requires

no_repeats (map fst local:preds) ∧ // les categories sont disjointes

mem (cat, local_pred) local preds // cat and local pred sont dans la liste local preds

)

(ensures global_pred_has_local_pred (mk_global_pred local preds) cat local_pred)

Par la suite, les preuves n'ont pas besoin de savoir comment est construit le prédicat global :
elles peuvent être paramétrées par ce prédicat global et seulement savoir qu'il contient un
prédicat local à l'aide de la propriété global_pred has local_pred. Une fois les preuves faites, on
peut alors modifier le prédicat global sans que les preuves existantes cassent, puisqu'elles ne
dépendent que du fait que le prédicat global contient un prédicat local donné.

5 Impact sur la standardisation du protocole MLS

Nous présentons ici brièvement une version simplifiée du protocole TreeSync et de son théo-
rème de sécurité, ainsi que les améliorations que nous avons apporté à ce protocole. La descrip-
tion complète du protocole TreeSync et de sa preuve font l'objet d'un autre article [38], et la
formalisation complète est disponible sur GitHub [20].

TreeSync et TreeKEM. TreeKEM et TreeSync travaillent sur un même arbre : un arbre binaire complet où les participants sont dans les feuilles (voir Figure 5). Chaque nœud interne contient une paire de clés de chiffrement asymétrique, avec la propriété suivante : la clé privée d'un nœud n'est connue que des participants dans son sous-arbre (propriété assurée par TreeKEM). La clé privée de la racine est alors un secret qui n'est connu que du groupe. Lorsqu'un nouveau participant rejoint le groupe, ce dernier reçoit un arbre rempli de clés publiques, et lorsqu'il chiffre un message pour une de ces clés publiques, s'attend à ce que ce message ne soit déchiffrable seulement par les participants dans le sous-arbre associé. Pour établir cette propriété, et éviter des attaques similaires à celle sur la première version de MiniTLS (§2.2), on peut se reposer sur les garanties d'authenticité offertes par TreeSync.

Théorème de sécurité pour TreeSync. Nous prouvons, à l'aide de DY*, que pour chaque nœud de l'arbre, nous pouvons trouver un participant dans le sous-arbre enraciné en ce nœud (celui qui l'a modifié en dernier) dont la signature authentifie ce sous-arbre tel qu'il était au
<figure><img src="image_96.png" /><figcaption>FIGURE 5 – Un arbre de clés TreeKEM, authentifié par TreeSync, où chaque sous-arbre est entouré de la couleur de la feuille qui l’authentifie. TreeKEM s’assure du fait qu’une clé privée $sk_n$ n’est connue que des feuilles du sous-arbre enraciné en $n$, par exemple $sk_{ab}$ n’est connu que de $a$ et $b$. TreeSync s’assure du fait que chaque sous-arbre est authentifié par une de ses feuilles, par exemple le nœud $ab$ est authentifié par $b$ (en rouge). Une feuille peut authentifier plusieurs sous-arbres en même temps, par exemple $b$ authentifie trois sous-arbres : celui enraciné en $b$, en $ab$ et en $abcd$.</figcaption></figure>

moment de la signature. Cette signature permet entre-autres d'initialiser la propriété de TreeKEM grâce à un invariant de signature. La preuve est complexe pour deux raisons : d'une part, il est possible d'ajouter des participants dans les feuilles d'un sous-arbre sans pour autant ré-authentifier celui-ci, il faut donc retrouver l'arbre tel qu'il était au moment de son authentification ; d'autre part, une seule signature authentifie de multiples sous-arbres (tous ceux dont la racine a été modifiée par le participant) et cette signature reste vérifiable même après que certains de ces sous-arbres ont été modifiés par d'autres personnes.

**Attaque sur les signatures.** Nous avons trouvé une attaque similaire à celle entre MiniTLS en SigneTout (§2.3), dû au fait que TreeSync et TreeDEM utilisent les mêmes clés de signature. Nous avons modifié le protocole MLS pour ajouter un tag de façon systématique dans les signatures, ce qui permet de les distinguer [32].

**Renforcement des invariants.** Les invariants des arbres manipulés dans MLS doivent être vrais lors de la création du groupe et être préservés par toutes les modifications du groupe. Mais ils doivent aussi être vérifiés au moment de rejoindre un groupe, sinon nous ne pouvons pas les utiliser lors des preuves de sécurité. Au cours de notre analyse de TreeSync, nous avons remarqué que les invariants vérifiés au moment de rejoindre un groupe n'étaient pas assez forts pour être préservés par les modifications du groupe. Nous les avons renforcés pour que ce soient de vrais invariants de MLS [35, 36].

**Renforcement du théorème de sécurité.** Le théorème de sécurité de TreeSync tel que décrit au début de cette section n’était initialement pas vrai : le contenu couvert par la signature était légèrement malléable, ce qui aurait rendu le théorème d’authentification plus compliqué à écrire. Nous avons renforcé la signature [37, 33, 34] pour pouvoir obtenir ce théorème de sécurité à la fois puissant et simple à énoncer : la signature des participants couvre exactement tous les sous-arbres modifiés par ce participant, là où auparavant elle ne couvrait qu’une partie de ces sous-arbres qu’il aurait fallu caractériser.
# 6 Travaux connexes

**Analyse de la sécurité de MLS.** J. Alwen et al. [2] étudie la sécurité de TreeKEM du brouillon 7 de MLS contre un adversaire passif. J. Alwen et al. [3] étudie modulairement la sécurité du brouillon 11 de MLS contre un adversaire actif. Ils ne trouvent pas l'attaque exploitant l'ambiguïté des signatures, que nous avons trouvé en faisant les preuves jusqu'aux manipulations de suites d'octets. C. Brzuska et al. [14] analyse les dérivations de clé du brouillon 11 de MLS. C. Cremers et al. [15] étudie la sécurité de MLS dans un contexte multi-groupe.

J. Alwen et al. [4] étudie la sécurité de TreeKEM contre un adversaire interne au groupe, et analyse les signatures du brouillon 11 de MLS. Cependant, ils étudient TreeSync et TreeKEM comme un protocole monolithique.

Tous ces travaux se basent sur des preuves à la main, papier et crayon. Au fur et à mesure que MLS grandit, ces preuves manuelles deviennent complexes, difficiles à vérifier et à maintenir. Nous utilisons des outils de vérification assistée par ordinateur afin de faire des preuves sur une implémentation de MLS operable.

Une analyse de la confidentialité persistante de TreeKEM en Tamarin a été réalisée dans [17], sans considérer la sécurité après compromission ni l'authentification. K. Bhargavan et al. [8] utilise F* pour analyser TreeKEM du brouillon 7 de MLS et trouve une attaque sur l'authentification, mais ne prouve pas l'authentification de façon indépendante.

**Preuve assistée par ordinateur de protocoles cryptographiques.** Certains outils de vérification de protocole se basent sur le modèle symbolique, qui traite la cryptographie de façon abstraite. Certains outils sont automatiques, comme ProVerif [13] et Tamarin [25], d'autres outils se basent sur un assistant de preuve général et permettent des preuves manuelles, comme DY* [9] qui se repose sur F* [31], ou les travaux de L. Paulson [27] qui se reposent sur Isabelle [26]. Des outils comme CryptoVerif [12], EasyCrypt [7], et Squirrel [5], se basent sur le modèle calculatoire, ce qui permet d'avoir une modélisation plus précise de la cryptographie mais permet moins d'automatisation. Les deux types d'outils ont été utilisés pour des protocoles de la vie courante, comme Signal [21, 9] et TLS 1.3 [10, 16].

Finalement, beaucoup de travaux vérifient la correction fonctionnelle d'implémentations de protocoles comme Signal [28], Noise [19], et TLS [11].

# 7 Conclusion

Nous avons produit une spécification formelle et operable de la version actuelle de MLS, ainsi qu'une preuve assistée par ordinateur de la sécurité de son sous-protocole TreeSync à l'aide du cadriciel DY*. Au cours de ce travail nous avons corrigé divers bogues et amélioré la conception de MLS, et nous avons développé de nouveaux outils pour faire des preuves de sécurité avec DY*.

# 8 Remerciements

Je remercie Lucas Franceschino pour ses remarques sur le premier brouillon de cet article, ainsi que (par ordre alphabétique) Adrien Koutsos, Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko, Sylvain Wallez, et les rapporteurs anonymes pour leur relecture de cet article et leurs nombreuses suggestions.
Références

[1] Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. Recalling a witness : foundations and applications of monotonic state. *Proc. ACM Program. Lang., 2*(POPL) :65 :1–65 :30, 2018.

[2] Joël Alwen, Sandro Coretti, Yevgeniy Dodis, and Yiannis Tselekounis. Security analysis and improvements for the IETF MLS standard for group messaging. In *CRYPTO*, volume 12170 of *Lecture Notes in Computer Science*, pages 248–277. Springer, 2020.

[3] Joël Alwen, Sandro Coretti, Yevgeniy Dodis, and Yiannis Tselekounis. Modular design of secure group messaging protocols and the security of MLS. In *ACM SIGSAC Conference on Computer and Communications Security (CCS)*, pages 1463–1483, 2021.

[4] Joël Alwen, Daniel Jost, and Marta Mularczyk. On the insider security of MLS. Cryptology ePrint Archive, Paper 2020/1327, 2020.

[5] David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, and Solène Moreau. An interactive prover for protocol verification in the computational model. In *IEEE Symposium on Security and Privacy (S&P)*, pages 537–554. IEEE, 2021.

[6] R. Barnes, J. Millican B. Beurdouche, R. Robert, E. Omara, and K. Cohn-Gordon. The messaging layer security protocol. IETF Internet Draft, September 2022. version 16.

[7] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Phillip Rogaway, editor, *Advances in Cryptology – CRYPTO*, pages 71–90, 2011.

[8] Karthikeyan Bhargavan, Benjamin Beurdouche, and Prasad Naldurg. Formal Models and Verified Protocols for Group Messaging : Attacks and Proofs for IETF MLS. Research report, Inria Paris, December 2019.

[9] Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele. DY* : A modular symbolic verification framework for executable cryptographic protocol code. In *IEEE European Symposium on Security and Privacy (EuroS&P)*, pages 523–542. IEEE, 2021.

[10] Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. In *IEEE Symposium on Security and Privacy (S&P)*, pages 483–502. IEEE, 2017.

[11] Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. Implementing TLS with verified cryptographic security. In *IEEE Symposium on Security and Privacy, (S&P)*, pages 445–459, 2013.

[12] Bruno Blanchet. CryptoVerif : Computationally sound mechanized prover for cryptographic protocols. In *Dagstuhl seminar “Formal Protocol Verification Applied”, volume 117*, page 156, 2007.

[13] Bruno Blanchet et al. Modeling and verifying security protocols with the applied pi calculus and ProVerif. *Foundations and Trends in Privacy and Security*, 1(1-2) :1–135, 2016.

[14] Chris Brzuska, Eric Cornelissen, and Konrad Kohbrok. Security analysis of the MLS key derivation. In *IEEE Symposium on Security and Privacy (S&P)*, pages 2535–2553. IEEE, 2022.

[15] Cas Cremers, Britta Hale, and Konrad Kohbrok. The complexities of healing in secure group messaging : Why cross-group effects matter. In *USENIX Security Symposium*, pages 1847–1864. USENIX Association, 2021.

[16] Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. A comprehensive symbolic analysis of TLS 1.3. In *ACM SIGSAC Conference on Computer and Communications Security (CCS)*, page 1773–1788, 2017.

[17] Cas Cremers, Charlie Jacomme, and Philip Lukert. Subterm-based proof techniques for improving the automation and scope of security protocol analysis. Cryptology ePrint Archive, Paper 2022/1130, 2022. https://eprint.iacr.org/2022/1130.

[18] Danny Dolev and Andrew Yao. On the security of public key protocols. *IEEE Transactions on*