# SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F

Cezar-Constantin Andrici, Danel Ahman, Cătălin Hriţcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter

## ► To cite this version:

Cezar-Constantin Andrici, Danel Ahman, Cătălin Hriţcu, Ruxandra Icleanu, Guido Martínez, et al. *SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F*. Proceedings of the ACM on Programming Languages, 2025, 9 (ICFP), pp.510-540. 10.1145/3747522. hal-05451025

HAL Id: hal-05451025

https://hal.science/hal-05451025v1

Submitted on 9 Jan 2026

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
SecRef*: Securely Sharing Mutable References between
Verified and Unverified Code in F*

CEZAR-CONSTANTIN ANDRICI, MPI-SP, Germany

DANEL AHMAN, University of Tartu, Estonia

CĂTĂLIN HRIȚCU, MPI-SP, Germany

RUXANDRA ICLEANU, University of Edinburgh, UK

GUIDO MARTÍNEZ, Microsoft Research, USA

EXEQUIEL RIVAS, Tallinn University of Technology, Estonia

THÉO WINTERHALTER, Inria Saclay, France

We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style mutable references. To ease program verification in this setting, we track which references are shareable with the unverified code, and which ones are not shareable and whose contents are thus guaranteed to be unchanged after calling into unverified code. This universal property of non-shareable references is exposed in the interface on which the verified program can rely when calling into unverified code. The remaining refinement types and pre- and post-conditions that the verified code expects from the unverified code are converted into dynamic checks about the shared references by using higher-order contracts. We prove formally in F* that this strategy ensures sound and secure interoperability with unverified code. Since SecRef* is built on top of the Monotonic State effect of F*, these proofs rely on the first monadic representation for this effect, which is a contribution of our work that can be of independent interest. Finally, we use SecRef* to build a simple cooperative multi-threading scheduler that is verified and that securely interacts with unverified threads.

CCS Concepts: • Software and its engineering → Software verification; Compilers.

Additional Key Words and Phrases: secure compilation, formal verification, proof assistants, monotonic state

# 1 INTRODUCTION

Verifying stateful programs using proof-oriented languages like Rocq, Lean, Isabelle/HOL, Dafny, and F* is being applied to increasingly realistic projects [6, 8, 9, 11, 22, 23, 27, 30, 33, 38, 46, 61]. In such projects, one notices that verified code calls into, or is called by, unverified code. These calls are necessary to integrate verified code with existing systems, but usually they have an assumed specification, making them a potential source of unsoundness and security vulnerabilities, since the unverified code can inadvertently or maliciously break the internal invariants of the verified code.

While this is a general problem in any proof-oriented language, in this work we work with F*
and represent stateful programs using a monadic effect called Monotonic State [3], instantiated to
obtain first-order ML-style mutable references, which are dynamically allocated and unforgeable,
which cannot be deallocated, and whose type cannot be changed. Monotonic State has facilitated the
verification of large projects that were later integrated into Firefox, Linux, and Windows [45, 55, 62],
yet it offers no guarantees that linking a verified program with unverified code is sound or secure.

Authors' addresses: Cezar-Constantin Andrici, MPI-SP, Bochum, Germany, cezar.andrici@mpi-sp.org; Danel Ahman, University of Tartu, Estonia, danel.ahman@ut.ee; Cătălin Hrițcu, MPI-SP, Bochum, Germany, catalin.hritcu@mpi-sp.org; Ruxandra Icleanu, University of Edinburgh, UK, r.icleanu@gmail.com; Guido Martínez, Microsoft Research, Redmond, WA, USA, guimartinez@microsoft.com; Exequiel Rivas, Tallinn University of Technology, Estonia, exequiel.rivas@ttu.ee; Théo Winterhalter, Inria Saclay, France, theo.winterhalter@inria.fr.

<figure><img src="image_2.png" /></figure>
The most challenging scenario for ensuring soundness involves dynamic sharing of dynamically
allocated mutable references with unverified code. This is so because sharing a reference is a
transitive property: the contents of the reference also gets shared, including any references reachable
from it. Sharing is also permanent: once shared, a reference is shared forever as it can be stashed
away by unverified code, and writes to a shared reference make the newly written values shared as
well. It is thus challenging to track which references are shared and which ones are not, so that
one could still apply static verification. Let's look at a simple example that illustrates these points:

1 let prog (lib : (ref (ref int) → cb:(unit → unit))) =

2 let secret : ref int = alloc 42 in

3 let r : ref (ref int) = alloc (alloc 0) in

4 let cb = lib r in

5 r := alloc 1;

6 cb ();

7 assert (!secret == 42)

It consists of a program that takes as argument
an unverified library. The library gets as input
a reference to a reference to an integer, and re-
turns a callback cb to the program. The program
allocates a reference r (line 3) and passes it to the
library (line 4). The library can store r and the
reference r points to, and read and modify them
in later callbacks. Thus, after the first call into the

library (line 4), the program and the library share both r and the reference r points to. Between the initial call into the library and the call into the callback cb (line 6), the program modifies r pointing it to a newly allocated reference (line 5), and thus this new reference also becomes shared, even if not passed to cb directly—the sharing happens by updating an already shared reference. So in this example, a total of three references allocated by the program are shared with the library, even if only one reference was explicitly passed. Here is an adversarial library that writes to all shared references every time the callback is invoked:

let lib r = let g : ref (list (ref int)) = alloc [] in

(λ () → g := !r :: !g; (** saves where r points to each time the callback is called **)

iter (λ r' → r' := 0) !g; (** writes to all these shared integer references **)

r := alloc 0) (** points r to a new location **)

To be able to verify a stateful program that calls into unverified code, for each such call one has to specify which of the program’s references get modified, also called the footprint of a call. If one cannot determine such a footprint, then in order to ensure soundness, one is forced to conservatively assume that the call can modify *all* references, which makes verification very challenging, because one loses almost all properties of references. For instance, in prog, we would lose that secret equals 42, and we would not be able to prove the assertion on line 7. Yet, as explained above, because references are dynamically allocated, and because of the transitive and persistent nature of their dynamic sharing, it is hard to determine which references are shared and which ones not.

The solution we propose in this paper allows the sound verification of stateful F* programs even if the verified program is linked with unverified code and references are dynamically shared. Our solution builds on the idea that being shareable is a monotonic property of references, meaning that it can be treated as a logical invariant once it is established. Instead of tracking precisely which references cross the verified-unverified boundary, we overapproximate by adding a computationally irrelevant labeling mechanism in which fresh references are labeled as *private*, and that allows the user to dynamically label a reference as *shareable*, which is permanent. Our overapproximation is sound since we statically verify that only references that are labeled as *shareable* can cross into unverified code. In our example, this requires the user to add the following calls to *label_shareable*:

1 let safeula lib =

2 let secret = alloc 42 in

3 let r = alloc (alloc 0) in label_shareable (!r); label_shareable r;

4 let cb = lib r in
5 let v = alloc 1 in label_shareable v; r := v;

6 cb ();

7 assert (!secret == 42)

To correctly overapproximate, we also maintain a global invariant on the heap stating that shareable references always point only to other shareable references—preventing one from accidentally pointing a shareable reference to a not shareable reference (e.g., the original `r:=alloc 1` would not be allowed on line 5 because the fresh reference returned by `alloc 1` is labeled `private`). The labels simplify specifying what the unverified code can do—it can modify only shareable references—which allows preserving the properties of private references (e.g., one is able to prove the assertion on line 7 since `secret` is labeled `private`). Note that we have only one notion of references for which we keep track of how the labels change dynamically.

We have built a secure compilation framework, SecRef*, around the main ideas above and inspired by previous work for the IO effect [4]. Like them, we shallowly embed the source and target language in F*, in our case on top of Labeled References. The only effect our languages have is state, with first-order ML-style mutable references. The difference between the languages is the interface through which the program communicates with the unverified code: a source interface has concrete refinement types and pre- and post-conditions to model verified code, while a target interface has them abstract to model unverified code. Part of SecRef* is dedicated to statically verifying stateful source programs like the one above against rich interfaces assumed about linked unverified target code that include refinement types as well as pre- and post-conditions. These interfaces expose a universal property of unverified code, which cannot modify private references. However, to establish any logical predicates on shareable references, which can cross the verified-unverified boundary, SecRef* adds dynamic checks, using higher-order contracts.

This paper makes the following **contributions**:

* We introduce Labeled References, a computationally irrelevant labeling mechanism built on top of Monotonic State [3] that allows one to verify stateful F* programs that share ML-style mutable references with unverified code. The labeling mechanism tracks which references are shareable with the unverified code and which ones are not. The labels simplify specifying which references can be modified by a call into unverified code—i.e., only shareable references can be modified. Our solution allows one to pass between the verified and the unverified code mutable data structures such as linked lists and callbacks that encapsulate and modify references.

* We build a secure compiler that takes a program verified using Labeled References and protects it so that it can be securely linked with unverified code, which can only modify shareable references. The compiler converts some of the specifications at the boundary between verified and unverified code into dynamic checks by adding higher-order contracts, and we verified in F* the soundness of this enforcement with respect to the specification of the program.

* We also provide a machine-checked proof in F* that a stateful program verified using Labeled References, then compiled with SecRef*, can be securely linked with arbitrary unverified code. For this we prove Robust Relational Hyperproperty Preservation (RrHP), which is the strongest secure compilation criterion of Abate et al. [1], and in particular stronger than full abstraction.

* We give the first monadic representation of Monotonic State by using a free monad, which overcomes a limitation in the original work of Ahman et al. [3]. We also provide a machine-checked soundness proof in F* for Monotonic State differently than the original paper proof of Ahman et al. [3]. While we expect the monadic representation of Monotonic State to be generally useful, even beyond this paper, it is also crucial for our mechanized proofs above.
► Finally, we put our framework into practice by developing a case study inspired by a simple cooperative multi-threading model. In this case study, we showcase that we can statically verify a simple scheduler even when it interacts with and manages unverified threads.

*Outline.* §2 starts with the key ideas of SecRef*. §3 presents our monadic representation and soundness proof for Monotonic State. §4 builds Labeled References on top of Monotonic State. §5 then presents our higher-order contracts. §6 shows how all pieces of SecRef* come together and how we prove that SecRef* satisfies soundness and RrHP. §7 presents the cooperative multi-threading case study. Finally, §8 discusses related work and §9 conclusions and future work. We believe SecRef* is a significant step towards building a secure compiler from F* to OCaml.

## 2 KEY IDEAS OF SECREF*

In this section, §2.1 introduces the running example of an autograder sharing references with unverified code, and showing how to verify it. §2.2 then explains how we represent unverified code and §2.3 how we add higher-order contracts. Lastly, beyond private and shareable, §2.4 introduces a third label, encapsulated, for references that are not shareable with the unverified code, but that can be indirectly updated by verified callbacks that are passed to the unverified code.

1. type linked_list (a:Type) = | LLNil → linked_list a | LLCons : a → ref (linked_list a) → linked_list a
2. type student_hw = ll:ref (linked_list int) → LR (either unit err)
3. (requires (λ h₀ → witnessed (is_shareable ll)))
4. (ensures (λ h₀ r h₁ → modif_only_shareable h₀ h₁ ∧ same labels h₀ h₁ ∧
5. (Inr? r ∨ (sorted ll h₁ ∧ no cycles ll h₁ ∧ same values ll h₀ h₁))))
6. let autograder (test:list int) (hw:student_hw) (grade: mref (option int) grade_preorder)
7. : LR unit (requires (λ h₀ → is_private h₀ grade ∧ None? (sel h₀ grade)))
8. (ensures (λ h₀ () h₁ → Some? (sel h₁ grade) ∧
9. same labels h₀ h₁ ∧ modif_shareable and !{grade} h₀ h₁)) =
10. let ll = create_llist test in
11. label_llist_as_shareable ll; witness (is_shareable ll);
12. let res = hw ll in gr := Some (determineISCO res)

<caption>Fig. 1. The illustrative example of a verified autograder. Types are simplified.</caption>

### 2.1 Static verification using Labeled References

In Figure 1 we show how to use Labeled References to verify an autograder.<fnref n="1" /> The autograder takes as argument a function submitted by a student to solve the homework (hw of type student_hw) and an initially empty (None) reference where the grade will be stored (line 6). The function provided by the student is supposed to sort a linked list in place. The autograder creates a shareable linked list, executes the homework on it, checks the result, and sets the grade (lines 10-12). The main

