Authors: Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
Paper Content:
Page 1:
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 HRIT ,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 propose a way of tracking 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.
1 INTRODUCTION
Verifying stateful programs using proof-oriented languages like Rocq, Lean, Isabelle/HOL, Dafny,
and F★is being applied to increasingly realistic projects [Appel 2016; Arasu et al. 2023; Bhargavan
et al. 2021; Delignat-Lavaud et al. 2017; Gu et al. 2016; Hance et al. 2020; Ho et al. 2022; Klein et al.
2010; Leroy 2009; Li et al. 2022; Murray et al. 2013; Ramananandro et al. 2019; Zakowski et al. 2021].
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 [Ahman et al. 2018],
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 [Protzenko et al. 2020; Swamy et al. 2022; Zinzindohoué et al. 2017], 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 t,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 .
This work is licensed under a Creative Commons Attribution 4.0 International License.arXiv:2503.00404v1 [cs.PL] 1 Mar 2025
Page 2:
2 Andrici et al.
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:
1let prog (lib: (ref(ref int )→cb:(unit→unit))) =
2let secret :ref int =alloc 42in
3let r :ref(ref int ) =alloc (alloc 0)in
4let cb =lib r in
5r:=alloc 1;
6cb();
7assert (!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 cbto the program. The program
allocates a reference r(line 3) and passes it to the
library (line 4). The library can store rand the
reference rpoints 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 rand the reference rpoints to. Between the
initial call into the library and the call into the callback cb(line 6), the program modifies rpointing
it to a newly allocated reference (line 5), and thus this new reference also becomes shared, even if
not passed to cbdirectly—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 𝑟points to each time the callback is called ∗∗)
iter(𝜆r'→r':= 0) ! g;(∗∗writes to all these shared integer references ∗∗)
r:=alloc 0)(∗∗points𝑟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 allreferences, 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.
To our knowledge, no existing technique allows for the sound verification of stateful programs
that can be linked with arbitrary unverified code while sharing dynamically allocated mutable
references with it. A simpler case considered by Georges et al. [2024] (also imaginable for other
separation logic work [Dreyer et al. 2012; Reynolds 2002]) is to have no passing of references to
unverified code (i.e., no dynamic sharing), but this cannot always be ensured, because existing code
cannot always be clearly separated to avoid passing references. While one could consider rewriting
the code to avoid reference passing by wrapping them in closures [Sammler et al. 2020; Swasey et al.
2017], or in some cases to only pass references at abstract types, this would involve refactoring the
unverified code to use a different interface. Other techniques allow passing references by checking
and restoring the properties of the not passed references after a call into unverified code [Agten
Page 3:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★3
et al. 2015; Georges et al. 2024], but this is done dynamically and adds an extra cost—for prog above,
the contents of secret would be checked/restored twice, once for each call into the unverified code.
The solution we propose in this paper allows the sound verification of stateful 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 :
1let safe_prog lib =
2let secret =alloc 42in
3let r =alloc (alloc 0)inlabel_shareable (!r); label_shareable r;
4let cb =lib r in
5let v =alloc 1inlabel_shareable v; r :=v;
6cb();
7assert (!secret == 42)
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 1would not be allowed on line 5 because the fresh
reference returned by alloc 1is 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. Using this solution, one is able to prove the assertion in the example above,
since secret is labeled private . This property is guaranteed even when linked with unverified code.
We have built a secure compilation framework, SecRef★, around the main ideas above and
inspired by previous work for the IO effect [Andrici et al. 2024]. Similarly to this work, we shallowly
embed the source and target language in F★, in our case on top of Labeled References. The only side
effect our languages have is state, and they both have first-order ML-style mutable references. The
difference is that source programs have concrete refinement types and pre- and post-conditions in
their interface, while target programs do not. 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 an 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★has to add dynamic checks, which it does 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 [Ahman et al. 2018] that allows one to verify stateful 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
Page 4:
4 Andrici et al.
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. [2019], 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. [2018]. We also provide a machine-
checked soundness proof in F★for Monotonic State in a different style than the original paper
proof of Ahman et al. [2018]. 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.
Artifact. This paper comes with an F★artifact that includes the full implementation of SecRef★,
the machine-checked proofs, and examples. Some of the examples can be extracted to native OCaml
code (without any monadic representation) via an extension to F★’s extraction rules (Appendix A).
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.
1type linked_list (a:Type ) = |LLNil→linked_list a |LLCons :a→ref(linked_list a )→linked_list a
2type student_hw =ll:ref(linked_list int )→LR(either unit err )
3 ( requires (𝜆h0→witnessed (is_shareable ll )))
4 ( ensures (𝜆h0r h1→modif_only_shareable h 0h1∧same_labels h 0h1∧
5 ( Inr?r∨(sorted ll h 1∧no_cycles ll h 1∧same_values ll h 0h1))))
6let autograder (test:list int ) (hw:student_hw ) (grade :mref (option int )grade_preorder )
7 : LR unit (requires (𝜆h0→is_private h 0grade∧None ? (sel h 0grade ))
8 ( ensures (𝜆h0()h1→Some ? (sel h 1grade )∧
9 same_labels h 0h1∧modif_shareable_and !{grade }h0h1)) =
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 (determine_grade res )
Fig. 1. The illustrative example of a verified autograder. Types are simplified.
Page 5:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★5
2.1 Static verification using Labeled References
In Figure 1 we show how to use Labeled References to verify an autograder.1The autograder takes
as argument a function submitted by a student to solve the homework 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 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-5in 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 exist-
ing 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 Inl), 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 [Ahman et al. 2018; Leino 2010; Reynolds 2002] 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
1F★syntax ˜citesciostar is similar to OCaml ( val,let,match , etc). Binding occurrences btake the form x:tor#x:tfor an
implicit argument. Lambda abstractions are written 𝜆b1...b𝑛→t, whereas b1→...→b𝑛→Cdenotes 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 (v1...v𝑛:t). Refinement types are written b{t}(e.g., x:int{x≥0}represents natural numbers).
Dependent pairs are written as x:t1&t2. 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 t1..tn|}is a special kind of implicit argument, solved by a tactic during elaboration. Type0 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 1t2has two constructors, Inl:(#t1#t2:Type )→t1→either t 1t2andInr:(#t1#t2:Type )→t2→either t 1t2. Expression
Inr?xtests whether xis of the shape Inr y . Binary functions can be made infix by using backticks: x`op`ystands for op x y .
Page 6:
6 Andrici et al.
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 wit-
nessed 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 ris share-
able in a heap h(i.e., is_shareable r h ), one can witness this and get a token witnessed (is_shareable r ),
which can be recalled later, say when the heap is h', to prove that is_shareable r h '.2
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 (line
6), a feature of Monotonic State (denoted using mref), that has a preorder on its stored value, which
is enforced statically. 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.
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.
The type of the new reference-manipulating operations is presented in Figure 2 and they use
three abstract predicates in a way that allows the operations to still be freely sequenced: (1) a global
invariant on the heap (denoted by I), required and guaranteed by all operations; (2) a predicate
2For readers familiar with Separation Logic, this is similar to invariants and their introduction and elimination rules.
Page 7:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★7
type poly_alloc_t (I:heap→Type0 ) (𝜑:ref𝛼→Type0 ) (≼:preorder heap ) =
init:𝛼→MST (ref𝛼) (𝜆h0→I h0∧every mref𝜑init) (𝜆h0r h1→h0≼h1∧I h1∧𝜑r)
type poly_read_t (I:heap→Type0 ) (𝜑:ref𝛼→Type0 ) (≼:preorder heap ) =
r:ref𝛼→MST𝛼(requires (𝜆h0→I h0∧𝜑r)) (ensures (𝜆h0v h1→h0≼h1∧I h1∧every mref𝜑v))
type poly_write_t (I:heap→Type0 ) (𝜑:ref𝛼→Type0 ) (≼:preorder heap ) =
r:ref𝛼→v:𝛼→MST unit (𝜆h0→I h0∧𝜑r∧every mref𝜑v) (𝜆h0_ h1→h0≼h1∧I h1)
Fig. 2. Types of the reference-manipulating operations polymorphic in I,𝜑and≼.
on references (denoted by 𝜑) constraining references stored in the heap by write and alloc, and
also ensured of freshly allocated references returned by alloc and of references gotten from the
heap by read; (3) a preorder on heaps (denoted by ≼) and a guarantee that for all our operations
the heap evolves according to this preorder. In Figure 2 we also use the every mrefcombinator that
takes a predicate on references (in our case 𝜑) and a value of an inductive type, then recursively
decomposes the value by pattern matching. For each reference, it applies the predicate, ensuring
that all reachable references satisfy the given predicate.
We used this representation for instance to write the following unverified homework that sorts
a linked list, which takes as argument the three operations and combines them freely.3
type target_student_hw =I:(heap→Type0 )→𝜑:(ref𝛼→Type0 )→≼:preorder heap→
(∗set of operations that use the abstract predicates ∗)
alloc :poly_alloc_tI𝜑(≼)→read :poly_read_tI𝜑(≼)→write :poly_write_tI𝜑(≼)→
(∗the actual type of the homework ∗)
ll:ref(linked_list int )→
MST (either unit err ) (requires (𝜆h0→I h0∧𝜑ll)) (ensures (𝜆h0r h1→h0≼h1∧I h1∧every mref𝜑r))
let unverified_student_hw :target_student_hw =𝜆my_alloc my_read my_write →
let rec sort (ll:ref(linked_list int )) =
match my_read ll with |LLNil→()
|LLCons x tl→begin
sort tl ;
match my_read tl with |LLNil→()
|LLCons x 'tl'→if x≤x'then ()else(
let new_tl =my_alloc (LLCons x tl ')in
sort new_tl ;
my_write ll (LLCons x 'new_tl ))
end
in sort
The abstract predicates are also used for specifying the homework in the target language, and we
explain how F★shows that the homework satisfies its post-condition, even if it is abstract. The first
conjunct of the post-condition is about the preorder on heaps ≼, which is satisfied because all our 3
operations ensure that the heap evolves according to ≼, which is a reflexive and transitive relation.
The second conjunct about global invariant Iis satisfied because it is required in the pre-condition
oftarget_student_hw , and then every operation requires and ensures this invariant. The third and
last conjunct states that any reference that is returned has to satisfy predicate 𝜑. This conjunct is
satisfied because a reference can be allocated (which ensures 𝜑), read from the heap (which ensures
𝜑), or is received from the outside, which is also guaranteed because of the pre-condition requiring
3We elided the proof of termination, which is needed since for simplicity our work assumes that state is the only side-effect.
Page 8:
8 Andrici et al.
that the input linked list satisfies 𝜑. The pre-condition and the post-condition of target_student_hw
ensure that every reference that crosses the verified-unverified boundary satisfies the predicate 𝜑.
We therefore claim that this is an appropriate representation for stateful unverified code shal-
lowly embedded in F★. To make it even more apparent, in the artifact we also have a syntactic
representation, a small deeply embedded lambda calculus with first-order ML-style references, and
we show a total (back)translation function in F★from any well-typed syntactic lambda-calculus
expression to the shallowly embedded representation with abstract predicates.
Now time for some magic: we show that we can instantiate the types 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 target_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 𝜑with𝜆r→witnessed (is_shareable r ), which
becomes the same pre-condition as in type student_hw . Then, we instantiate the preorder ≼, with
𝜆h0h1→modif_only_shareable h 0h1∧same_labels h 0h1, 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. This is a first step towards bridging the gap
between verified and unverified code, 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 3 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, since, due to the new
specs, they are now specialized for shareable references. For readan interesting interaction happens
between every mref𝜑rand the global invariant to show that whatever was read from the heap is
also shareable. The every mrefcombinator stops when reaching a reference because once it was
established that a reference is shareable, the global invariant offers the guarantee that all references
reachable form this reference are also shareable.
2.3 Higher-order contracts in SecRef★
After the instantiation, an unverified computation of type unverified_student_hw almost has the
type 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 [Findler and Felleisen 2002], 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 [Findler and Felleisen 2002] 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.
Page 9:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★9
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 3 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.
1val generate_nr :int→int→int(∗a pure computation ∗)
2let post =𝜆h0_ h1→modif_shareable_and_encaps h 0h1∧same_labels h 0h1
3let prng (seed:int)
4 : LR(unit→LR int (requires (𝜆_→⊤ )) (ensures post )) (requires (𝜆_→⊤ )) (ensures post ) =
5 let counter :mref int (≤) =alloc 0in label_encapsulated counter ;
6 (𝜆()→counter := !counter + 1;generate_nr seed (!counter ))
Fig. 3. The illustrative example of a pseudo-number generator
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.
Page 10:
10 Andrici et al.
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. [2018], 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 holds in one part of a program, resulting
in a state-independent token witnessing this action, and then use this token to recall that the
predicate still holds at arbitrary later program points.
Ahman et al. [2018] considered a general Monotonic State notion, 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 ⪯heaps enforcing that allocated
references stay allocated forever, and monotonic references preserve their preorders. With this, we
obtain our MST effect, which models first-order4ML-style mutable references.
The interface of MST, presented in Figure 4, 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 ⪯. ML-style references ref a are a special case for
the trivial 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
previous 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, no labels yet).Specifically, for a set sof addresses, modifies s h 0h1holds if any references
contained in h0and not contained in sremain unmodified. Above, !{r}is F★’s syntax for the singleton
set containing the address of r. Notice that the pre-conditions of readand write require the reference
to be contained, yet for simplicity, we often elide this detail from the other sections of the paper.
3.2 MST as a Dijkstra monad with a free-monad-based representation
In the work of Ahman et al. [2018], the MST effect and the operations above were simply assumed and
not given definitions within F★. We improve on this by giving a free-monad-based representation
forMST in F★, from which it can be defined as a Dijkstra monad [Maillard et al. 2019].
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
D, the typeD𝛼𝑤classifies computations that return 𝛼-typed values and satisfy a specification
4Providing a monadic representation that allows storing effectful functions given F★’s predicative, countable hierarchy of
universes is an open research problem, further detailed in §3.2 and §9.
Page 11:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★11
val heap :Type0
val mref :a:Type0→rel:preorder a→Type0
type ref (a:Type0 ) =mref a (trivial_preorder a )
val contains : #a:Type0→#rel:preorder a→heap→mref a rel→Type0
val sel : #a:Type0→#rel:preorder a→h:heap→r:mref a rel {h`contains `r}→a
val heap_write : #a:_→#rel:_→h:heap→r:mref a rel {h`contains `r}→x:a{sel h r `rel`x}→heap
val heap_alloc : #a:Type0→rel:preorder a→heap→a→mref a rel &heap
val addr_of : #a:Type0→#rel:preorder a→mref a rel→erased pos
val next_addr :heap→erased pos
let(⪯)h0h1=∀a rel (r:mref a rel ).h0`contains `r=⇒(h1`contains `r∧(sel h0 r ) `rel` (sel h1 r ))
val alloc : #a:Type→#rel:preorder a→init:a→
MST (mref a rel ) (requires (𝜆h0→⊤ ))
(ensures (𝜆h0r h1→h0⪯h1∧fresh r h 0h1∧modifies !{}h0h1∧
addr_of r ==next_addr h 0))
val read : #a:_→#rel:_→r:mref a rel→MST a (requires (𝜆h0→h0`contains `r))
(ensures (𝜆h0v h1→h0==h1∧v==sel h 1r))
val write : #a:_→#rel:_→r:mref a rel→v:a→
MST unit (requires (𝜆h0→h0`contains `r∧(sel h 0r) `rel`v))
(ensures (𝜆h0()h1→h0⪯h1∧modifies !{r}h0h1∧equal_dom h 0h1))
val witnessed :p:(heap→Type0 )→Type0
let stable_heap_predicate =p:(heap→Type0 ){∀h0h1.p h0∧h0⪯h1=⇒p h1}
val witness :p:stable_heap_predicate →MST unit (requires (𝜆h0→p h0))
(ensures (𝜆h0()h1→h0==h1∧witnessed p ))
val recall :p:stable_heap_predicate →MST unit (requires (𝜆_→witnessed p ))
(ensures (𝜆h0()h1→h0==h1∧p h1))
Fig. 4. Interface of Monotonic State
𝑤:𝑊 𝛼, where𝑊is an aforementioned specification monad. A common way to define a Dijkstra
monadD[Maillard et al. 2019] is to identify (i) a monad 𝑀to represent computations classified
byD, (ii) an ordered monad 𝑊that models specifications for the computations in 𝑀, where the
order formalizes when one specification implies another, and (iii) a monad morphism 𝜃:𝑀→𝑊
that infers for every computation its “most precise” specification. The Dijkstra monad Dis then
defined asD𝛼𝑤=𝑚:𝑀𝛼{𝜃(𝑚)⊑𝑤}, formalizing the idea that D𝛼𝑤classifies computations
𝑚:𝑀𝛼 that satisfy the given specification 𝑤. Below we work out such a Dijkstra monad for MST.
The computational monad. We begin by defining the computational monad as a free monad:5
type mst_repr (a:Type u #a) :Type u #(max 1a) =
|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
5We omit a constructor that is needed in F★to account for partiality coming from pre-conditions [Winterhalter et al. 2022].
Page 12:
12 Andrici et al.
nowitnessed 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 #ainto a Type u #(max 1a), 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. For specifications, we use the monad of weakest pre-conditions:
let mst_w (a:Type ) =wp:((a→heap→Type0 )→(heap→Type0 )){
∀post post '. (∀v h1.post v h 1=⇒post 'v h1)=⇒(∀h0.wp post h 0=⇒wp post 'h0)}
A specification wp:mst_w a is a function that transforms any post-condition post:a→heap→Type0
over return values and final heaps into a pre-condition wp post :heap→Type0 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 h 0=post v h 0, and the bind operation
composes two predicate transformers, as mst_w_bind wp wp 'post h 0=wp(𝜆v h1→wp 'v post h 1)h0.
The order⊑onmst_w is defined so that wp⊑wp 'holds when∀post h 0.wp 'post h 0=⇒wp post h 0.
The monad morphism and the Dijkstra monad. As the final ingredient for defining a
Dijkstra monad, we define a monad morphism 𝜃:mst_repr𝛼→mst_w𝛼by recursion on the tree
structure of mst_repr𝛼. 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 =⇒post ()h)) (𝜆v→𝜃(k r))
|Recall p k→mst_w_bind (𝜆post h→witnessed p∧(p h=⇒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𝜃to their continuations. For instance, the mst_w interpretation of Witness matches exactly the
specification of witness from §3.1 using the correspondence between pre- and post-conditions and
predicate transformers [Maillard et al. 2019]. The same pattern repeats for all the other operations.
The Dijkstra monad is defined by refining mst_repr computations using mst_w predicates via 𝜃:
type mst_dm (a:Type ) (wp:mst_w a ) =m:mst_repr a {𝜃m⊑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 to extend F★with new effects [Rastogi et al. 2021].
effect MSTATE (a:Type ) (w:mst_w a )with {repr =mst_dm ;return =mst_dm_return ; ... }
effect MST (a:Type ) (pre:heap→Type0 ) (post:heap→a→heap→Type0 ) =
MSTATE a (𝜆p h0→pre h 0∧(∀v h1.h0≼h1∧post h 0v h1=⇒p v h 1))
The last effect, MST, is derived as a pre- and post-condition based effect synonym [Maillard et al.
2019], 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
Page 13:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★13
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 𝜃.
3.3 Soundness of the free-monad-based Dijkstra monad for Monotonic State
In the work of Ahman et al. [2018], the MST effect was simply axiomatized in F★, with its computa-
tional interpretation defined and the soundness of its axiomatization proved, both on paper. Above
we defined such a computational interpretation in F★and now give a soundness proof that the
specifications computed with 𝜃from the free monad representation are computationally satisfied.
A soundness proof is desirable because choosing a specification for the free monad operations in 𝜃
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 able to vary the
relevance of witnessed tokens, we consider a variant of 𝜃, written𝜃w, which is parametric in the
tokens w: (heap→Type0 )→Type0 used in the specifications of Witness and Recall , but is otherwise
defined like 𝜃. 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𝛼had to
originate from an earlier call to witness p inm, which is a property of closed programs.
let rec witnessed_before (preds :set stable_heap_predicate ) (m:mst_repr𝛼) :Type0 =
match m with |Return _→⊤ |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 mas being
verified to satisfy a specification wp, but we instantiate the wparameter of 𝜃wwith the trivial tokens
witnessed_trivial p =⊤, 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 postholds 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 for which the
witnessed predicates are stable. 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 hp 0)∧(snd hp 0) `witnessed_before `m})
: (r:𝛼&hp1:heap_w_preds {post r (fst hp 1)})
=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 hp 0)init in
run_mst_with_preds (𝜃witnessed_trivial (k r)) (k r)post (h1,snd hp 0)
|Witness p k→let lp = (snd hp 0) `union ` (singleton p )in
run_mst_with_preds (𝜃witnessed_trivial (k())) (k())post (fst hp 0,lp)
|Recall p k→run_mst_with_preds (𝜃witnessed_trivial (k())) (k())post hp 0
let run_mst (wp:state_wp𝛼) (m:mst_repr𝛼{𝜃witnessed_trivial m⊑wp∧empty `witnessed_before `m})
(post:(𝛼→heap→Type0 )) :h0:heap {wp post h 0}→r:𝛼&h1:heap {post r h 1}
Page 14:
14 Andrici et al.
=𝜆h0→let(r,hp1) =run_mst_with_preds wp m post (h0,empty )in(r,fst hp 1)
Using run_mst , we define the soundness theorem which states that if a closed program mis
well-typed against a specification that uses abstract witnessed tokens (modelled using universal
quantification), then for any post-condition postand initial heap h0, if the weakest pre-condition
wp post holds in h0, the post-condition holds for the return value vin the final heap h1.
let soundness (m:mst_repr𝛼) (wp:state_wp𝛼)
:Lemma (requires ((∀w.𝜃wm⊑wp)∧empty `witnessed_before `m))
(ensures (∀post h 0.wp post h 0=⇒(let(v,h1) =run_mst wp m post h 0in post v h 1))) = ()
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 refer-
ence either with shareable orencapsulated . Labeling a reference with shareable orencapsulated 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→⊤ |_,_→⊥
To track references’ labels and how they evolve in programs, we assume a ghost top-level
monotonic reference that stores a map from the addresses of references to their labels
type label_map_t =erased (mref (pos→erased label ) (𝜆m0m1→∀r. (m0r)≼lab(m1r)))
assume val label_map :label_map_t
The heap relation⪯defined in Figure 4 from §3 ensures that label_map can only evolve according
to≼lab, which in turn is what makes being shareable orencapsulated 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 amref-parameterised stable heap predicate. In contrast, as private
references can get relabeled with other labels, being private isnota stable property of the heap:
let is_private_addr :pos→heap→Type0 =𝜆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 , so as 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 orencapsulated , or both kinds of references:
Page 15:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★15
let modif_only_shareable_and_encaps (h0:heap ) (h1:heap ) :Type0 =∀a rel (r:mref a rel ).
(¬(eq_addrs r label_map )∧¬(is_shareable r h 0∨is_encaps r h 0))=⇒sel h 0r==sel h 1r
let modif_shareable_and (h0:heap ) (h1:heap ) (s:set nat ) :Type0 =∀a rel (r:mref a rel ).
(¬(eq_addrs r label_map )∧¬(is_shareable r h 0∨(addr_of r ) `mem `s))=⇒sel h 0r==sel h 1r
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 either base types, sums or products of them, other references storing
values of such types, and data structures built from them, collectively known in the literature as
full ground types [Kammar et al. 2017; Murawski and Tzevelekos 2018]. 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
|SLList :full_ground_typ→full_ground_typ
and comes with the evident recursive inclusion to_Type :full_ground_typ→Type0 into Type0 types.
It is important to emphasize that this deep embedding is only used for stating the global invariant
about shareable references and to help with proofs about its preservation, but it does not limit
the capacity of the heap to store values of more general types in universe Type0 (recall Figure 4).
Only certain operations (e.g., label_shareable in §4.3) need their type arguments to be given as
full_ground_typ instead of Type0 , so as to help F★with proving that the global invariant is preserved.
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 rec forall_refs (pred:mref_predicate ) (#t:full_ground_typ ) (x:to_Type t ) :Type0 =
let rcall #t x=forall_refs pred #t x in
match t with |SUnit |SInt |SBool→⊤
|SSum t 1t2→match x with |Inl x '→rcall x '|Inr x '→rcall x '
|SPair t 1t2→rcall (fst x)∧rcall (snd x )
|SRef t '→pred x
|SLList t '→match x with |LLNil→⊤ |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_ground_typ ) (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 rpoints to a value (sel h r) that contains only shareable references.
Page 16:
16 Andrici et al.
4.3 The LReffect
We define the Labeled References effect LRon 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 LReffect 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, LRis defined in F★as follows:
effect LR (a:Type )pre post =MST a (requires (𝜆h0→lr_inv h 0∧pre h 0))
(ensures (𝜆h0r h1→lr_inv h 1∧post h 0r h1))
By providing the MST operations we discussed in §3 with suitable stronger pre- and post-
conditions, we can lift them to the LReffect. For allocation, the LRoperation lr_alloc #a#rel init addi-
tionally requires that if the type ahappens to be a full_ground_typ , then every reference contained
in the initial value inithas 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 (𝜆h0→∀t.to_Type t ==a=⇒forall_refs_heap contains_pred h 0#t init ))
(ensures (𝜆h0r h1→alloc_post #a#rel init h 0r h1∧is_private r h 1∧becomes_shareable !{}h0h1))
The specification of LR’slr_read operation remains the same as for MST’sread (see Figure 4). 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 ahappens to be a full_ground_typ ,
then every reference contained in vhas to be contained in the heap, and that if rhappens to be a
shareable reference, then every reference contained in vhas 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 (𝜆h0→write_pre #a#rel r v∧¬(eq_addrs r label_map )∧
(∀t.to_Type t ==a=⇒forall_refs_heap contains_pred h 0#t v∧
(is_shareable r h 0=⇒forall_refs_heap is_shareable h 0#t v))))
(ensures (𝜆h0()h1→write_post r v h 0()h1∧becomes_shareable !{}h0h1))
Page 17:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★17
Similarly to reading from a reference, witnessing and recalling stable predicates also retain the
exact pre- and post-conditions as listed in Figure 4, 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 LReffect comes with two important
additional operations, which allow private references to be relabeled as shareable orencapsulated .
val label_shareable (#t:full_ground_typ ) (r:ref(to_Type t )) :LR unit
(requires (𝜆h0→h0`contains `r∧is_private r h 0∧forall_refs_heap is_shareable h 0(sel h 0r)))
(ensures (𝜆h0()h1→equal_dom h 0h1∧modifies !{label_map }h0h1∧
is_private (label_map )h1∧becomes_shareable !{sr}h0h1))
val label_encapsulated (#a:Type ) (#rel:preorder a ) (r:mref a rel ) :LR unit
(requires (𝜆h0→h0`contains `r∧is_private r h 0∧¬(eq_addrs r label_map )))
(ensures (𝜆h0()h1→equal_dom h 0h1∧modifies !{label_map }h0h1∧
is_private (label_map )h1∧becomes_encapsulated !{r}h0h1))
Both operations can be called with private references contained in the heap, with label_shareable re-
quiring that the reference rhas to store full_ground_typ -values (this helps to prove that label_shareable
preserves the global invariant, as noted in §4.2), that rhas a trivial preorder (via the type refof
non-monotonic references, see Figure 4), and that any references rpoints to have 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 rand label_map being different.
These operations are defined by appropriately modifying the ghost state storing the labeling.
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. 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 5 the type class poly_iface , parameterised 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 the base
types unit,intand bool, and for pairs, sums, option, list and arrow types, as well as for references
and for linked lists. In Figure 5, we show the most interesting instances. 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 poly_iface class. Also notice that poly_iface applies the
ideas from §2.2 so that it can be used to describe higher-order interfaces as well.
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
Page 18:
18 Andrici et al.
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 :threep ) :poly_iface preds int = {wt=every_mref_tc_int }
instance poly_iface_sum (preds :threep )t1 t2 {|poly_iface preds t1 |} {|poly_iface preds t2 |}
:poly_iface preds (either t1 t2 ) = { wt=every_mref_tc_sum t1 t2 }
instance poly_iface_ref (preds :threep ) (t_emb :full_ground_typ ) :poly_iface preds (ref(to_Type t_emb ))
= {wt=every_mref_tc_ref t1 #(full_ground_typ_is_every_mref_tc t_emb ) }
instance poly_iface_arrow ((I,𝜑,≼):threep )t1 t2 {|c1:poly_iface preds t1 |} {|c2:poly_iface preds t2 |}
:poly_iface preds (x:t1→MST t2 (requires (𝜆h0→I h0∧c1.wt.every mrefx𝜑))
(ensures (𝜆h0r h1→I h1∧h0≼h1∧c2.wt.every mref𝜑r)))
= {wt=every_mref_tc_arrow t1 t2 _ _ }
Fig. 5. Showing the polymorphic interface implemented with type class poly_iface.
polymorphism (§2.2), our higher-order contracts have to be enforced on functions under polymor-
phism as well [Andrici et al. 2024], 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 andimport are implemented as fields of two type classes, named exportable_from
and importable_to . For instance, exportable_from styp carries an intermediate type ityptogether with
a function styp→itypthat is shown to preserve the every mrefcombinator. Its dual, importable_to styp
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 parameterised 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 andimport 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.
class 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,
theexport function for option a when a is itself exportable will map theexport 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 fof source type
a→MST (either b err )pre post to a function of the intermediate type a'→MST (either b 'err)pre 'post ',
Page 19:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★19
where a'and b'are the intermediate counterparts of aand b, and pre 'and post 'are the pre- and post-
condition that appear in poly_iface_arrow in Figure 5. For this, we need an import function ( a'→a)
for type aand an export function ( b→b') for type b, which we then compose with f. To be able to
callf, we have to ensure that preholds, 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:
check :x:a→MST (either unit err ) (requires (pre 'x)) (ensures (𝜆h0r h1→h0==h1∧(Inl?r=⇒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 fsatisfies the following property: ∀x h0r h1.post x h 0r h1=⇒post 'h0r h1.
One detail that we omitted is that pre 'and post 'are polymorphic in the type of xand r, compared to
preand postthat use the types aand b. Therefore, because we call import and export , we also have
to prove that pre 'x=⇒pre '(import x )and post 'h0r h1=⇒post 'h0(export r )h1, 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 fof the intermediate type
x:a'→MST (either b 'err)pre 'post 'to the source type x:a→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 atoa', call the function, and import the output from b'tob. To be
able to call the function f, we need to enforce pre 'using pre, hence we only provide an instance
under the assumption ∀x h0.pre x h 0=⇒pre 'x h0. Similarly, once the function is run, we only know
that post 'is verified, so we also require ∀x h0e h1.pre x h 0∧post 'h0(Inr e )h1=⇒post x h 0(Inr e )h1,
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 [Findler and Felleisen 2002], see select_check [Andrici et al. 2024] below:
type cb_check a b {|every_mref_tc b |}pre post x eh =
r:b→MST (either unit err ) (𝜆h1→post 'eh r h 1) (𝜆h1rck h 1'→h1==h1'∧(Inl?rck=⇒post x eh r h 1))
select_check :x:a→MST (eh:erased heap {pre x eh } &cb_check a (either b err )pre post x eh )
(requires (pre x )) (ensures (𝜆h0 r h1→reveal (dfst r ) == h0∧h0==h1))
A stateful contract is first run before calling fto read from the heap information necessary to
enforce the post-condition, which it can store in the closure, and then the callback of the contract is
run after freturns to verify the post-condition post, or return an error otherwise. The same_values
predicate from the autograder example (Figure 1) is enforced by SecRef★using a stateful contract.
6 SECREF★: FORMALLY SECURE COMPILATION FRAMEWORK
In this section we present the formalization of SecRef★(Figure 6). The formalization is mechanized
in F★and instantiates the compiler model presented by Abate et al. [2019] with source and target
languages that are shallowly embedded in the style of Andrici et al. [2024]. 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 present compilation and back-translation (§6.4), and how we prove soundness and RrHP (§6.5).
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.5).
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
Page 20:
20 Andrici et al.
letI𝑐=lr_inv (∗from §4.3. The three concrete predicates, defined as in §2.2.∗)
let𝜑𝑐=𝜆r→witnessed (is_contained r )∧witnessed (is_shareable r )
let≼𝑐=𝜆h0h1→modif_shareable_and_encaps h 0h1∧same_labels h 0h1
type interface𝑆= {
ctype :threep→Type ;
specs_of_ctype :threep→spec_tree threep ;
hocs :hoc_tree (specs_of_ctype (I𝑐,𝜑𝑐,≼𝑐));
imp_ctype :preds :threep→safe_importable_to preds (ctype preds ) (specs_of_ctype preds );
𝜓:heap→int→heap→Type0 }
type ctx𝑆I𝑆=I𝑆.ctype (I𝑐,𝜑𝑐,≼𝑐)
type prog𝑆I𝑆=I𝑆.ctype (I𝑐,𝜑𝑐,≼𝑐)→LR int⊤I𝑆.𝜓
type whole𝑆=𝜓:post_cond & (unit→LR int⊤𝜓)
let link𝑆#I𝑆(P:prog𝑆I𝑆) (C:ctx𝑆I𝑆) = (| I𝑆.𝜓,𝜆()→P C|)(∗∗denoted by𝐶[𝑃]∗∗)
type interface𝑇= {
ctype :threep→Type ;
interm_ctype :preds :threep→poly_iface preds (ctype preds ); }
type ctx𝑇I𝑇=I:_→𝜑:_→≼:_→
poly_alloc_tI𝜑(≼)→poly_read_tI𝜑(≼)→poly_write_tI𝜑(≼)→I𝑇.ctype (I,𝜑,≼)
type prog𝑇I𝑇=I𝑇.ctype (I𝑐,𝜑𝑐,≼𝑐)→LR int⊤⊤
type whole𝑇=unit→LR int⊤⊤
let link𝑇#I𝑇(P:prog𝑇I𝑇) (C:ctx𝑇I𝑇) =
𝜆()→P(CI𝑐𝜑𝑐(≼𝑐)ctx_alloc ctx_read ctx_write )(∗∗denoted by𝐶[𝑃]∗∗)
let compile_interface (I𝑆:interface𝑆) :interface𝑇= {(∗∗denoted by𝐼𝑆↓∗∗)
ctype = (𝜆preds→(I𝑆.imp_ctype preds ).ityp);
interm_ctype = (𝜆preds→(I𝑆.imp_ctype preds ).c_ityp ); }
let compile_prog #I𝑆(P:prog𝑆I𝑆) :prog𝑇(I𝑆↓) =(∗∗denoted by𝑃↓∗∗)
𝜆C→P((I𝑆.imp_ctype (I𝑐,𝜑𝑐,≼𝑐)).safe_import C I𝑆.hocs )
let back_translate_ctx #I𝑆(C:ctx𝑇I𝑆↓) :ctx𝑆I𝑆=(∗∗denoted by𝐶𝑇↑∗∗)
(I𝑆.imp_ctype (I𝑐,𝜑𝑐,≼𝑐)).safe_import (C(I𝑐,𝜑𝑐,≼𝑐))I𝑆.hocs
Fig. 6. Secure compilation framework. Idealized mathematical notation. Type threep is presented in Figure 5.
Types poly_alloc_t, poly_read_t, and poly_write_t are presented in Figure 2.
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𝑆, which contains a type ( ctype ), a type class constraint on this type ( imp_ctype ), and a
post-condition 𝜓. 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 andhocs 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𝑆) is a computation in the monadic
Page 21:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★21
effect LRthat takes as argument a value of type ctype instantiated with the concrete predicates,
returns an integer, and ensures the post-condition 𝜓. The representation of source contexts ( ctx𝑆) is
just a value of type ctype instantiated with the concrete predicates. Source linking ( link𝑆) is then
defined just as function application. A whole source program is a dependent pair between a post-
condition and a computation in effect LRfrom unit to integer that guarantees the post-condition.
The type class constraint imp_ctype 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_ctype 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𝑇) 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𝑇) use the representation from §2.2. The type ctype in the target interface (of type
interface𝑇), now is constrained with the poly_iface type class from §5.1.
A partial target program (see prog𝑇) 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 [Andrici
et al. 2024]. This can be seen in the definition of target linking ( link𝑇), it instantiates the target
context with the concrete predicates I𝑐,𝜑𝑐, and≼𝑐, 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𝑇. 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 LReffect, 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_sem =heap→state→heap→Type0
let(⊆) (s1s2:state_sem ) =∀h0r h1.s1h0r h1=⇒s2h0r h1
To define the semantics of whole programs, we must first reveal the monadic representation of LR
using the reify construct provided by F★[Rastogi et al. 2021]. We define the semantics function beh
by adapting the monad morphism 𝜃from §3.2 [Andrici et al. 2024; Maillard et al. 2019].
let beh_mst (m:mst_repr int ) :state_sem =𝜆h0r h1→∀p.𝜃m p h 0=⇒p r h 1
Page 22:
22 Andrici et al.
let beh (W:unit→LR int⊤⊤) =beh_mst (reify (W()))
Since we use 𝜃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 𝜓into an extrinsic property:
Theorem 6.1 (Soundness of whole source programs). ∀(𝜓,𝑊):whole𝑆.beh(𝑊)⊆𝜓
Proof sketch. For a whole source program, we know its underneath monadic representation
ism:(mst_repr int ){𝜃m⊑(𝜆p h0→∀r h1.𝜓h0r h1=⇒p r h 1)}(§3.2), which implies that beh m⊆𝜓.□
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.
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 Trusted
Computing Base (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 abstractions
provided by modules. We also assume that assume is not used by the program and context.
6.4 Compilation + Target Linking = Back-translation + Source Linking
We define the compilation of partial programs ( compile_prog in Figure 6, denoted as 𝑃↓) as wrapping
the partial source program in a new function of type prog𝑇. 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 now introduce the back-translation (the dual of compilation, denoted by 𝐶↑). It is used in the
proofs of soundness and Robust Relational Hyperproperty Preservation (§6.5). Back-translation
takes a target context and produces a source context. We define it as instantiating the context
and then adding the higher-order contracts. One immediately observes that this is exactly what
happens during compilation plus target linking, which can be proved as the next equality.
Theorem 6.2 (Syntactic inversion law). ∀𝐼𝑆.∀𝐶𝑇:ctx𝑇𝐼𝑆↓.∀𝑃:prog𝑆𝐼𝑆.𝐶𝑇[𝑃↓]=𝐶𝑇↑[𝑃]
Proof sketch. Follows by unfolding definitions. □
Theorem 6.2 is one of the main contributions of Andrici et al. [2024], which we also manage
to successfully prove in our setting. The key to such a strong result is the carefully designed
compilation model. We build on the model presented by Andrici et al. [2024] for IO programs and
show how to build a secure compilation framework for stateful programs. The novel additions
include dealing with references that cross the verified-unverified boundary by taking advantage of
the monotonicity of LR, like𝜑in the representation for unverified code and how 𝜑𝑐uses witnessed .
6.5 Soundness and Robust Relational Hyperproperty Preservation (RrHP)
Andrici et al. [2024] show how to use Theorem 6.2 to prove soundness and Robust Relational
Hyperproperty Preservation in their setting for IO. We prove the criteria for our setting with state
by following their proofs. In particular, SecRef★allows one to statically verify that a partial program
satisfies a post-condition 𝜓. 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 𝜓(when the partial program has initial control).
Theorem 6.3 (Soundness). ∀𝐼𝑆.∀𝑃:prog𝑆𝐼𝑆.∀𝐶𝑇:ctx𝑇𝐼𝑆↓.beh(𝐶𝑇[𝑃↓])⊆𝐼𝑆.𝜓
Page 23:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★23
Proof sketch. We rewrite the goal with Theorem 6.2 to 𝐶𝑇[𝑃↓]=𝐶𝑇↑[𝑃]. Now,𝐶𝑇↑[𝑃]
builds a whole source program and we can apply Theorem 6.1. □
We prove that SecRef★robustly preserves relational hyperproperties. Abate et al. [2019] 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)).
∀𝐼𝑆.∀𝐶𝑇:ctx𝑇𝐼𝑆↓.∃𝐶𝑆:ctx𝑆𝐼𝑆.∀𝑃:prog𝑆𝐼𝑆.beh(𝐶𝑇[𝑃↓])=beh(𝐶𝑆[𝑃])
Proof sketch. The proof follows by back-translating the target context ( 𝐶𝑇↑) and using it to
instantiate the existential of a source context, after which we conclude with Theorem 6.2. □
Finally, we have proved that SecRef★also satisfies RrHP (Theorem 6.4) in the dual setting:
when the context has initial control. We mention it briefly because the proofs are similar, since
Theorem 6.2 again holds. In this case, instead of soundness, we proved the dual of soundness [Andrici
et al. 2024], a less interesting criterion stating that the resulting whole target program modifies only
shareable references. We also proved RrHP in the setting where target contexts are represented
with typed syntactic expressions [Andrici et al. 2024] 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 ( ctx𝑇). 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. [2017] 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 (#t:full_ground_typ ) (r:ref(to_Type t )) (a:Type0 ) =
|Return :a→atree r a
|Yield :continuation r a→atree r a
and continuation (#t:full_ground_typ ) (r:ref(to_Type t ))a=
unit→LR(atree r a ) (requires (𝜆h0→is_shareable r h 0)) (ensures (𝜆h0_ h1→h0≼𝑐h1)
These trees share a global reference r, which can be accessed by any of the involved stateful
computations. For the continuations, we assume that they represent unverified code, and thus
they have a corresponding specification: the pre-condition requires the reference rto be shareable ,
while the post-condition ensures that the unverified code only modifies shareable (orencapsulated )
references using the relation ≼𝑐from Figure 5. As before, we elide the reference containment
requirements from pre- and post-conditions, as well as 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 fairness
property that the execution history needs to satisfy, and also ensure that both the next thread and
inactive counts are within valid ranges. The argument kis used to keep track of the number of
threads that was passed to the scheduler on initialization. In detail, we define it as follows:
Page 24:
24 Andrici et al.
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.1`prefix_of `v'.1
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 #t(r:ref(to_Type t )) (tasks :list(continuation r unit )) (counter :counter_t (length tasks ))
:LR unit (requires (𝜆h0→is_private counter h 0∧is_shareable r h 0))
(ensures (𝜆h0_ h1→modif_shareable_encaps_and h 0h1!{counter }∧gets_shared empty h 0h1))
It takes a list of tasks to be executed (represented as unit-typed continuations), the global shared
reference r, 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. 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 #t(v:to_Type t ) (tasks :list(r:ref(to_Type t )→continuation r unit ){length tasks > 0}) : LR(to_Type t )
(requires (𝜆h0→forall_refs_heap contains_pred h0 v ∧forall_refs_heap is_shared h0 v ))
(ensures (𝜆h0_ h1→h0≼𝑐h1)) =
let counter :counter_t (length tasks ) =alloc (| [], 0, 0 |) in
let r =alloc v in label_shareable r ;
let tasks =map (𝜆(f: (s:ref(to_Type t ))→continuation s 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’s allocated state is the initial one: empty history, the next task is the first one in the
task list, and the number of inactive tasks is zero. As a final remark, we note that the function run
can also be called by unverified code to cooperatively execute other unverified code. Importantly,
runhas the exact same post-condition as unverified code (as used in the continuations).
8 RELATED WORK
We already mentioned in the introduction a list of techniques that allow verification of a stateful
program, however, they do not support sound verification of a program that can then be linked
with arbitrary unverified code with which it dynamically shares mutable references.
Secure Compilation. The approaches of Agten et al. [2015] and Strydonck et al. [2021] support
secure compilation of formally verified stateful programs against unverified contexts. Agten et al.
[2015] securely compile modules verified with separation logic [Reynolds 2002], 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
Page 25:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★25
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. [2021] 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 [Georges et al. 2021].
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 [Watson et al.
2020], but this required us to overcome the challenge of unverified contexts that stash references.
Gradual verification is a combination of static and dynamic verification proposed by Bader
et al. [2018]. 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. [2025] 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. As future work, one could try to extend SecRef★so that it statically analyzes unverified
code and discards the contracts using soft contract verification [Nguyen et al. 2014, 2018].
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 [Maillard et al. 2019; Silver and Zdancewic 2021]). 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 [Letan and Régis-Gianas 2020; Maillard et al. 2020; Xia et al. 2020; Yoon et al. 2022].
Page 26:
26 Andrici et al.
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 get
closer to this goal: (1) Modeling higher-order store for effectful functions around F★’s predicative,
countable hierarchy of universes. Koronkevich and Bowman [2024] 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 [Landin 1964]). (2) Modeling more of the effects of OCaml by extending the repre-
sentation 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 [Andrici et al.
2024], how other effects would impact soundness and security is an open question. (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 (to go
from the shallow embedding to a deep embedding), and verified erasure specialized for a Dijkstra
monad. For verified erasure, Forster et al. [2024] 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 [Sozeau et al. 2020], 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 [Fromherz et al. 2021; Swamy et al. 2020, 2024].
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 RUNNING SECREF★PROGRAMS BY EXTRACTING TO OCAML
As the MST effect is marked reifiable , F★can automatically extract effectful programs to OCaml by
using the reified representation of the program (i.e. the free monad is §3.2). However, we wanted
native extraction in order to be more efficient and more realistic.
To extract our custom effects to native operations, we make use of existing support in F★to
extend its extraction rules. Essentially, we add rules that recognize the operations of the MST effect
(alloc,read,write ) and translate them directly to their native OCaml counterparts, bypassing the
monadic representation. This is implemented in a standalone F★module that uses compiler-internal
APIs in order to register the new rules. This module is later built into a dynamic object (an OCaml
cmxs file) and loaded dynamically by F★when extraction is to be performed.
The original monadic representation and its operations are marked with the ‘ noextract ’ qualifier,
to make sure they do not appear in extracted code, and only the primitive operations are used.
It was necessary to write a small patch to F★to allow this. The current F★rejects trying to use
native extraction rules for reifiable effects. Our patch allow this, and uses the native representation
for extraction purposes. The patch applies cleanly over the latest F★release (v2025.02.17) and is
included in the supplementary material.
B ADDITIONAL EXAMPLE: GUESSING GAME
To showcase the use of encapsulated references, in Figure 7 we present another example of a
verified program that plays the “guess the number I’m thinking of” with an unverified player. The
Page 27:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★27
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).
1type cmp = |LT|GT|EQ
2let post =𝜆h0_ h1→modif_shareable_and_encaps h 0h1∧same_labels h 0h1
3type player_t = (l:int ∗r:int ∗(guess :int→LR cmp (𝜆_→⊤ )post))→LR int (𝜆_→l<r)post
4let play_guess (l pick r :int) (player :player_t ) :LR(bool ∗list int ) (𝜆_→l<pick∧pick <r)post =
5let guesses :mref (list int ) (𝜆l l'→l`prefix_of `l') =alloc []in label_encapsulate guesses ;
6let final_guess =
7 player (𝜆x→guesses :=guesses @ [x];if pick =x then EQ else if pick <x then LT else GT )in
8guesses :=guesses @ [final_guess ];
9if pick =final_guess then (true, !guesses )
10 else(false , !guesses )
Fig. 7. The illustrative example of a function that plays "Guess the number I’m thinking of"
REFERENCES
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.
P. Agten, B. Jacobs, and F. Piessens. Sound modular verification of C code executing in an unverified context. POPL . 2015.
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.
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.
A. W. Appel. Modular verification for computer security. CSF. 2016.
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.
J. Bader, J. Aldrich, and É. Tanter. Gradual program verification. VMCAI . 2018.
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.
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.
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.
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.
D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. J.
Funct. Program. , 22(4-5):477–528, 2012.
R. B. Findler and M. Felleisen. Contracts for higher-order functions. ICFP . 2002.
Y. Forster, M. Sozeau, and N. Tabareau. Verified extraction from Coq to OCaml. Proc. ACM Program. Lang. , 8(PLDI):52–75,
2024.
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.
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.
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.
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.
Page 28:
28 Andrici et al.
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.
S. Ho, J. Protzenko, A. Bichhawat, and K. Bhargavan. Noise*: A library of verified high-performance secure channel protocol
implementations. IEEE S&P . 2022.
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.
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.
P. Koronkevich and W. J. Bowman. Type universes as allocation effects. CoRR , abs/2407.06473, 2024.
P. J. Landin. The mechanical evaluation of expressions. The Computer Journal , 6(4):308–320, 1964.
K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. LPAR . 2010.
X. Leroy. Formal verification of a realistic compiler. CACM , 52(7):107–115, 2009.
T. Letan and Y. Régis-Gianas. FreeSpec: specifying, verifying, and executing impure computations in Coq. CPP. 2020.
J. Li, A. Lattuada, Y. Zhou, J. Cameron, J. Howell, B. Parno, and C. Hawblitzel. Linear types for large-scale systems verification.
OOPSLA , 2022.
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.
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.
A. S. Murawski and N. Tzevelekos. Algorithmic games for full ground references. Formal Methods Syst. Des. , 52(3):277–314,
2018.
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.
P. C. Nguyen, S. Tobin-Hochstadt, and D. V. Horn. Soft contract verification. ICFP . 2014.
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.
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.
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.
A. Rastogi, G. Martínez, A. Fromherz, T. Ramananandro, and N. Swamy. Programming and proving with indexed effects,
2021.
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.
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.
L. Silver and S. Zdancewic. Dijkstra monads forever: termination-sensitive specifications for interaction trees. Proc. ACM
Program. Lang. , 5(POPL):1–28, 2021.
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.
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.
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.
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.
N. Swamy, A. Rastogi, G. Martínez, M. Frisella, T. Dardinier, G. Ebner, and T. Ramananandro. PulseCore: A dependently
typed stratified separation logic, 2024.
D. Swasey, D. Garg, and D. Dreyer. Robust and compositional verification of object capability patterns. PACMPL , 1(OOPSLA):
89:1–89:26, 2017.
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
Page 29:
SecRef★: Securely Sharing Mutable References Between Verified and Unverified Code in F★29
Cambridge, Computer Laboratory, 2020.
T. Winterhalter, C.-C. Andrici, C. Hriţcu, K. Maillard, G. Martínez, and E. Rivas. Partial Dijkstra Monads for all. TYPES, 2022.
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.
I. Yoon, Y. Zakowski, and S. Zdancewic. Formal reasoning about layered monadic interpreters. Proc. ACM Program. Lang. , 6
(ICFP), 2022.
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.
J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche. HACL*: A verified modern cryptographic library. CCS.
2017.