<footnote n="1">¹F* syntax [4] is similar to OCaml (val, let, match, etc). Binding occurrences b take the form x:t or #x:t for an implicit argument. Lambda abstractions are written λb₁... bₙ → t, whereas b₁ → ... → bₙ → C denotes a curried function type with result C, a computation type describing the effect, result, and specification of the function. Contiguous binders of the same type may be written (v₁... vₙ : t). Refinement types are written b{t} (e.g., x:int{x≥0} represents natural numbers). Dependent pairs are written as x:t₁& t₂. For non-dependent function types, we omit the name in the argument binding, e.g., type #a:Type → (#m #n : nat) → vec a m → vec a n → vec a (m+n) represents the type of the append function on vectors, where both unnamed explicit arguments and the return type depend on the implicit arguments. A type-class constraint {| d : c t₁ .. tn |} is a special kind of implicit argument, solved by a tactic during elaboration. Type₀ is the lowest universe of F*; we also use it to write propositions, including ⊤ (True) and ⊥ (False). We generally omit universe annotations. The type either t₁ t₂ has two constructors, Inl:(#t₁#t₂:Type) → t₁ → either t₁ t₂ and Inr:(#t₁#t₂:Type) → t₂ → either t₁ t₂. Expression Inr? x tests whether x is of the shape Inr y. Binary functions can be made infix by using backticks: x `op` y stands for op x y.</footnote>
property verified for the autograder is that the grade stays private and that it gets set to some value (lines 8-9).

Naturally, the homework is unverified since it is written by a student. Thus, since the autograder
calls the unverified homework, to be able to verify it, one has to assume a specification for the
behavior of the homework. SecRef* then ensures that the homework satisfies the specification.
Soundly specifying the behavior of unverified code is one of the main contributions of this paper, and
we explain this below for student hw (lines 2-5 in Figure 1), illustrating the assumed specification:

(1) The pre-condition requires that the linked list is labeled as shareable, statically guaranteeing that the verified autograder passes only shareable references to the homework (line 3).

(2) The post-condition ensures that only shareable references have been modified, and existing references have the same label (line 4). This is a universal property of all unverified computations, which work only with shareable references (§2.2).

(3) The post-condition also ensures that if the computation succeeds (by returning |n|), the linked list is sorted, without cycles, and contains the same values (line 5). This is the part of the specification that gets enforced dynamically using higher-order contracts (§2.3).

The way we specify the footprint in Figure 1 in the post-condition of the student_HW (item (2) above, line 4) is novel. We specify it as the set of references that are labeled as shareable (using the predicate modif_only_shareable). The usual way of specifying it as the set of references that are in the linked list (i.e., the root reference, the one that follows, and so on to the last reference in the linked list) [3, 30, 49] does not scale in our setting, where we also need to specify higher-order unverified code. Imagine that the unverified function is in fact a result of a bigger piece of unverified code and that another liked list was already shared with it (as in the example from the introduction). This means that the unverified function can also modify that linked list, thus, to soundly specify its behavior one has to add to the footprint the references in that linked list too. Moreover, references that were shared through subsequent updates to the first linked list also have to be added. Using our labeling mechanism tames the complexity of globally tracking the shared references and allows stating the footprint in a simple way.

The assumption that unverified code modifies only shareable references is true if (1) the unverified
code cannot forge references (which we assume), (2) we treat the references allocated by the
unverified code as shareable references (which we do and explain in §2.2), and (3) the verified code
shares only shareable references with the unverified code. To ensure this last point we added the
pre-condition for calling the unverified code that the passed reference has to be shareable (item (1),
line 3). This pre-condition in combination with a global invariant on the heap enforces that the
explicitly passed reference is shareable, and that all references that are reachable from the reference
are shareable too. The global invariant on the heap ensures that a shareable reference can point
only to other shareable references. This means that the SecRef* user has to manually track only
the label of the root reference of a complex data structure (e.g., the head of a linked list). The global
invariant is necessary to prevent accidental sharing by subsequent writes to shareable references
(e.g., the example from the introduction). The user never has to prove directly the preservation of
the global invariant though, because the operations to manipulate references provided by Labeled
References take care of that. The only extra proof burden appears when labeling a reference as
shareable or writing to a shareable reference, one has to prove some conditions ensuring that the
affected reference will point only to shareable references after the operation.

The witnessed token used in the pre-condition (line 3) is produced by the witness operation
of Monotonic State, which provides two such operations: (1) witness, allowing one to convert
stable heap predicates into heap-independent ones, and (2) recall, allowing one to recover an
already witnessed predicate for any future heap. For example, being shareable is a stable property
with respect to our preorder that shareable references stay shareable. Thus if one knows that
a reference *r* is shareable in a heap *h* (i.e., *is_shareable* *r* *h*), one can witness this and get a heap-
independent token witnessed (*is_shareable* *r*), which can be recalled later, say when the heap is *h*',
to prove that *is_shareable* *r* *h*'.<fnref n="2" /> For intuition, making *is_shareable* *r* into a heap-independent token
witnessed (*is_shareable* *r*) can be thought of as defining a proposition, which states that there exists
some past heap *h* in which *is_shareable* *r* *h* was true, and as *is_shareable* *r* is stable with respect to
any allowed heap changes, *is_shareable* *r* *h*' is also true in any future heap *h*' from *h*.

To be able to statically verify the specifications of the autograder (lines 7-9) we reiterate that
giving a specification to the unverified function is necessary. Since the autograder calls into
unverified code, it inherits the property that it can modify shareable references, thus, its footprint is
defined as the union of all shareable references and the singleton set of references containing only
the grade (line 9). The autograder's code stores the grade inside a monotonic reference (denoted by
*mref* on line 6), a feature of Monotonic State [3] that allows putting a statically enforced preorder
on the value stored in a reference. For the grade, the preorder ensures that the grade cannot be
modified once it is set. To be able to set the grade (on line 12), however, one has to know that the
grade was not set by calling into the homework, which we know because the footprint of the call
states that it modifies only shareable references, and we know that the grade was private before
the call. The preorder on the grade is defined as follows:

let grade_preorder (g₀ g₁:option int):Type₀=match g₀ with |None→ T |Some v₀→ Some? g₁ ∧ v₀=Some?.v g₁

In SecRef*, one cannot share a monotonic reference with the unverified code because there
would be no way to guarantee the preorder of the reference, but the verified code can use monotonic
references. One can share only normal references, denoted by *ref*, as long as they are labeled as
shareable. Normal references are just monotonic references with the trivial preorder.

## 2.2 Representation for unverified code

We give a representation for unverified code as a shallow embedding in F\* satisfying two constraints: first, obviously, it has to be a representation for *unverified code* (i.e., it requires only trivial logical reasoning), and second, we need to be able to show that any piece of unverified code using this representation satisfies the universal property that it modifies only shareable references.

We found a representation that satisfies both these constraints and that is also unaware of the
labeling mechanism, by using the effect *MST*. The representation uses abstract predicates as well as
a version of the reference-manipulating operations that mention only these abstract predicates
in their specifications. The intuition why this is an appropriate representation for *unverified code*
in F\* is that one can sequence the new operations freely, because the operations require and
ensure only the abstract predicates, so one only has to carry the abstract predicates around from
post-conditions to pre-conditions, but one never has to do nontrivial logical reasoning. To make it
even more apparent that it is an appropriate representation, in the artifact we also have a syntactic
representation, a small deeply embedded λ-calculus with first-order ML-style references, and we
show a total (back)translation function in F\* from any well-typed syntactic λ-calculus expression
to the shallowly embedded representation with abstract predicates.

The type of the new reference-manipulating operations is presented in Figure 2. They use three
abstract predicates in a way that allows the operations to still be freely sequenced: (1) a global
invariant on the heap (*I*), required and guaranteed by all operations; (2) a predicate on references (*φ*)
constraining references stored in the heap by write and *alloc*, ensured of freshly allocated references
using *alloc*, and ensured of references returned from the heap by read; (3) a preorder on heaps (aby)
and a guarantee that for all our operations the heap evolves according to this preorder. In Figure 2

<footnote n="2">²For readers familiar with Separation Logic, this is similar to invariants and their introduction and elimination rules.</footnote>
Now time for some magic: we show that we can instantiate the polymorphic interface we give to unverified code, so that this code gets closer to something that can be safely linked with verified code. We illustrate this instantiation step by step for `polyoca student_hw` above. Instantiating the abstract invariant, *I*, lifts all the functions to the effect *LR*, which is just a synonym for the effect *MST* with an extra global invariant, ensuring that shareable points to shareable, so after instantiation we have the same effect as in the type `student_hw` from Figure 1. We instantiate $\varphi$ with $\lambda r \rightarrow$ witnessed (is_shareable $r$), which becomes the same pre-condition as in type `student_hw`. Then, we instantiate the preorder $\ll$, with $\lambda h_0 h_1 \rightarrow$ `modif_only_shareable h_0 h_1 \land same labels h_0 h_1`, which means we now have as post-condition the universal property that unverified code modifies only shareable references, which is also the first part of the post-condition of `student_hw`. So unverified code is instantiated during linking to obtain a type with concrete pre- and post-conditions, now having what we call an *intermediate interface*. This is a first step towards bridging the gap between verified and unverified code (see Figure 3), and in §2.3 we show how we additionally use higher-order contracts during the compilation of the verified program to fully bridge this gap.

But first, let us still mention that instantiating the three operations from Figure 2 is straightforward. We instantiate allocation by allocating a reference and then labeling it as shareable. And we instantiate read and write using the default operations of Labeled References, which because of the specs given by the three concrete predicates, they are now specialized for shareable references. For read an interesting interaction happens between every $mref$ $\varphi r$ and the global invariant to show that whatever was read from the heap is also shareable. The every $mref$ combinator stops when reaching any reference because once it was established that a reference is shareable, the global invariant offers the guarantee that all references reachable from this reference are also shareable.

<figure><img src="image_3.png" /><figcaption>Fig. 3. An overview of SecRef\*.</figcaption></figure>

## 2.3 Higher-order contracts in SecRef\*

After the instantiation, an unverified computation of type `unverifiedeca student_hw` almost has the type, which we call a *strong interface*, `student_hw`. The only missing piece is a part of the post-condition (item 3 in §2.1), which states that after the homework returns, if the run was successful, then the linked list is sorted, has no cycles and contains the same values as before. This part is enforced by SecRef\* using higher-order contracts [15], which are used to enforce only properties of shareable references or values passed when unverified code gives control to the verified code. Since the verified code has no insights into what the unverified code does with the shareable references and with which values it gives them, no logical predicates can be established about them. Therefore, it is the choice of the user if they want to strengthen the types and use higher-order contracts, or if they want to manually establish the logical predicates by adding dynamic checks. The advantage of strengthening the specification is that if one would instead link with some verified program, then there would be no need for the dynamic checks, and for unverified code, one would use SecRef\*.

We implement the idea of Stateful Contracts [15] using wrapping and by implementing two dual functions `export` and `import`: `export` takes existing specs and converts them into dynamic checks (e.g., converts pre-conditions of arrows and refinements on the arguments to dynamic checks), while `import` adds dynamic checks to have more specs (e.g., adds dynamic checks to strengthen the post-conditions of arrows and to add refinements on the result). The functions `export` and `import` are defined in terms of each other to support higher-order functions. In SecRef\*, when the verified
program has initial control, the import function is used during both compilation and back-translation (the dual of compilation, used for the secure compilation proof in §6). During compilation import is used to add dynamic checks to the verified-unverified boundary of the compiled program to protect it. During back-translation import is used to add dynamic checks to the unverified code so that it can be typed as having the necessary specification. In the dual setting, when the unverified code has the initial control, the export function is used.

Our implementation of higher-order contracts is verified not to modify the heap in any way (it only reads from the heap). SecRef* also verifies if the dynamic checks imply the specification that has to be enforced. Since F* specifications are not directly executable, SecRef* leverages type classes to automatically infer the check. If this fails though, the user is asked to manually provide the check and prove that the check implies the specification, which benefits from SMT automation.

## 2.4 Encapsulated references

We want to enable the verified program to mutate private references inside the callbacks it passes to the unverified code. Such references are not shared with the unverified code, but are modified indirectly by the callback calls the unverified code makes. To enable this use case, we introduce a third label, encapsulated. Only references labeled as private can become encapsulated, and they remain encapsulated forever. Since encapsulated references are used only in verified code, there is no need to add a constraint that limits to which kind of references they point.

Encapsulated references are only directly modified by the verified program, but an unknown number of times, since the unverified code can call back as many times as it likes. The callback can also be called at later times, since it can be stashed away. The advantage of encapsulated references is that one knows how they get modified, thus, one can encapsulate monotonic references to take advantage of a preorder, and/or use refinement types and/or dependent types for the value stored.

Encapsulated references are especially useful when the unverified code has initial control. The unverified code can call multiple times the verified program, but in a first-order setting the calls are independent, and any reference allocated by the program gets lost when it gives control back to the unverified code. If the program is higher-order though, it can have callbacks with persistent state by using encapsulated references. We illustrate this case in Figure 4 using the example of a pseudo-number generator that has an initialization phase where it gets a seed as an argument and returns a callback that generates a number on each call. To generate a new number for every call to the callback, the program allocates an encapsulated reference, counter, with which it keeps track of how many times it has been called. This is a monotonic reference with the preorder that it can only increase. Since the generator does not make any assumption about the unverified code (the pre-conditions are trivial), SecRef* does not add any dynamic checks during compilation.

1. `val generate_nr: int → int → int` (* a pure computation *)

2. `let post = λh₀ _ h₁ → modif_shareable_and_encaps h₀ h₁ ∧ same labels h₀ h₁`

3. `let prng (seed:int)`

4. `: LR (unit → LR int (requires (λ_ → T)) (ensures post)) (requires (λ_ → T)) (ensures post) =`

5. `let counter : mref int (≤) = alloc 0 in label_encapsulated counter;`

6. `(` ` counter := !counter + 1; generate_nr seed (!counter))`

<caption>Fig. 4. The illustrative example of a pseudo-number generator</caption>

This last example also reveals that the presentation in Figure 1 and §2.2 is simplified to improve readability, and in fact, SecRef* uses the more general predicate `modif_shareable_and_encaps` (instead of the more specific `modif_only_shareable`) as a post-condition for unverified code.
# 3 MONOTONIC STATE REPRESENTED USING A DIJKSTRA MONAD

We first introduce the Monotonic State monadic effect MST on which Labeled References builds. We present the interface of Monotonic State as in the original work of Ahman et al. [3], after which we present our contribution involving defining MST as a Dijkstra monad with a free-monad-based representation (§3.2), and finally we present a mechanized soundness proof for MST (§3.3).

## 3.1 The interface of Monotonic State

Monotonic State is an $F^*$ effect characterizing stateful computations whose state evolves according to a given preorder, with additional features to make specifying and verifying such computations more convenient. In particular, given some predicate on states that is stable for any state changes respecting the preorder, one can witness that the predicate $p$ holds in one part of a program, resulting in a state-independent token witnessed $p$ witnessing this action, and then use this token to recall that the predicate $p$ still holds at arbitrary later program points and in later states.

Ahman et al. [3] considered a general notion of Monotonic State, in which the effect is param- eterized by an arbitrary type of states and a preorder on them. In this paper, we pick as states monotonic heaps (type heap) provided by $F^*$, with the preorder $\le$ on heaps enforcing that allocated references stay allocated forever, and monotonic references preserve their preorders. With this, we obtain our MST effect, which models first-order$^4$ ML-style mutable references.

The interface of MST, presented in Figure 5, hides the concrete representation of the heap and references, and the implementation of the operations that manipulate them. The interface provides proof that the operations preserve the preorder through a series of lemmas (which we elide).

The basic reference type is that of monotonic references, `mref` a rel, which have individual pre- orders enforced by the preorder on the heaps $\le$. ML-style references `ref a` are a special case for the total preorder that relates all the $a$-values. Behind the interface, the references have concrete addresses which are hidden from the user to ensure their unforgeability. For reasoning, however, the interface exposes a function `addr_of` that returns an erased, computationally irrelevant value that can only be used in specifications, but not branched on in programs, ensuring the abstraction boundary is respected. Labeled References uses `addr_of` in the encoding of the labeling mechanism.

The MST effect comes with operations for reading from, writing to, and allocating fresh references. The pre-condition of write requires the new value to be related to the value of the reference in the current heap. This ensures that the reference evolves according to the preorder of the reference. The write and alloc operations both contain a modifies clause in their post-conditions, which is the usual way of specifying that only specific references are allowed to be modified (the footprint of the call). Specifically, for a set $s$ of addresses, modifies $s h_0 h_1$ holds if any references contained in $h_0$ and not contained in $s$ remain unmodified. Above, $!{r}$ is $F^*$'s syntax for the singleton set containing the address of $r$. Notice that the pre-conditions of read and write require the reference to be contained, yet for simplicity, we often elide this detail from the other sections of the paper.

For users of MST, it is important to note that both the original work of Ahman et al. [3] and our work on MST rely for their soundness on the logical witnessed tokens being abstract, unforgeable, and only constructible using the witness operation of the MST effect. Therefore, one must avoid using strong abstraction and parametricity breaking classical axioms in code written using the MST effect, such as the axiom of strong excluded middle that equates `prop` and `bool` and allows one to test the validity of arbitrary propositions, because that leads to an inconsistency in $F^*$.<fnref n="5" /> Avoiding

<footnote n="4">⁴Providing a monadic representation that allows storing effectful functions given $F^*$'s predictive, countable hierarchy of universes is an open research problem, further detailed in §3.2 and §9.</footnote>

<footnote n="5">⁵Monotonic State is Incompatible with Strong Excluded Middle: https://github.com/FStarLang/FStar/issues/2814</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 5. Interface of Monotonic State</figcaption></figure>

such axioms in user code is standard practice in F\*-based projects because of their abstraction- and parametricity-breaking nature. They are typically used very carefully only by library designers.

## 3.2 MST as a Dijkstra monad with a free-monad-based representation

In the work of Ahman et al. [3], the MST effect and the operations discussed above were simply assumed in F\* (using the `assume` keyword) and not given any representation or definitions within F\*. In this paper, we improve on this situation by giving a free-monad-based *representation* for MST in F\*, from which it can be defined as a Dijkstra monad [34]. While the main definition of the MST effect remains axiomatic, via the monad morphism $\theta$ we define below,<fnref n="6" /> the existence of a free-monad-based representation enables us to separately define a computational state-passing semantics for MST computations, and use that semantics to for the first time prove the soundness of the MST effect interface within F\* itself (§3.3), whereas Ahman et al. [3] gave their soundness proof only on paper because there was no representation of MST computations to work with inside F\*.

We recall that a Dijkstra monad is a monad-like structure indexed by specifications, which themselves often come from some monad, called a specification monad. For a Dijkstra monad $\mathcal{D}$, the type $\mathcal{D} \alpha w$ classifies computations that return $\alpha$-typed values and satisfy a specification $w : W \alpha$, where $W$ is an aforementioned specification monad. A common way to define a Dijkstra monad $\mathcal{D}$ [34] is to identify (i) a monad $M$ to represent computations classified by $\mathcal{D}$, (ii) an

<footnote n="6">⁶The axiomatic nature of the effect definition is due to the use of a free monad as its representation, whose elements are inert trees and where no actual computation takes place. As such, the specifications assigned by the monad morphism play the same role as the assumed types of operations in the existing work, but now we also have a representation to work with.</footnote>
ordered monad W that models specifications for the computations in M, where the order formalizes when one specification implies another, and (iii) a monad morphism $\theta: M \to W$ that infers for every computation its “most precise” specification. The Dijkstra monad $\mathcal{D}$ is then defined as $\mathcal{D}\alpha w = m: M\alpha\{\theta(m) \sqsubseteq w\}$, formalizing the idea that $\mathcal{D}\alpha w$ classifies computations $m: M\alpha$ that satisfy the given specification $w$. Below we work out such a Dijkstra monad for MST.

**The computational monad.** We begin by defining the computational monad as a free monad:<fnref n="7" />

```
type mst_repr (a:Type u#a) : Type u#(max 1 a) =
| Return : a -> mst_repr a
| Read : #b:Type0 -> #rel: preorder b -> r: mref b rel -> k:(b -> mst_repr a) -> mst_repr a
| Write : #b:Type0 -> #rel: preorder b -> r: mref b rel -> v:b -> k:mst_repr a -> mst_repr a
| Alloc : #b:Type0 -> #rel: preorder b -> init: b -> k:(mref b rel -> mst_repr a) -> mst_repr a
| Witness : p:stable_heap predicate -> k:(unit -> mst_repr a) -> mst_repr a
| Recall : p:stable_heap predicate -> k:(unit -> mst_repr a) -> mst_repr a
```

As is standard with free monads, elements of mst_repr denote computations modelled as trees whose nodes are operation calls and whose leaves contain return values. Observe that the continuations of Witness and Recall accept simply unit-typed values—at the level of the computational representation no witnessed p tokens are passed to the continuation, they only appear and are passed around in the logical specifications. The return and bind operations of this free monad are standard.

Let us also discuss why we cannot store higher-order effectful functions. Notice that our monad transforms a Type u#a into a Type u#(max 1 a), this is because the operations Read, Write, and Alloc quantify over Type0. Thus, it increases the universe level, which makes functions represented using this monad unstorable in our references. There is no known monadic representation that allows storing effectful functions given $F^*$'s predicative, countable hierarchy of universes. We support references that point to other references but cannot point to effectful functions.

**The specification monad.** we use, mst_w, is the monad of weakest pre-conditions:

```
let mst_w (a:Type) = wp:(post:(a -> heap -> Type0) -> pre:(heap -> Type0))
    {\forall post post'. (\forall v h1. post v h1 =\Rightarrow post' v h1) =\Rightarrow (\forall h0. wp post h0 =\Rightarrow wp post' h0)}
```

A specification is a function that transforms any post-condition over return values and final heaps into a pre-condition over initial heaps. The refinement type restricts us to monotonic predicate transformers. The unit of this monad requires the post-condition to hold of the initial state, as mst_w_return v post h0 = post v h0, and the bind operation composes two predicate transformers, as mst_w_bind wp' post h0 = wp (λv h1→ wp' v post h1) h0. The order $\sqsubseteq$ on mst_w is defined so that wp $\sqsubseteq$ wp' holds when $\forall post\ h0. \ wp'\ post\ h0 =\Rightarrow wp\ post\ h0$.

**The monad morphism and the Dijkstra monad.** As the final ingredient for defining a Dijkstra monad, we define a monad morphism $\theta: mst_repr \alpha \to mst_w \alpha$ by recursion on the tree structure of mst_repr $\alpha$, which assigns weakest-pre-condition-based specifications to MST operations and computations. For illustration, the cases for return, witness, and recall are given as follows.

```
let rec θ m = match m with
| Return v -> mst_w_return v | Read r k -> ... | Write r v k -> ... | Alloc init k -> ...
| Witness p k -> mst_w_bind (λ post h -> p h ∧ (witnessed p =\Rightarrow post () h)) (λ v → θ (k r))
| Recall p k -> mst_w_bind (λ post h -> witnessed p ∧ (p h =\Rightarrow post () h)) (λ v → θ (k r))
```

The unit of mst_repr is mapped to the unit of mst_w, and for the operations the bind of mst_w is used to compose the specificational interpretation of operations with the recursive application of $\theta$ to their continuations. For instance, the mst_w interpretation of Witness matches exactly the

<footnote n="7">⁷We omit a constructor that is needed in $F^*$ to account for partiality coming from pre-conditions [58].</footnote>
specification of witness from §3.1 using the correspondence between pre- and post-conditions and predicate transformers [34]. The same pattern repeats for all the other operations.

The Dijkstra monad is defined by refining `mst_repr` computations using `mst_w` predicates via $\theta$:
$$ \text{type mst\_dm(a:Type)} (\text{wp:mst\_w a}) = \text{m:mst\_repr a}\{\theta \mid m \sqsubseteq wp} $$

*The layered effects.* So far `mst dm` is just an ordinary type in F\*. In order to turn it into the *MST* effect discussed earlier to support direct-style programming (where monadic returns and binds are implicit), we use a mechanism for extending F\* with new effects [47].

effect MSTATE (a:Type) (w:mst_w a) with { repr = mst dm; return = mst dm return; ... }
effect MST (a:Type) (pre:heap → Type₀) (post:heap → a → heap → Type₀) =
MSTATE a (λp h₀ → pre h₀ ∧ (∀v h₁ . h₀ ≤ h₁ ∧ post h₀ v h₁ = ⇒ p v h₁))

The last effect, *MST*, is derived as a pre- and post-condition based effect synonym [34], and is the one we discussed in §3.1. In F\* we mark *MSTATE* (and thus also the derived effects) *total*, *reifiable*, and *reflectable*. Since our monadic representation is based on an inductive type, we indicate to F\* that our effect is total. Totality means that any programs that typecheck against these effects are guaranteed to terminate, and vice versa, any programs we write in these effects have to be proven to terminate. Reification allows us to reveal the underlying free-monad-based representation of these effects in proofs, and reflection allows us to reflect the free monad operation calls to operations in these effects, with the specification of the reflected code determined by $\theta$.

## 3.3 Soundness of the free-monad-based Dijkstra monad for Monotonic State

As noted earlier, in the work of Ahman et al. [3] the *MST* effect interface was simply assumed in F\*, with its computational interpretation defined and the soundness of its axiomatization proved only on paper. Also, the proof of Ahman et al. [3] only applied to a $\lambda$-calculus much less powerful than full F\*. To improve on this, we now use the free-monad-based representation of *MST* to define a computational state-passing semantics for *MST* and use it to give a soundness proof in F\* that the specifications computed with $\theta$ from the free monad representation are computationally satisfied. A soundness proof is desirable because choosing a specification for the free monad operations in $\theta$ is not necessarily the same as being sound with respect to the intended computational behavior.

At the core of our soundness proof is the idea that the witnessed tokens are merely a convenience for communicating logical information from one part of a program to another one, and any program that is provable using witnessed tokens ought to also be provable without them. To be able to vary the relevance of witnessed tokens, we consider a variant of $\theta$, written $\theta_w$, which is parametric in the tokens w: (heap → Type₀) → Type₀ used in the specifications of Witness and Recall, but is otherwise defined like $\theta$. We also define a predicate witnessed_before that captures which stable heap predicates are recalled in a computation, but were not witnessed in the same computation. In particular, when we can prove empty `witnessed_before` m, then any witnessed p token recalled in m:mst_repr $\alpha$ had to originate from an earlier call to witness p in m, which is a property of closed programs.

let rec witnessed_before (preds銷:SET stable_heap predicate) (m:mst_repr $\alpha$) : Type₀ =
match m with
| Return _ → T | Read r k → ... | Write r v k → ...
| Alloc init k → ∀r. preds `witnessed_before` (k r)
| Witness pred k → (union preds (singleton pred)) `witnessed_before` (k())
| Recall pred k → pred `mem` preds ∧ preds `witnessed_before` (k())

We define the state-passing semantics `run_mst` for a closed program m. We refine m as being verified to satisfy a specification `wp`, but we instantiate the w parameter of $\theta_w$ with the trivial tokens witnessed_trivial p = T, modelling that witnessing and recalling are computationally irrelevant. Using
refinement types, we require that the weakest pre-condition `wp` post holds of the initial heap, and we ensure that the post-condition post holds of the return value and the final heap. During the recursive traversal of `m`, the heap is augmented with a set of predicates witnessed during execution and with a refinement type ensuring that these predicates hold for the given heap. The refinement holds as the heap evolves, since the operations that manipulate the heap preserve the preorder which the witnessed predicates are stable for. During the traversal, the refinement with `witnessed_before` ensures that any predicates witnessed are contained in the set of predicates of the augmented heap.

type heap_w preds = h:heap & preds(set stable_heap predicate){ ∀ pred. pred `mem` preds = ⇒ pred h}

let rec run_mst_with preds (wp:state wp α) (m:mst repr α{θwitnessed_trivial m ⊑wp})

(post:(α → heap → Type0)) (hp0:heap w preds{wp post (fst hp0) ∧ (snd hp0) `witnessed_before` m})

: (r:α & hp1:heap w preds{post r (fst hp1)})

= match m with | Return v → (v, hp0) | Read r k → ... | Write r v k → ...

| Alloc #b #rel init k → let (r,h1) = heap_alloc rel (fst hp0) init in

run_mst_with preds (θwitnessed_trivial (k r)) (k r) post (h1,snd hp0)

| Witness p k → let lp = (snd hp0) `union` (singleton p) in

run_mst_with preds (θwitnessed_trivial (k l)) (k l) post (fst hp0, lp)

| Recall p k → run_mst_with preds (θwitnessed_trivial (k k)) (k k) post hp0

let run_mst (wp:state wp α) (m:mst repr α{θwitnessed_trivial m ⊑wp ∧ empty `witnessed_before` m})

(post:(α → heap → Type0)) : h0:heap{wp post h0} → r:α & h1:heap{post r h1}

= λh0 → let (r, hp1) = run_mst_with preds wp m post (h0, empty) in (r, fst hp1)

Using `run_mst`, we define the soundness theorem which states that if a closed program `m` is well-typed against a specification that uses abstract witnessed tokens (modelled using universal quantification), then for any post-condition post and initial heap `h0`, if the weakest pre-condition `wp` post holds in `h0`, the post-condition holds for the return value `v` in the final heap `h1`.

let soundness (m:mst repr α) (wp:state wp α)

: Lemma (requires ((∀ w. θw m ⊑wp) ∧ empty `witnessed_before` m))

(ensures (∀ post h0. wp post h0 = ⇒ (let (v,h1) = run_mst wp m post h0 in post v h1))) = ()

The soundness proof is not completely axiom-free because it relies on a library for the witnessed tokens that is defined in terms of an axiomatic presentation of hybrid modal logic [48] in F\*.

# 4 LABELED REFERENCES

We now explain how we build our reference labeling mechanism on top of Monotonic State.

## 4.1 The labels

As illustrated in §2, in SecRef\* we work with three labels for references:

type label = | Private | Shareable | Encapsulated

When a reference is allocated, it starts labeled with private. The user can then relabel the reference either with shareable or encapsulated. Labeling a reference with shareable or encapsulated is permanent. We ensure this using the following preorder on reference labels:

let ≲lab : preorder label = λl l' → match l , l' with

| Private , _ | Shareable , Shareable | Encapsulated , Encapsulated → T | _ , _ → ⊥

To track references' labels and how they evolve in programs, we assume a ghost top-level monotonic reference<fnref n="8" /> that stores a map from the addresses of references to their labels

<footnote n="8">⁸We prefer to assume the top-level reference to avoid precisely modeling ghost state [14, 24].</footnote>
type label_map_t = erased (mref (pos → erased label) (λ m₀ m₁ → ∀r. (m₀ r) ≤ₗ lab (m₁ r))))

assume val label_map : label_map_t

The heap relation ≤ defined in Figure 5 from §3 ensures that label_map can only evolve according to ≤<sub>lab</sub>, which in turn is what makes being shareable or encapsulated a stable property of references:

let is_shareable : mref_stable_heap predicate = λ#a #rel (r:mref a rel) h →

h `contains` label_map (* necessary to show stability *) ∧ Shareable? ((sel h label_map) (addr_of r))

let is_encaps : mref_stable_heap predicate = λ#a #rel (r:mref a rel) h →

h `contains` label_map (* necessary to show stability *) ∧ Encapsulated? ((sel h label_map) (addr_of r))

where mref_stable_heap predicate is an mref-parameterized stable heap predicate. In contrast, as private references can get relabeled, being private is not a stable property of the heap:

let is_private_addr : pos → heap → Type₀ = λr h → Private? ((sel h label_map) r)

let is_private : mref_heap predicate = λ#a #rel (r:mref a rel) h → is_private_addr (addr_of r) h

We mark the contents of the map and the map itself as erased, to on the one hand ensure that labels can only be used in specifications and programs cannot branch on them, and on the other hand, to avoid passing label_map to computationally relevant operations that expect non-erased arguments. The latter allows label_map to be erased in extracted code (as erased is extracted to unit).

Finally, we find it useful to define variants of the *modifies* clause discussed in §3 to specify that the footprint of a computation modifies only *shareable* or *encapsulated*, or both kinds of references:

let modif_only_shareable_and_encaps (h₀:heap) (h₁:heap) : Type₀ = ∀a rel (r:mref a rel).

¬(eq_addrs r label_map) ∧ ¬(is_shareable r h₀ ∨ is_encaps r h₀)) ⇒ sel h₀ r == sel h₁ r

let modif_shareable_and (h₀:heap) (h₁:heap) (s:sel nat) : Type₀ = ∀a rel (r:mref a rel).

¬(eq_addrs r label_map) ∧ ¬(is_shareable r h₀ ∨ (addr_of r) `mem' s)) ⇒ sel h₀ r == sel h₁ r

## 4.2 The global invariant for shareable references

We introduced our global invariant on the heap, that *shareable references* can only point to *shareable references*, in §2.1. To formally state it in §4.3, we want to quantify over all references of all types that are labeled as *shareable* and check that the stored value contains only *shareable references*. A convenient way to state the invariant is using a deep embedding of the types a *shareable reference* can store values of. These are built from base types, sums, products and references, collectively known in the literature as full ground types [26, 36, 37]. Arrows are not part of the embedding since our heap is only first-order (see §3.2). The embedding is given by:

type full_ground Typ = | SUnit | SInt | SBool

| SSum : full_ground Typ → full_ground Typ → full_ground Typ

| SPair : full_ground Typ → full_ground Typ → full_ground Typ

| SRef : full_ground Typ → full_ground Typ

| SList : full_ground Typ → full_ground Typ

and comes with the evident recursive inclusion to_Type : full_ground Typ → Type₀ into Type₀ types.

To check that a stored value contains only *shareable references*, we use the deep embedding to define a predicate *forall_refs* which checks that every reference in a given value of *full_ground Typ* type satisfies a predicate. We then lift this predicate to properties of references with respect to heaps. As these predicates are parametric in *pred*, we can instantiate them with different predicates.

let recforall_refs (pred:mref predicate) (#t:full_ground Typ) (x:to_Type t) : Type₀ =

let rcall #t x =forall_refs pred #t x in
match t with | SUnit | SInt | SBool → T
| SSum t₁ t₂ → match x with | Inl x' → rcall x' | Inr x' → rcall x'
| SPair t₁ t₂ → rcall x.₁ ∧ rcall x.₂
| SRef t' → pred x
| SList t' → match x with | LLNil → T | LLCons v xsref → rcall v ∧ pred xsref
let `forall Refs_heap` (pred:mref_heap predicate) h x = `forall Refs` (λ r → pred r h) x

Finally, to be able to define the invariant, we transitively close these predicates on a heap:

let trans_forall_refs_heap (h:heap) (pred:mref_stable_heap predicate) =
∀(t:full_groundjin) (r:ref (to_Type t)). h `contains` r ∧ pred r h =⇒ `forall refs heap` pred h (sel h r)

This general version we apply to is_shareable and contains predicates, e.g., so as to specify that every
shareable reference r points to a value (sel h r) that contains only shareable references.

4.3 The LR effect

We define the Labeled References effect LR on top of the Monotonic State effect MST by restricting
MST computations with a global invariant that enforces the correct usage of shareable references
and the ghost state storing reference labels. The invariant is defined as a conjunction of conditions:

let contains_pred #a #rel (r:mref a rel) h = h `contains` r
let lr_inv (h:heap) : Type0 =
  trans_forall_refs_heap h contains_pred ∧ (* contained references point to contained references *)
  trans_forall_refs_heap h is_shareable ∧ (* shareable references point to shareable references *)
  h `contains` label_map ∧ (* the labeling map is contained in the heap *)
  is_private (label_map) h ∧ (* the labeling map remains private *)
  (∀ r. r ≥ next_addr h =⇒ is_private_addr r h) (* all yet to be allocated references are labeled as private *)

The last condition ensures that any freshly allocated reference is private by default and will only
become shareable by explicitly labeling it so, allowing for fine-grained control over which references
can cross the verified-unverified code boundary. This also applies to encapsulated references.

The LR effect is then defined on top of MST by packaging the invariant both into pre- and post-
conditions. By being an effect synonym as opposed to a new effect, we can seamlessly coerce any
MST computation into LR, as long as it satisfies the invariant, something that is very helpful for
linking verified code with unverified code (see §2.2). In detail, LR is defined in F* as follows:

effect LR (a:Type) pre post = MST a (requires (λ h₀ → lr_inv h₀ ∧ pre h₀))
(ensures (λ h₀ r h₁ → lr_inv h₁ ∧ post h₀ r h₁))

By providing the MST operations we discussed in §3 with suitable stronger pre- and post-
conditions, we can lift them to the LR effect. For allocation, the LR operation lr_alloc #a #rel init addi-
tionally requires that if the type a happens to be a full_groundjin, then every reference contained
in the initial value init has to be contained in the heap. In its post-condition, lr_alloc additionally
guarantees that the freshly allocated reference is labeled private and no other references become
shareable during its allocation. Modulo the use of lemmas proving that allocation of references
preserves lr_inv, lr_alloc is defined simply as alloc, with the type

val lr_alloc #a (#rel:preorder a) (init:a) : LR (mref a rel)
(requires (λ h₀ → ∀t. to_Type t == a =⇒ `forall refs_heap contains_pred h₀ #t init`))
(ensures (λ h₀ r h₁ → alloc_post #a #rel init h₀ r h₁ ∧ is_private r h₁ ∧ becomes_shareable !{h₀ h₁})))

The specification of LR's `lr_read` operation remains the same as for MST's read (see Figure 5). For `lr_write` #a #rel r v, we strengthen the pre-condition by additionally requiring that the reference is
different from the ghost state holding the labeling map, and that if a happens to be a full groundrch, then every reference contained in v has to be contained in the heap, and that if r happens to be a shareable reference, then every reference contained in v has to be shareable as well. In return, the post-condition additionally guarantees that no new references become shareable while writing into r. As with lr_alloc, modulo the use of some lemmas, lr_write is defined as write.

val lr_write #a (#rel:preorder a) (r:mref a rel) (v:a) : LR unit
(requires (λ h₀ → write_pre #a #rel r v ∧ ¬(eq_addrs r label_map) ∧
(∀ t. to_Type t == a =⇒forall Refs_heap contains_pred h₀ #t v ∧
(is_shareable r h₀ =⇒forall Refs_heap is_shareable h₀ #t v))))
(ensures (λ h₀ () h₁ → write_post r v h₀ () h₁ ∧ becomes_shareable !{h₀ h₁}))

Similarly to reading from a reference, witnessing and recalling stable predicates also retain the
exact pre- and post-conditions as listed in Figure 5, as they also keep the whole heap unchanged.

In programs and in particular in the examples in the rest of the paper, programmers can use
lr_alloc, lr_read, and lr_write via the usual ML-style syntax, as alloc, !, and := respectively.

In addition to the operations lifted from the MST effect, the LR effect comes with two important additional operations, which allow private references to be relabeled as shareable or encapsulated.

val label_shareable (#t:full_groundrch) (r:ref (to_Type t)) : LR unit
(requires (λ h₀ → h₀ `contains` r ∧ is_private r h₀ ∧ forall Refs_heap is_shareable h₀ (sel h₀ r)))
(ensures (λ h₀ () h₁ → equalisation h₀ h₁ ∧ modifies !{label_map} h₀ h₁ ∧
is_private (label_map) h₁ ∧ becomes_shareable !{sr} h₀ h₁))
val label_encapsulated (#a:Type) (#rel:preorder a) (r:mref a rel) : LR unit
(requires (λ h₀ → h₀ `contains` r ∧ is_private r h₀ ∧ ¬(eq_addrs r label_map)))
(ensures (λ h₀ () h₁ → equalisation h₀ h₁ ∧ modifies !{label_map} h₀ h₁ ∧
is_private (label_map) h₁ ∧ becomes_encapsulated !{r} h₀ h₁))

Both operations can be called with private references contained in the heap, with label_shareable requiring that the reference r has to store full Exhibits (this helps to prove that label_shareable preserves the global invariant, as noted in §4.2), that r has a trivial preorder (via the type ref of non-monotonic references, see Figure 5), and that any references r points to have already been labeled as shareable. This last point means that when labeling complex data structures as shareable (e.g., linked lists), we have to first apply label_shareable at the end of chains of references. The label_encapsulated operation on the other hand applies to private monotonic references with arbitrary preorders, which in turn necessitates the explicit comparison with label_map—something that follows implicitly for label_shareable due to the preorders of r and label_map being different. These operations are defined by appropriately modifying the ghost state storing the labeling.

Usability.  From our experience working on the examples in the paper, we report that the library  
interface is usable and, compared to the Monotonic State interface, the extra burden to the user is  
reasonable for the extra functionality. The main two differences are that the user has to specify both  
the footprint and what gets shared for each call, and to keep track of the labels of the references.  
Some of the details of the library are explicit into the interface, in particular predicates about the  
label_map reference, which are not relevant to the user, but the user does not have to deal with  
them because of F*'s SMT automation. We did not find a way to hide these details without losing  
expressiveness. On the other hand, the use of a deep embedding to implement the full ground  
types—which was necessary to prove preservation of the invariant inside the stateful operations—is  
not great for SMT automation, as sometimes the user has to help F* figure out what the type is.
type threep = I:(heap → Type0) & φ: (#a: → #rel: → mref a rel) & ≲:(preorder heap)

class poly_iface (preds:threep) (t:Type) = { wt : every_mref_tc t }

instance poly_iface_int preds : poly_iface preds int

instance poly_iface_sum preds a b {|poly_iface preds a|} {|poly_iface preds b|} : poly_iface preds (either a b)

instance poly_iface_ref preds (t_emb:full_groundjin) : poly_iface preds (ref (to_Type t_emb))

instance poly_ifaceArrow I φ ( ≲ ) a b { | c1:poly_iface (I, φ, ≲ ) a | } { | c2:poly_iface (I, φ, ≲ ) b | }

: poly_iface preds (x:a → MST b (requires (λ h₀ → I h₀ ∧ c1.wt.every mref x φ)) (ensures (λ h₀ r h₁ → I h₁ ∧ h₀ ≲ h₁ ∧ c2.wt.every mref φ r)))

<caption>Fig. 6. Showing the polymorphic interface implemented with type class poly_iface. Selected instances.</caption>

5 HIGHER-ORDER CONTRACTS

As explained in §2.3, SecRef* uses higher-order contracts at the boundary between verified and unverified code to ensure properties about returned or passed shareable references that cannot be statically determined. The higher-order contracts are built around two functions, import and export, that map from *intermediate types* to *source types*, and vice versa (Figure 3). We first introduce intermediate types in §5.1, and then explain in §5.2 how the export and import functions are defined.

5.1 The polymorphic and intermediate interfaces

The verified program and the unverified code communicate through an interface, which is different
in the source language compared to the target language. To represent the interface of unverified
code as presented in §2.2, we define in Figure 6 the type class poly_iface, parameterized by three
abstract predicates (threep). The types that can appear on the interface of unverified code are
thus determined by the instances we provide for the poly_iface class. We provide instances for
base types, sums, products, references, and arrow types. The instance for arrows is defined so that
poly_iface can be used to describe higher-order interfaces (e.g., polyosa from §2.2). Notice
that the instances for references and linked lists take a full ground type (§4.2). All types that have a
representation as a full ground type can be characterized by the poly_iface class.

Having defined polymorphic interfaces necessary to represent unverified code, we define in-
termediate interfaces as polymorphic interfaces instantiated with some concrete predicates, and
intermediate types as instances of such interfaces. Because we represent unverified code using
polymorphism (§2.2), our higher-order contracts have to be enforced on functions under polymor-
phism as well [4], which means that our contracts do not know what they enforce until the very
end, when the type is instantiated and the actual checks are provided.

5.2 Exporting and importing

The functions export and import are implemented using two type classes, named exportable_from and importable_to. To build an instance for exportable_from, one has to provide a function from a strong type (styp) to an intermediate type (ityp), and a proof that it preserves the every<sub>mref</sub> combinator. Such a proof is easy to provide because a reference is not affected by the export function since its type is restricted to be a full ground type—i.e., exporting a reference is identity. Its dual, importable_to is similar, but it has to account for potential breaches of contract by allowing import to fail with an error. We also provide a safe_importable_to class for types for which importing always succeeds.

To be able to export/import functions that are polymorphic in the three predicates (threep), the
type classes are parameterized with some implementation of the three predicates. The specs_of_styp
is just an inductive type that semi-syntactically represents the pre- and post-condition that appear on
type styp, structured as a tree. It allows us to be able to provide the contracts at importing/exporting
time, when the three predicates become concrete. The functions export and import take the contracts
as a tree of type `hoc_tree specs_of_styp`, which has the same structure as ` specs_of Typ`, and its type guarantees that each pre- and post-condition that has to be enforced has a contract.

```hhl
c exportable_from (preds:threep) (styp:Type) ( specs_of_styp:spec_tree preds ) = {
  c_styp : every_mref_tc styp;
  ityp : Type; c_ityp : poly_iface preds ityp;
  export : styp → hoc_tree specs_of_styp → ityp;
  export_preserves_φ : x:styp → φ: = hocs: = Lemma ( every_{mref φ x} ( every_{mref φ} (export x hocs) ) )
}
class importable_to (preds:threep) (styp:Type) ( specs_of_styp:spec_tree preds ) = {
  c_styp : every_mref_tc styp;
  ityp : Type; c_ityp : poly_iface preds ityp;
  import : ityp → hoc_tree specs_of_styp → either styp err;
  import_preserves_φ : x:ityp → φ: = hocs: = Lemma ( every_{mref φ x} ( every_{mref φ} (import x hocs) ) )
}
```

For intermediate types (and thus already in the source language), these type classes are trivially instantiated with identities, and for operators such as option, one proceeds recursively. For instance, the export function for option a when a is itself exportable will map the export function for a. What is more interesting is importing and exporting functions that may have pre- and post-conditions.

**Exporting functions.** We provide a general instance to export a function $f$ that has source type $a \to \text{MST}$ (either `b err`) pre post to a function of the intermediate type $a' \to \text{MST}$ (either $b'$ `err`) pre post', where $a'$ and $b'$ are the intermediate counterparts of $a$ and $b$, and pre' and post' are the pre- and post-condition that appear in `poly_ifacearrow` in Figure 6. For this, we need an import function ($a' \to a$) for type $a$ and an export function ($b \to b'$) for type $b$, which we then compose with $f$. To be able to call $f$, we have to ensure that pre holds, which we cannot do in general without a dynamic check, thus, the instance requires the existence of a check function which approximates the pre-condition:

```hhl
check : x:a \to \text{MST} \text{ (either unit err) (requires (pre' x)) (ensures } (\lambda h_0 \ r \ h_1 \to h_0 == h_1 \land (\text{Inl? r } \implies \text{pre } x \ h_0)))
```

which either returns an error or succeeds by enforcing pre. Notice that check may safely assume pre' as it holds when it is called. Finally, one has to ensure that post' holds, for which we require that the original post-condition of $f$ satisfies the following property: $\forall x h_0 \ r \ h_1$. post $x$ $h_0 \ r \ h_1 \implies$ post' $h_0 \ r \ h_1$. One detail that we omitted is that pre' and post' are polymorphic in the type of $x$ and $r$, compared to pre and post that use the types $a$ and $b$. Therefore, because we call import and export, we also have to prove that pre' $x \implies$ pre' (import $x$) and post' $h_0 \ r \ h_1 \implies$ post' $h_0$ (export $r$) $h_1$, which we do by using the two lemmas included in the type classes, `export_preserves_φ` and `import_preserves_φ`.

**Importing functions.** Similarly, we can import a general function $f$ of the intermediate type $x:a' \to \text{MST}$ (either $b'$ `err`) pre post' to the source type $x:a \to \text{MST}$ (either $b$ `err`) pre post. Because the type already accounts for errors, we use the `safe_importable_from` class to avoid duplicating errors. This time we export the input from $a$ to $a'$, call the function, and import the output from $b'$ to $b$. To be able to call the function $f$, we need to enforce pre' using pre, hence we only provide an instance under the assumption $\forall x h_0$. pre $x$ $h_0 \implies$ pre' $x$ $h_0$. Similarly, once the function is run, we only know that post' is verified, so we also require $\forall x h_0 \ e \ h_1$. pre $x$ $h_0 \land$ post' $h_0$ (Inr $e$) $h_1 \implies$ post $x$ $h_0$ (Inr $e$) $h_1$, which ensures we do preserve the post-condition of the error case. Often this will be discharged automatically by having the post-condition trivially true for errors. The more interesting part is when the function succeeds, and we need to verify the post-condition. For this, the instance also requires a stateful contract [15], see `select_check [4]` below:

```hhl
type cb_check a b {[} every_mref_tc b {]} pre post x eh =
  r:b \to \text{MST} \text{ (either unit err) } (\lambda h_1 \to \text{post' eh r } h_1) (\lambda h_1 \ rck h_1' \to h_1 == h_1' \land (\text{Inl? rck} \implies \text{post x eh r } h_1))
select_check : x:a \to \text{MST} \text{ (eh:erased heap {pre x eh} & cb_check a (either b err) pre post x eh)}
```
# 6 SECREF*: FORMALLY SECURE COMPILATION FRAMEWORK

In this section we present the formalization of SecRef\* (Figure 7). The formalization is mechanized in F\* and instantiates the compiler model presented by Abate et al. [1] with source and target languages that are shallowly embedded in the style of Andrici et al. [4]. We start by presenting the source (§6.1) and target language (§6.2). We continue by giving a semantics to them (§6.3). Then, we prove soundness and RrHP by carefully defining compilation and back-translation (§6.4). For all of these, we first present the setting when the verified program has initial control, however, SecRef\* is verified to be secure also when the unverified code has initial control (also §6.4).

## 6.1 Source Language

We make a clear split between the verified program and the code it is linked with. In the source language, we refer to the former as a partial source program, and the latter as a source context. The latter is also a verified piece of code, but for secure compilation we think of it as a target context (aka unverified) that was back-translated (the dual of compilation) to a source context (aka verified).

The partial source program and context communicate through a higher-order interface of type interface<sup>S</sup>, which contains a type (ctype), a type class constraint on this type (imp_ctype), and a post-condition $\psi$. As we want the type ctype to be polymorphic in the three predicates in our source language, so as to obtain a polymorphic type in the target language, we include the fields specs_of_ctype and hocs to be able to apply higher-order contracts to a polymorphic type as explained in §5.2. The representation of the partial source programs (prog<sup>S</sup>) is a computation in the monadic effect LR that takes as argument a value of type ctype instantiated with the concrete predicates, returns an integer, and ensures the post-condition $\psi$. The representation of source contexts (ctx<sup>S</sup>) is just a value of type ctype instantiated with the concrete predicates. Source linking (link<sup>S</sup>) is then defined just as function application. A whole source program is a dependent pair between a post-condition and a computation in effect LR from unit to integer that guarantees the post-condition.

The type class constraint imp_type guarantees that the specification on the interface can be soundly enforced by SecRef\*. The assumptions made about the unverified code appear on this source interface (e.g., the assumptions the autograder makes about the homework in Figure 1), and imp_type ensures that they are one of the two types of assumptions that SecRef\* supports (§2.1).

## 6.2 Target language

The formalization of the target language is similar to the source language, with two notable differences: the representation of partial target programs (prog<sup>T</sup>) does not require the computation to be verified with respect to a post-condition, since it has the trivial post-condition; and target contexts (ctx<sup>T</sup>) use the representation from §2.2. The type ctype in the target interface (of type interface<sup>T</sup>), now is constrained with the poly_iface type class from §5.1.

A partial target program (see prog<sup>T</sup>) expects the context to satisfy the concrete specification it assumes about the context: to only modify shareable and encapsulated references. Therefore, linking is done at the types of the target language, but after linking, the communication between the program and the context happens at an intermediate type that contains specifications [4]. This can be seen in the definition of target linking (link<sup>T</sup>). It instantiates the target context with the concrete predicates $I_c$, $\varphi_c$, and $\ll_c$, thus strengthening the type of the context.

During linking, the concrete implementations of the operations alloc, read, and write are provided. As explained in §2.2, their definitions are straightforward (specifications and proofs elided):

let ctx_alloc init = let r = lr_alloc init in label_shareable r; r / let ctx_read = lr_read / let ctx_write = lr_write

The representation of target contexts is a reasonable representation for unverified code—logical reasoning is not necessary to prove the pre- and post-conditions that use the abstract predicates. As
noted in §2.2, we deeply embed a total simply typed language with first-order ML-style references, and provide a translation from any typed expression in this language to a context of type ctype to the representation of target contexts `ctx^T`. The translation is defined structurally recursively on the typing derivations. Formalizing this translation revealed multiple edge cases in higher-order settings, and also the fact that monotonic references cannot be shared with unverified code. This gives us sufficient confidence that our representation is reasonable, in addition to multiple examples we implemented using this representation in the artifact (e.g., the homework in §2.2).

## 6.3 Semantics

Our source and target languages are shallowly embedded. Since whole source and target programs are computations in the LR effect, we can define the same semantics for both. We define this semantics as predicates over the initial heap, the final result (an integer), and the final heap.

```
type state = heap → state → heap → Type₀
let (⊆) (s₁ s₂:state) = ∀h₀ r h₁. s₁ h₀ r h₁ =⇒ s₂ h₀ r h₁
```

To define the semantics of whole programs, we must first reveal the monadic representation of LR using the reify construct provided by F\* [47]. We define the semantics function `beh` by adapting the monad morphism $\theta$ from §3.2 [4, 34].

```
let beh_mst (m:mst_repr int) : state = λh₀ r h₁ → ∀p. θ m p h₀ =⇒ p r h₁
let beh (W:unit → LR int τ) = beh_mst (reify (W ()))
```

Since we use $\theta$ for both the Dijkstra monad and our semantics function, we can easily turn the intrinsic property that a whole source program satisfies a post-condition $\psi$ into an extrinsic property:

**THEOREM 6.1 (SOUNDNESS OF WHOLE SOURCE PROGRAMS).** $\forall (\psi, W) : \text{whole}^S$. $\text{beh}(W) \subseteq \psi$

**PROOF SKETCH.** For a whole source program, we know its underneath monadic representation is $m:(mst_repr int)\{\theta m \subseteq (\lambda p h_0 \to \forall r h_1. \psi h_0 r h_1 = p r h_1)\}$ (§3.2), which implies that $\text{beh} m \subseteq \psi$. $\square$

The proof is so straightforward because the type of a whole source program contains an intrinsic specification. We just lift the specification to an extrinsic property of the whole program. Intuitively, the proof that the program satisfies the specification was already done modularly by F\* typing.

*Trusted Computing Base (TCB).* The semantics function is written in the same language as the code it reasons about, meaning that the semantics a program is given depends on F\*'s consistency. Therefore, as part of our TCB we include the following F\* features that SecRef\* relies on: F\*'s type system, the effect mechanism (which has a paper proof), the axiomatized *Ghost* effect, and the type abstractions provided by the module system (e.g., the implementation of references is hidden behind a module interface).

## 6.4 Soundness and Robust Relational Hyperproperty Preservation (RrHP)

Andrici et al. [4], in their setting for IO, show that soundness and RrHP can be proved using a Syntactic Inversion Law, informally, *Compilation+Target Linking=Back-translation+Source Linking*. Such a strong result is achievable because we are working with shallow embeddings, we take advantage of polymorphism to model the context, and we implement higher-order contracts using two dual functions. We managed to adapt their compilation model in our setting for state, and to prove the law and the two criteria by following their proofs.

We define the compilation of partial programs (compileula in Figure 7, denoted as $P \downarrow$) as wrapping the partial source program in a new function of type $prog^T$. The partial target program takes as argument an instantiated target context whose specification states that it modifies only
shareable references. Therefore, to enforce the other assumptions made by the partial source program, SecRef* adds to the compiled program the higher-order contracts using safe_import.

We define the back-translation of target contexts (denoted by $C\uparrow$) as instantiating the context and then adding the higher-order contracts to produce a source context. One immediately observes that this is exactly what happens during compilation plus target linking, and since source linking is just function application, it means syntactic inversion law can be proved just by unfolding definitions.

**THEOREM 6.2 (SYNTACTIC INVERSION LAW).** $\forall I^S. \forall C^T : \text{ctx}^T I^S \downarrow. \forall P : \text{prog}^S I^S. C^T [P \downarrow] = C^T \uparrow [P]$

SecRef* allows one to statically verify that a partial program satisfies a post-condition $\psi$. We prove a soundness theorem that guarantees that compiling the partial program and then linking it with arbitrary unverified code produces a whole target program that also satisfies the post-condition $\psi$ (when the partial program has initial control).

**THEOREM 6.3 (SOUNDNESS).** $\forall I^S. \forall P : \text{prog}^S I^S. \forall C^T : \text{ctx}^T I^S \downarrow. \text{beh}(C^T [P \downarrow]) \subseteq I^S \psi$

**PROOF SKETCH.** We rewrite the goal with Theorem 6.2 to $C^T [P \downarrow] = C^T \uparrow [P]$. Now, $C^T \uparrow [P]$ builds a whole source program and we can apply Theorem 6.1. $\square$

We prove that SecRef* robustly preserves relational hyperproperties. Abate et al. [1] have this as their strongest secure compilation criterion, and they show it is stronger than full abstraction.

**THEOREM 6.4 (ROBUST RELATIONAL HYPERPROPERTY PRESERVATION (RRHP)).**

$$ \forall I^S. \forall C^T : \text{ctx}^T I^S \downarrow. \exists C^S : \text{ctx}^S I^S. \forall P : \text{prog}^S I^S. \text{beh}(C^T [P \downarrow]) = \text{beh}(C^S [P]) $$

**PROOF SKETCH.** The proof follows by back-translating the target context ($C^T \uparrow$) and using it to instantiate the existential of a source context, after which we conclude with Theorem 6.2. $\square$

Finally, we have proved that SecRef* also satisfies RrHP (Theorem 6.4) in two other settings as Andrici et al. [4]. **The dual setting: when the context has initial control.** In this setting, the proofs are similar, since Theorem 6.2 again holds. Instead of soundness, we proved the dual of soundness, a less interesting criterion stating that the resulting whole target program modifies only shareable references. As a sanity check that our shallow embedding of unverified code is correct, we also proved RrHP in **the setting where target contexts are represented with typed syntactic expressions** of the deeply-embedded language mentioned in §2.2, a case in which target linking and back-translation first do the extra step of translating the expression into the representation for target contexts ($\text{ctx}^T$). The proofs can be found in the artifact.

# 7 CASE STUDY: SIMPLE STATEFUL COOPERATIVE MULTI-THREADING

To test our framework further, we verify a simple stateful cooperative multi-threading case study. In this case study, we are particularly interested in showcasing how scheduling properties can be verified, even when the verified scheduler is orchestrating tasks that are themselves unverified.

Our model of cooperative multi-threading is inspired by the work of Dolan et al. [13] in the context of OCaml, where effect handlers are used to program concurrent systems. In this model, running threads are represented as computation trees. A computation tree is either a final value or a computation yielding control to the next task. When yielding control, the continuation is a stateful computation that returns a new computation tree. We can model these trees as follows:

type atree (a:Type0) = | Return : a → atree a | Yield : continuation a → atree a and continuation a = unit → LR (atree a) (requires (λ h0 → T)) (ensures (λ h0 _ h1 → h0 ≪c h1))
Continuations represent unverified code, and their specification consists of a trivial precondition and a postcondition stating the unverified code only modifies *shareable* (or encapsulated) references using the relation $\ll_c$ from Figure 7. As before, we omit reference containment requirements from pre- and post-conditions, along with fuel parameters used for proving termination.

We model the scheduler state using a private reference, which stores (i) an execution history (a list of thread IDs), (ii) the ID of the next thread to be executed, and (iii) a count of the number of finished threads (to which we refer as *inactive*). We refine the scheduler state by adding a simple fairness property: each thread must have taken either ticks or ticks + 1 steps, ensuring fair progress among all threads (with ticks logically incremented on each round of the round-robin progress):

let fairness ticks (limit : int) (ticks : nat) (hist : list int) (next : int) = ...

let fairness (limit : int) (hist : list int) (next : int) = $\exists$ ticks : nat . fairness ticks limit ticks hist next

In the refined scheduler state, we also ensure that both the next thread and inactive counts are within valid ranges. The argument *k* is used to keep track of the number of threads passed to the scheduler on initialization. In detail, we define it as follows:

type count_st k = hist:(list int) & next:int & inact:int{fairness k hist next ∧ 0 ≤ next < k ∧ 0 ≤ inact ≤ k}

let counter_preorder k : preorder (count_st k) = λv v' → v.₁ `prefix_of` v'.₁

let counter_t k = mref (count_st k) (counter_preorder k)

The scheduler is implemented as a structurally recursive function with the following type:

val scheduler (r : ref int) (tasks:list (continuation unit)) (counter:counter_t (length tasks))

: LR unit (requires (λ h₀ → is_private counter h₀ ∧ is_shareable r h₀))

(ensures (λ h₀ _ h₁ → modif_shareable_encaps_and h₀ h₁ !{counter} ∧ gets_shared empty h₀ h₁))

It takes a global shared reference *r* to an integer (which can be accessed by any of the involved stateful computations), a list of tasks to be executed (represented as unit-typed continuations), and the reference to the current state of the scheduler (which is required to be *private* in the pre-condition). On each iteration, the scheduler picks the next task to be run, runs it, and acts depending on whether the outcome was a final value or a computation yielding control. We are guaranteed that at each step we run a next task from the given task list and only shared references are modified. This invariant allows us to verify the fairness property of the scheduler’s state, as we know that the counter reference was not modified by the tasks. In comparison to the post-condition of unverified code, notice that the post-condition for the scheduler ensures that no labels are modified, but we do not claim to have only modified shared and encapsulated variables: the scheduler state gets updated as the scheduler runs the tasks.

Building on the scheduler implementation, we can write a function to run a list of computations.

let run (v:int) (tasks:list (ref int → continuation unit){length tasks > 0}) : LR int

(requires (λ h₀ → forall_refs_heap contains_pred h₀ v ∧ $\forall$ refs_heap is_shareable h₀ v))

(ensures (λ h₀ _ h₁ → h₀ $\ll_c$ h₁)) =

let counter : counter_t (length tasks) = alloc (| [] , 0 , 0 |) in

let r = alloc v in label_shareable r;

let tasks = map (λ (f : ref int → continuation unit) → f r) tasks in

scheduler r tasks counter;

!r

Here we allocate two references: one that is shared by the different tasks (and thus it is labeled *shareable*) and one that is used to store the scheduler’s state (and which is kept *private*). We then run the computations using the scheduler and in the end return the final value of the shared reference. The scheduler starts with an empty history, the first task selected, and zero inactive tasks. After
its execution, the final history satisfies the fairness predicate, indicating that all tasks took the
same number of steps. However, this fact is not made explicit in the postcondition of run, which
only focuses on the references modified during the execution. As a final remark, we note that the
function run can also be called by unverified code to cooperatively execute other unverified code.
Importantly, run has the exact same post-condition as unverified code (as used in the continuations).

8 RELATED WORK

*Verification of stateful code.* Labeled References are encoded in F* on top of Monotonic State, and this enables specifying the footprint of a call using labels, which allows us to tame the complexity of globally tracking the dynamically shared references. As explained in §2.1, the usual way of specifying the footprint of a call, by providing the precise set of references that gets modified [3, 30, 49], does not scale to higher-order unverified code when dynamic sharing of references is allowed. This approach enabled verification of stateful F* programs linked with unverified code. Similar approaches [50, 56] were used to build logics on Iris [25] for verifying such programs, with which we compare next.

*Capabilities and robust safety.* Swasey et al. [56] introduce OCPL, a logic for verifying object capability patterns. It can be used to verify concurrent, non-terminating, stateful programs that are fully higher-order, including support for higher-order references. OCPL has a notion of high and low references, where high references can be wrapped in closures that are passed to the untrusted code, while low references are considered shared between the trusted and untrusted code. In OCPL, low references can only point to low references, and callbacks that are crossing the verified-unverified boundary can take as argument and return only low references. This notion of high and low references seems to correspond to the *private/encapsulated* and *shareable* labels in Labeled References. Swasey et al. [56] prove a robust safety theorem stating that code verified with OCPL can be safely linked with arbitrary unverified code. They then use OCPL to verify the robust safety of using wrappers like dynamic sealing, the caretaker pattern and the membrane pattern. By comparison, SecRef* is a secure compilation framework using higher-order contracts that dynamically enforce specifications about shared references. Soundness of SecRef* (Theorem 6.3) intuitively provides similar guarantees to OCPL's robust safety theorem. SecRef* additionally satisfies RrHP (Theorem 6.4), the preservation of a large class of properties including robust safety.

Georges et al. [20] propose Cerise: a program logic for reasoning about a low-level capability machine. It guarantees robust safety of verified code that interacts with unverified code in multiple scenarios: when the verified-unverified code share static allocated memory, when they use wrappers in the style of Swasey et al. [56], and when the unverified code can allocate dynamically its own memory. To obtain safety in the last scenario, they use activation records, a technique involving saving the content of the references that are not in the call's footprint, and restoring them after the call, but it is done dynamically and adds an extra cost. In our work, unverified code can also allocate its own memory dynamically, and we show how to specify the footprint using labels so that there is no need to perform dynamic restoring of references when calling into unverified code.

In a setting where, instead of ML-style references, one uses integer pointers that can be dereferenced, Sammler et al. [50] showed that one can enforce robust safety by using sandboxing. They allow sharing dynamically allocated pointers between verified and unverified code under some conditions: they have to clearly distinguish between the *high heap* of the trusted code and the *low heap* of the untrusted code, something we do not have to do because our references are unforgeable.

*Secure compilation.* The approaches of Agten et al. [2] and Strydonck et al. [53] support secure compilation of formally verified stateful programs against unverified contexts. Agten et al. [2] securely compile modules verified with separation logic [49], but written in the C language, which normally lacks memory safety. To overcome that, they add runtime checks at the boundary between
verified and unverified code, and also use two static notions of memory: local, which is never shared with the unverified code, and heap memory, which the unverified code can read and write arbitrarily because of the lack of memory safety. The local memory is protected using hardware enclaves, and if one wants to share data from local memory, one has to copy it to the heap memory. To protect the heap memory when calling into the unverified code, they first hash the complement of the assumed footprint of the call, and when control is returned, they recompute the hash and compare it, to make sure that the unverified code did not change heap locations outside the footprint. What we do is different because we work with memory safe languages with ML-style references, which act like capabilities. We show that if the source and target language have capabilities, one can avoid these expensive hash computations by getting the footprint right. Moreover, we have only one notion of references, which can be kept private or be dynamically shared with the unverified code by using the labeling mechanism.

Strydonck et al. [53] compile stateful code verified with separation logic to a target language with hardware-enforced *linear* capabilities, which cannot be duplicated at runtime. The main idea is to require the unverified context to return the linear capabilities back so that the verified code can infer that the context cannot have stored them. Linear capabilities are, however, an unconventional hardware feature that is challenging to efficiently implement in practice [19]. In contrast to their solution, *SecRef*\* provides soundness and security in a target language with ML-style mutable references, which can be implemented using standard capabilities [57], but this required us to overcome the challenge of unverified contexts that stash references.

New et al. [39] propose a fully abstract compiler from a simply typed $\lambda$-calculus with unit, sums, pairs, and recursive types to a target language that has additional support for exceptions. Their compiler is not, however, addressing ML-references or verified code as ours does. The full abstraction property is a security criterion that was shown to be implied by the criterion we prove about our compiler, RrHP (Theorem 6.4), by Abate et al. [1]. New et al. [39] employ a comparable approach to ours to prove full abstraction, involving a translation between two shallow embeddings.

*Gradual verification.* is a combination of static and dynamic verification proposed by Bader et al. [9]. For assertions that cannot be proven statically using the existing code annotations, one can opt to let the tool insert dynamic checks that dynamically enforce the assertion. DiVincenzo et al. [12] introduced Gradual C0 to do gradual verification for stateful programs. Gradual C0 requires analyzing the unverified code, while our DSL does not. Gradual C0 requires the unverified code to determine what checks to add, and it can be many, while *SecRef*\* avoids adding checks to preserve logical invariants about private references. *SecRef*\* adds higher-order contracts to enforce pre- and post-conditions at the boundary of verified-unverified code. In the absence of unverified code, the dynamic checks are necessary to be able to establish logical predicates about shareable references.

*Secure interoperability.* There is also related work based on typed approaches to safe interoperability between high and low-level code that share references. The main difference with those works is that they look at safe interoperability between languages with different semantics, while we look at code *verified* in the traditional Hoare/separation-logic style and unverified code. Patterson et al. [43] present a multi-language that supports interoperability between a simply typed functional language and a typed assembly language. Their multi-language allows integrating assembly code into the functional language, and reason about their mix. Patterson and Ahmed [42] present the notion of linking types, a more expressive way to annotate the interface, that enable one to reason about behavioral equality using only one language, even though the code may be linked with code written in a different language with more expressive power. Patterson et al. [44] show how to soundly encapsulate foreign code using linked types, so that the foreign code is unobservable and the invariants of the language are undisturbed.
# 9 CONCLUSIONS AND FUTURE WORK

In this paper we introduce SecRef*, a secure compilation framework that allows for the sound verification of stateful programs that can be compiled and then linked with arbitrary unverified code, importantly allowing dynamic sharing of mutable references. SecRef* solves a problem that, to our knowledge, exists in all proof-oriented programming languages (Rocq, Lean, Isabelle/HOL, Dafny, F*, etc). We present our contributions in the context of F*, but we believe many of the ideas could be applied to other proof-oriented programming languages as well, especially to the dependently-typed ones. Our monadic representation for Monotonic State, which uses a Dijkstra monad, can be ported to other dependently-typed languages (e.g., Dijkstra monads also have been implemented in Rocq [34, 51]). Once Monotonic State is ported, we believe one should be able to port the other contributions we present in this paper too: Labeled References, the higher-order contracts, the model for secure compilation, and the soundness and RrHP proofs. Dijkstra monads work well in F* because of SMT automation and the effect mechanism of F*, but they are not the standard means to perform verification in other proof-oriented programming languages. Dijkstra monads are however just a way to reason about monadic computations, thus one could instead use other frameworks built to reason about monadic computations [32, 35, 59, 60].

We believe that SecRef* is a significant step towards the long-term goal of building a secure compiler from F* to OCaml. We see four orthogonal open problems that need to be solved to reach this goal: (1) *Modeling higher-order store* for effectful functions around F*'s predicative, countable hierarchy of universes. Koronkevich and Bowman [28] propose an acyclic higher-order store, but this would not be sufficient to model realistic attackers written in OCaml (e.g., no support for Landin's Knot [29]). In a different type theory than that of F*, Frumin et al. [18] adapt Interaction Trees to Guarded Type Theory to support cyclic higher-order stores. (2) *Modeling more of the effects of OCaml* by extending the representation of the monadic effect, and then figuring out how this impacts the soundness and security guaranteed by SecRef*. While this was already studied separately for the IO effect [4], how other effects would impact soundness and security is an open question. For example, adding non-termination would involve switching from the inductive definition of the Free monad to a co-inductive definition (probably of Interaction Trees [51, 59]), and probably would involve assuming that untrusted code can always loop. (3) *End-to-end verified compilation to OCaml*. While SecRef* targets a language shallowly embedded in F*, at least two more steps are necessary to target OCaml, both open research problems: verified quoting<fnref n="9" /> (to go from the shallow embedding to a deep embedding), and verified erasure specialized for a Dijkstra monad. Forster et al. [16] present a verified correct erasure from Rocq to Malfunction (one of the intermediate languages of OCaml), which we hope can be specialized to computations represented using monads and extended to verify security. Their proof relies on the formalization of Rocq [52], which means that before one is able to reproduce and extend their proof, one would first have to give a formalization to F*. (4) *Encoding Labeled References on top of Separation Logic*, yet how to do Separation Logic in F* well is itself a topic of ongoing research [14, 17, 54].

Finally, it would be interesting to do a performance evaluation of the added higher-order contracts. To improve performance, one could try to extend SecRef* so that it statically analyzes unverified code and discards the contracts using soft contract verification [40, 41].

# DATA AVAILABILITY STATEMENT

This paper comes with an F* artifact that includes the full implementation of SecRef*, the machine-checked proofs, and examples. The examples can be extracted to native OCaml code (without any monadic representation). The artifact is available on Zenodo [6] and Github [5].

<footnote n="9">⁹Verifying quoting in MetaRocq: https://github.com/MetaRocq/metarocq/blob/coq-8.16/quotation/theories/README.md</footnote>
## ACKNOWLEDGMENTS

This work was in part supported by the European Research Council under ERC Starting Grant SECOMP (715753), by the German Federal Ministry of Education and Research BMBF (grant 16KISK038, project 6GEM), and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) as part of the Excellence Strategy of the German Federal and State Governments – EXC 2092 CASA - 390781972. Exequiel Rivas was supported by the Estonian Research Council starting grant PSG749. Danel Ahman was supported by the Estonian Research Council grant PRG2764.

## A ADDITIONAL EXAMPLE: GUESSING GAME

To showcase the use of encapsulated references, in Figure 8 we present another example of a verified program that plays the “guess the number I’m thinking of” with an unverified player. The verified program gives to the player a range and a callback that the player can use to guess the number. The verified program saves the guesses of the player using an encapsulated monotonic reference that has a preorder that ensures that no guess is forgotten (line 5). SecRef* does not add any dynamic checks using higher-order contracts during compilation because the post-condition of the player follows from the universal property of unverified code (§2.2).

1. type cmp = | LT | GT | EQ
2. let post = λh₀ _ h₁ → modif_shareable_and_encaps h₀ h₁ ∧ same labels h₀ h₁
3. type player_t = (l:int * r:int * (guess:int → LR cmp (λ _ → T) post)) → LR int (λ _ → l < r) post
4. let play.guess (l pick r:int) (player:player_t) : LR (bool * list int) (λ _ → l < pick ∧ pick < r) post =
5. let guesses : mref (list int) (λ l l' → l 'prefix_of ` l') = alloc [] in label_encapsulate guesses;
6. let final.guess =
7. player (λ x → guesses := guesses @ [x]; if pick = x then EQ else if pick < x then LT else GT) in
8. guesses := guesses @ [final.guess];
9. if pick = final.guess then (true, ! guesses)
10. else (false, ! guesses)

<caption>Fig. 8. The illustrative example of a function that plays "Guess the number I'm thinking of"</caption>

## REFERENCES

[1] C. Abate, R. Blanco, D. Garg, C. Hritcu, M. Patrignani, and J. Thibault. Journey beyond full abstraction: Exploring robust property preservation for secure compilation. CSF. 2019.

[2] P. Agten, B. Jacobs, and F. Piessens. Sound modular verification of C code executing in an unverified context. POPL. 2015.

[3] D. Ahman, C. Fournet, C. Hrițcu, K. Maillard, A. Rastogi, and N. Swamy. Recalling a witness: Foundations and applications of monotonic state. PACMPL, 2(POPL):65:1–65:30, 2018.

[4] C.-C. Andrici, Ş. Ciobăcă, C. Hritcu, G. Martínez, E. Rivas, É. Tanter, and T. Winterhalter. Securing verified IO programs against unverified code in F*. Proc. ACM Program. Lang., 8(POPL):2226–2259, 2024.

[5] C.-C. Andrici, D. Ahman, C. Hrițcu, R. Icleanu, G. Martínez, E. Rivas, and T. Winterhalter. Artifact for the ICFP 2025 paper 'SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*'. GitHub, 2025.

[6] C.-C. Andrici, D. Ahman, C. Hritcu, R. Icleanu, G. Martínez, E. Rivas, and T. Winterhalter. SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F* - ICFP 2025 Artifact, 2025.

[7] A. W. Appel. Modular verification for computer security. CSF. 2016.

[8] A. Arasu, T. Ramananandro, A. Rastogi, N. Swamy, A. Fromherz, K. Hietala, B. Parno, and R. Ramamurthy. FastVer2: A provably correct monitor for concurrent, key-value stores. CPP. 2023.

[9] J. Bader, J. Aldrich, and É. Tanter. Gradual program verification. VMCAI. 2018.

[10] K. Bhargavan, A. Bichhawat, Q. H. Do, P. Hosseyni, R. Küsters, G. Schmitz, and T. Würtele. An in-depth symbolic security analysis of the ACME standard. CCS. 2021.

[11] A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, J. Protzenko, A. Rastogi, N. Swamy, S. Z. Béguelin, K. Bhargavan, J. Pan, and J. K. Zinzindohoue. Implementing and proving the TLS 1.3 record layer. IEEE S&P. 2017.
[12] J. DiVincenzo, I. McCormack, C. Zimmerman, H. Gouni, J. Gorenburg, J.-P. Ramos-Dávila, M. Zhang, J. Sunshine, E. Tanter, and J. Aldrich. *Gradual C0: Symbolic execution for gradual verification*. *ACM Trans. Program. Lang. Syst.*, 46 (4), 2025.

[13] S. Dolan, S. Eliopoulos, D. Hillerström, A. Madhavapeddy, K. C. Sivaramakrishnan, and L. White. *Concurrent system programming with effect handlers*. In M. Wang and S. Owens, editors, *Trends in Functional Programming - 18th International Symposium, TFP 2017, Canterbury, UK, June 19-21, 2017, Revised Selected Papers*. 2017.

[14] G. Ebner, G. Martínez, A. Rastogi, T. Dardinier, M. Frisella, T. Ramananandro, and N. Swamy. *PulseCore: An impredicative concurrent separation logic for dependently typed programs*. *Proc. ACM Program. Lang.*, (PLDI), 2025.

[15] R. B. Findler and M. Felleisen. *Contracts for higher-order functions*. *ICFP*. 2002.

[16] Y. Forster, M. Sozeau, and N. Tabareau. *Verified extraction from Coq to OCaml*. *Proc. ACM Program. Lang.*, 8(PLDI): 52-75, 2024.

[17] A. Fromherz, A. Rastogi, N. Swamy, S. Gibson, G. Martínez, D. Merigoux, and T. Ramananandro. *Steel: proof-oriented programming in a dependently typed concurrent separation logic*. *Proc. ACM Program. Lang.*, 5(ICFP):1-30, 2021.

[18] D. Frumin, A. Timany, and L. Birkedal. *Modular denotational semantics for effects with guarded interaction trees*. *Proc. ACM Program. Lang.*, 8(POPL):332-361, 2024.

[19] A. L. Georges, A. Guéneau, T. V. Strydonck, A. Timany, A. Trieu, S. Huyghebaert, D. Devriese, and L. Birkedal. *Efficient and provable local capability revocation using uninitialized capabilities*. *Proc. ACM Program. Lang.*, 5(POPL):1-30, 2021.

[20] A. L. Georges, A. Guéneau, T. V. Strydonck, A. Timany, A. Trieu, D. Devriese, and L. Birkedal. *Cerise: Program verification on a capability machine in the presence of untrusted code*. *J. ACM*, 71(1):3:1-3:59, 2024.

[21] R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim, V. Sjöberg, and D. Costanzo. *CertiKOS: An extensible architecture for building certified concurrent OS kernels*. *OSDI*. 2016.

[22] T. Hance, A. Lattuada, C. Hawblitzel, J. Howell, R. Johnson, and B. Parno. *Storage systems are distributed systems (so verify them that way!)*. *OSDI*. 2020.

[23] S. Ho, J. Protzenko, A. Bichhawat, and K. Bhargavan. *Noise*: A library of verified high-performance secure channel protocol implementations. *IEEE S&P*. 2022.

[24] R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer. *Higher-order ghost state*. In J. Garrigue, G. Keller, and E. Sumii, editors, *Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016*. 2016.

[25] R. Jung, R. Krebbers, J. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer. *Iris from the ground up: A modular foundation for higher-order concurrent separation logic*. *J. Funct. Program.*, 28:e20, 2018.

[26] O. Kammar, P. B. Levy, S. K. Moss, and S. Staton. *A monad for full ground reference cells*. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*. 2017.

[27] G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. A. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. *seL4: formal verification of an operating-system kernel*. *CACM*, 53 (6):107-115, 2010.

[28] P. Koronkevich and W. J. Bowman. *Type universes as Kripke Worlds*. *Proc. ACM Program. Lang.*, 9(ICFP), 2025.

[29] P. J. Landin. *The mechanical evaluation of expressions*. *The Computer Journal*, 6(4):308-320, 1964.

[30] K. R. M. Leino. *Dafny: An automatic program verifier for functional correctness*. *LPAR*. 2010.

[31] X. Leroy. *Formal verification of a realistic compiler*. *CACM*, 52(7):107-115, 2009.

[32] T. Letan and Y. Régis-Gianas. *FreeSpec: specifying, verifying, and executing impure computations in Coq*. *CPP*. 2020.

[33] J. Li, A. Lattuada, Y. Zhou, J. Cameron, J. Howell, B. Parno, and C. Hawblitzel. *Linear types for large-scale systems verification*. *OOPSLA*, 2022.

[34] K. Maillard, D. Ahman, R. Atkey, G. Martínez, C. Hriţcu, E. Rivas, and E. Tanter. *Dijkstra monads for all*. *PACMPL*, 3 (ICFP), 2019.

[35] K. Maillard, C. Hriţcu, E. Rivas, and A. Van Muylder. *The next 700 relational program logics*. *PACMPL*, 4(POPL): 4:1-4:33, 2020.

[36] A. S. Murawski and N. Tzevelekos. *Algorithmic games for full ground references*. In A. Czumaj, K. Mehlhorn, A. M. Pitts, and R. Wattenhofer, editors, *Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II*. 2012.

[37] A. S. Murawski and N. Tzevelekos. *Algorithmic games for full ground references*. *Formal Methods Syst. Des.*, 52(3): 277-314, 2018.

[38] T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. *seL4: From general purpose to a proof of information flow enforcement*. *IEEE S&P*. 2013.

[39] M. S. New, W. J. Bowman, and A. Ahmed. *Fully abstract compilation via universal embedding*. In J. Garrigue, G. Keller, and E. Sumii, editors, *Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016*. 2016.
[40] P. C. Nguyen, S. Tobin-Hochstadt, and D. V. Horn. *Soft contract verification*. ICFP, 2014.

[41] P. C. Nguyen, T. Gilray, S. Tobin-Hochstadt, and D. V. Horn. *Soft contract verification for higher-order stateful programs*. Proc. ACM Program. Lang., 2(POPL):51:1–51:30, 2018.

[42] D. Patterson and A. Ahmed. Linking types for multi-language software: Have your cake and eat it too. In B. S. Lerner, R. Bodik, and S. Krishnamurthi, editors, *2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA*. 2017.

[43] D. Patterson, J. Perconti, C. Dimoulas, and A. Ahmed. *Funtal: reasonably mixing a functional language with assembly*. In A. Cohen and M. T. Vechev, editors, *Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017*. 2017.

[44] D. Patterson, A. Wagner, and A. Ahmed. *Semantic encapsulation using linking types*. In Y. Cong and P. Dagand, editors, *Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2023, Seattle, WA, USA, 4 September 2023*. 2023.

[45] J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, A. Delignat-Lavaud, C. Fournet, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. M. Wintersteiger, and S. Z. Béguelin. *EverCrypt: A fast, verified, cross-platform cryptographic provider*. IEEE S&P. 2020.

[46] T. Ramananandro, A. Delignat-Lavaud, C. Fournet, N. Swamy, T. Chajed, N. Kobeissi, and J. Protzenko. *EverParse: Verified secure zero-copy parsers for authenticated message formats*. USENIX Security. 2019.

[47] A. Rastogi, G. Martínez, A. Fromherz, T. Ramananandro, and N. Swamy. *Programming and proving with indexed effects*, 2021.

[48] J. Reed. *A Hybrid Logical Framework*. PhD thesis, Carnegie Mellon University, 2009.

[49] J. C. Reynolds. *Separation logic: A logic for shared mutable data structures*. In *17th IEEE Symposium on Logic in Computer Science (LICS 2002)*, 22-25 July 2002, Copenhagen, Denmark, *Proceedings*. 2002.

[50] M. Sammler, D. Garg, D. Dreyer, and T. Litak. *The high-level benefits of low-level sandboxing*. Proc. ACM Program. Lang., 4(POPL):32:1–32:32, 2020.

[51] L. Silver and S. Zdancewic. *Dijkstra monads forever: termination-sensitive specifications for interaction trees*. Proc. ACM Program. Lang., 5(POPL):1–28, 2021.

[52] M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, and T. Winterhalter. *Coq Coq correct! Verification of type checking and erasure for coq, in Coq*. Proc. ACM Program. Lang., 4(POPL):8:1–8:28, 2020.

[53] T. V. Strydonck, F. Piessens, and D. Devriese. *Linear capabilities for fully abstract compilation of separation-logic-verified code*. J. Funct. Program., 31:e6, 2021.

[54] N. Swamy, A. Rastogi, A. Fromherz, D. Merigoux, D. Ahman, and G. Martínez. *SteelCore: An extensible concurrent separation logic for effectful dependently typed programs*. Proc. ACM Program. Lang., 4(ICFP), 2020.

[55] N. Swamy, T. Ramananandro, A. Rastogi, I. Spiridonova, H. Ni, D. Malloy, J. Vazquez, M. Tang, O. Cardona, and A. Gupta. *Hardening attack surfaces with formally proven binary format parsers*. In R. Jhala and I. Dillig, editors, *PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022*. 2022.

[56] D. Swasey, D. Garg, and D. Dreyer. *Robust and compositional verification of object capability patterns*. PACMPL, 1 (OOPSLA):89:1–89:26, 2017.

[57] R. N. M. Watson, P. G. Neumann, J. Woodruff, M. Roe, H. Almatary, J. Anderson, J. Baldwin, G. Barnes, D. Chisnall, J. Clarke, B. Davis, L. Eisen, N. W. Filardo, R. Grisenthwaite, A. Joannou, B. Laurie, A. T. Markettos, S. W. Moore, S. J. Murdoch, K. Nienhuis, R. Norton, A. Richardson, P. Rugg, P. Sewell, S. Son, and H. Xia. *Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8)*. Technical Report UCAM-CL-TR-951, University of Cambridge, Computer Laboratory, 2020.

[58] T. Winterhalter, C.-C. Andrici, C. Hriţcu, K. Maillard, G. Martínez, and E. Rivas. *Partial Dijkstra Monads for all*. TYPES, 2022.

[59] L. Xia, Y. Zakowski, P. He, C. Hur, G. Malecha, B. C. Pierce, and S. Zdancewic. *Interaction trees: representing recursive and impure programs in Coq*. Proc. ACM Program. Lang., 4(POPL):51:1–51:32, 2020.

[60] I. Yoon, Y. Zakowski, and S. Zdancewic. *Formal reasoning about layered monadic interpreters*. Proc. ACM Program. Lang., 6(ICFP), 2022.

[61] Y. Zakowski, C. Beck, I. Yoon, I. Zaichuk, V. Zaliva, and S. Zdancewic. *Modular, compositional, and executable formal semantics for LLVM IR*. Proc. ACM Program. Lang., 5(ICFP):1–30, 2021.

[62] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche. *HACL*: A verified modern cryptographic library. CCS. 2017.