# A Categorical Approach to Secure Compilation

Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

► To cite this version:

Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens. A Categorical Approach to Secure Compilation. 15th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2020, Dublin, Ireland. pp.155-179, 10.1007/978-3-030-57201-3_9. hal-03232345

HAL Id: hal-03232345

https://inria.hal.science/hal-03232345

Submitted on 21 May 2021

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# A categorical approach to secure compilation

Stelios Tsampas¹, Andreas Nuyts¹, Dominique Devriese
(Corresponding)², and Frank Piessens¹

¹ KU Leuven, Leuven, Belgium name.surname@cs.kuleuven.be

² Vrije Universiteit Brussel, Brussels, Belgium dominique.devriese@vub.be

**Abstract.** We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive laws can potentially be a viable alternative for compiler security instead of full abstraction, which is the preservation and reflection of contextual equivalence. To that end, we also make use of the well-behavedness properties of distributive laws to construct a categorical argument for the contextual connotations of bisimilarity.

**Keywords:** Secure compilation · Distributive laws · Structural Operational Semantics

## 1 Introduction

As a field, secure compilation is the study of compilers that formally preserve abstractions across languages. Its roots can be tracked back to the seminal observation made by Abadi [1], namely that compilers which do not protect high-level abstractions against low-level contexts might introduce security vulnerabilities. But it was the advent of secure architectures like the Intel SGX [15] and an ever-increasing need for computer security that motivated researchers to eventually work on formally proving compiler security.

The most prominent [16, 18, 49, 35, 37, 32, 45] formal criterion for compiler security is full abstraction: A compiler is fully abstract if it preserves and reflects Morris-style contextual equivalence [31], i.e. indistinguishability under all program contexts, which are usually defined as programs with a hole. The intuition is that contexts represent the ways an attacker can interact with programs and so full abstraction ensures that such interactions are consistent between languages.

Full abstraction is arguably a strong and useful property but it is also notoriously hard to prove for realistic compilers, mainly due to the inherent challenge of having to reason directly about program contexts [37, 18, 9, 24]. There is thus a need for better formal methods, a view shared in the scientific community [10, 33]. While recent work has proposed generalizing from full abstraction towards the so-called robust properties [36, 2], the main challenge of quantifying over program contexts remains, which manifests when directly translating target contexts to the source (back-translation). Other techniques, such as trace semantics [35] or logical relations [17], require complex correctness and completeness proofs w.r.t. contextual equivalence in order to be applicable.
In this paper we introduce a novel, categorical approach to secure compilation. The approach has two main components: the elegant representation of Structural Operational Semantics (SOS) [38] using category-theoretic distributive laws [48]<fnref n="3" /> and also maps of distributive laws [40, 50, 27] as secure compilers that preserve bisimilarity. Our method aims to be unifying, in that there is a general, shared formalism for operational semantics, and simplifying, in that the formal criterion for compiler security, the coherence criterion for maps of distributive laws, is straightforward and relatively easy to prove.

The starting point of our contributions is an abstract proof on how coalgebraic bisimilarity under distributive laws holds contextual meaning in a manner similar to contextual equivalence (Section 4.3). We argue that this justifies the use of the coherence criterion for testing compiler security as long as bisimilarity adequately captures the underlying threat model. We then demonstrate the effectiveness of our approach by appeal to four examples of compiler (in)security. The examples model classic, non-trivial problems in secure compilation:

- An example of an extra processor register in the target language that conveys additional information about computations (Section 5).

- A datatype mismatch between the type of variable (Section 6).

- The introduction of illicit control flow in the target language (Section 7)

- A case of incorrect local state encapsulation (Section 8).

For each of these examples we present an insecure compiler that fails the coherence criterion, then introduce security primitives in the target language and construct a secure compiler that respects it. We also examine how bisimilarity can be both a blessing and a curse as its strictness and rigidity sometimes lead to relatively contrived solutions. Finally, in Section 9, we discuss related work and point out potential avenues for further development of the underlying theory.

**On the structure and style of the paper** This work is presented mainly in the style of programming language semantics but its ideas are deeply rooted in category theory. We follow an “on-demand” approach when it comes to important categorical concepts: we begin the first example by introducing the base language used throughout the paper, *While*, and gradually present distributive laws when required. From the second example in Section 6 and on, we relax the categorical notation and mostly remain within the style of PL semantics.

# 2 The basic *While* language

## 2.1 Syntax and operational semantics

We begin by defining the set of arithmetic expressions.

$$ \langle expr \rangle ::= lit N | var N | \langle expr \rangle \langle bin \rangle \langle expr \rangle | \langle un \rangle \langle expr \rangle $$

<footnote n="3">³ The authors use the term “Mathematical Operational Semantics”. The term “Coalgebraic Semantics” is also used in the literature.</footnote>
The constructors are respectively literals, a dereference operator var, binary arithmetic operations as well as unary operations. We let S be the set of lists of natural numbers. The role of S is that of a run-time store whose entries are referred by their index on the list using constructor var. We define function eval : S × E → N inductively on the structure of expressions.

**Definition 1 (Evaluation of expressions in While).**

$$ \mathit{eval\ store} (\mathit{lit} \ n) = n $$

$$ \mathit{eval\ store} (\mathit{var} \ l) = \mathit{get\ store} \ l $$

$$ \mathit{eval\ store} (e_1 \ b \ e_2) = (\mathit{eval\ store} \ e_1) [[b]] (\mathit{eval\ store} \ e_2) $$

$$ \mathit{eval\ store} (u \ e) = [[u]] (\mathit{eval\ store} \ e) $$

Programs in While language are generated by the following grammar:

$$ \langle prog \rangle ::= \mathit{skip} \mid \mathbb{N} ::= \langle expr \rangle \mid \langle prog \rangle ; \langle prog \rangle \mid \mathit{while} \langle expr \rangle \langle prog \rangle $$

The operational semantics of our While language are introduced in Figure 1. We are using the notation $s, x \downarrow s'$ to denote that program $x$, when supplied with $s : S$, terminates producing store $s'$. Similarly, $s, x \to s', x'$ means that program $x$, supplied with $s$, evaluates to $x'$ and produces new store $s'$.

$$ \begin{array}{ccc} \frac{s, \mathit{skip} \downarrow s}{s, p \to s', p'} & \frac{s, l := e \downarrow \mathit{update} \ s \ l \ (\mathit{eval} \ s \ e)}{s, \mathit{while} \ e \ p \to s, \mathit{skip}} & \frac{s, p \downarrow s'}{s, p; q \to s', q} \\ \frac{s, p; q \to s', p'; q}{s, p} & \frac{\mathit{eval} \ s \ e = 0}{s, \mathit{while} \ e \ p \to s, \mathit{skip}} & \frac{\mathit{eval} \ s \ e \neq 0}{s, \mathit{while} \ e \ p \to s, p; \mathit{while} \ e \ p} \end{array} $$

<caption>**Fig. 1.** Semantics of the While language.</caption>

## 2.2 While, categorically

The categorical representation of operational semantics has various forms of incremental complexity but for our purposes we only need to use the most important one, that of GSOS laws [48].

**Definition 2.** Given a syntax functor $\Sigma$ and a behavior functor $B$, a GSOS law of $\Sigma$ over $B$ is a natural transformation $\rho : \Sigma(\mathrm{Id} \times B) \Rightarrow B\Sigma^*$, where $(\Sigma^*, \eta, \mu)$ is the monad freely generated by $\Sigma$.

*Example 1.* Let $E$ be the set of expressions of the While-language. Then the syntax functor $\Sigma : \mathbf{Set} \to \mathbf{Set}$ for While is given by $\Sigma X = \top \uplus (\mathbb{N} \times E) \uplus (X \times X) \uplus (E \times X)$ where $\uplus$ denotes a disjoint (tagged) union. The elements could be denoted as skip, $l := e$, $x_1; x_2$ and while $e \ x$ respectively. The free monad
$\Sigma^*$ satisfies $\Sigma^* X \cong X \uplus \Sigma \Sigma^* X$, i.e. its elements are programs featuring program variables from $X$. Since *While*-programs run in interaction with a store and can terminate, the behavior functor is $BX = S \to (S \times \text{Maybe } X)$, where $S$ is the set of lists of natural numbers and $X \to Y$ denotes the exponential object (internal Hom) $Y^X$.

The GSOS specification of *While* determines $\rho$. A premise $s, p \to s', p'$ denotes an element $(p, b) \in (\text{Id} \times B)X$ where $b(s) = (s', \text{just } p')$, and a premise $s, p \downarrow s'$ denotes an element $(p, b)$ where $b(s) = (s', \text{nothing})$. A conclusion $s, p \to s', p'$ (where $p \in \Sigma X$ is further decorated above the line to $\bar{p} \in \Sigma(\text{Id} \times B)X$) specifies that $\rho(\bar{p}) \in B\Sigma^* X$ sends $s$ to $(s', \text{just } p')$, whereas a conclusion $s, p \downarrow s'$ specifies that $s$ is sent to $(s', \text{nothing})$. Concretely, $\rho_X : \Sigma(X \times BX) \to B\Sigma^* X$ is the function (partially from [47]):

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

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

It has been shown by Lenisa et al. [28] that there is a one-to-one correspondence between GSOS laws of $\Sigma$ over $B$ and distributive laws of the free monad $\Sigma^*$ over the cofree copointed endofunctor [28] $\text{Id} \times B$.<fnref n="4" />

**Definition 3 (In [26]).** A distributive law of a monad $(T, \eta, \mu)$ over a copointed functor $(H, \epsilon)$ is a natural transformation $\lambda : TH \implies HT$ subject to the following laws: $\lambda \circ \eta = H\eta$, $\epsilon \circ \lambda = T\epsilon$ and $\lambda \circ \mu = H\mu \circ \lambda \circ T\lambda$.

Given any GSOS law, it is straightforward to obtain the corresponding distributive law via structural induction (In [50], prop. 2.7 and 2.8). By convention, we shall be using the notation $\rho$ for GSOS laws and $\rho^*$ for the equivalent distributive laws unless stated otherwise.

A distributive law $\lambda$ based on a GSOS law $\rho$ gives a category $\lambda$-Bialg of $\lambda$-bialgebras [48], which are pairs $\Sigma X \xrightarrow{h} X \xrightarrow{k} BX$ subject to the pentagonal law $k \circ h = Bh^* \circ \rho_X \circ \Sigma[id, k]$, where $h^*$ is the inductive extension of $h$. Morphisms in $\lambda$-Bialg are arrows $X \to Y$ that are both algebra and coalgebra homomorphisms at the same time. The trivial initial B-coalgebra $\perp \to B\perp$ lifts uniquely to the initial $\lambda$-bialgebra $\Sigma\Sigma^*\perp \xrightarrow{a} \Sigma^*\perp \xrightarrow{h_\lambda} B\Sigma^*\perp$, while the trivial final $\Sigma$-algebra $\Sigma\top \to \top$ lifts uniquely to the final $\lambda$-bialgebra $\Sigma B^\infty\top \xrightarrow{g_\lambda} B^\infty\top \xrightarrow{z} BB^\infty\top$<fnref n="5" />. Since $\Sigma^*\perp$ is the set of programs generated by $\Sigma$ and $B^\infty\top$ the set of behaviors cofreely generated by $B$, the unique bialgebra morphism $f : \Sigma^*\perp \to B^\infty\top$ is the interpretation function induced by $\rho$.

<footnote n="4">⁴ A copointed endofunctor is an endofunctor $F$ equipped with a natural transformation $F \implies \text{Id}$.</footnote>

<footnote n="5">⁵ We write $B^\infty$ for the cofree comonad over $B$, which satisfies $B^\infty X \cong X \times BB^\infty X$.</footnote>
**Remark 1.** We write $A$ for $\Sigma^* \perp$ and $Z$ for $B^\infty \top$, and refer to $h_\lambda : A \to BA$ as the *operational model* for $\lambda$ and to $g_\lambda : \Sigma Z \to Z$ as the *denotational model* [48]. Note also that $a : \Sigma A \cong A$ and $z : Z \cong BZ$ are invertible.

**Example 2.** Continuing Example 1, the initial bialgebra $A$ is just the set of all *While*-programs. Meanwhile, the final bialgebra $Z$, which has the meaning of the set of behaviors, satisfies $Z \cong (S \to S \times \text{Maybe } Z)$. In other words, our attacker model is that of an attacker who can count execution steps and moreover, between any two steps, read out and modify the state. In Section 9, we discuss how we hope to consider weaker attackers in the future.

## 3 An extra register (Part I)

Let us consider the scenario where a malicious party can observe *more* information about the execution state of a program, either because information is being leaked to the environment or the programs are run by a more powerful machine. A typical example is the presence of an extra *flags register* that logs the result of a computation [34, 8, 35]. This is the intuition behind the augmented version of *While* with additional observational capabilities, $While_\Delta$.

The main difference is in the behavior so the notation for transitions has to slightly change. The two main transition types, $s, x \Downarrow_v s'$ and $s, x \to_v s', x'$ work similarly to *While* except for the label $v : \mathbb{N}$ produced when evaluating expressions. We also allow language terms to interact with the labels by introducing the constructor **obs** $\mathbb{N} \langle prog \rangle$. When terms evaluate inside an **obs** block, the labels are sequentially placed in the run-time store. The rest of the constructors are identical but the distinction between the two languages should be clear.

While the expressions are the same as before, the syntax functor is now $\Sigma_\Delta X = \Sigma X \uplus \mathbb{N} \times X$, and the behavior functor is $B_\Delta = S \to \mathbb{N} \times S \times \text{Maybe } X$. The full semantics can be found in Figure 2. As for *While*, they specify a GSOS law $\rho_\Delta : \Sigma_\Delta (\text{Id} \times B_\Delta) \implies B_\Delta \Sigma_\Delta^*$.

<figure><img src="image_4.png" /><figcaption>**Fig. 2.** Semantics of $While_\Delta$.</figcaption></figure>

Traditionally, the (in)security of a compiler has been a matter of *full abstraction*; a compiler is fully abstract if it preserves and reflects Morris-style [31]
contextual equivalence. For our threat model, where the attacker can directly observe labels, it makes sense to define contextual equivalence in While<sub>Δ</sub> as:

**Definition 4.** $p \cong_{\Delta} q \iff \forall c : C_{\Delta}, c \llbracket p \rrbracket \downarrow \iff c \llbracket q \rrbracket \downarrow$

Where C is the set of one-hole contexts, $\llbracket \cdot \rrbracket : C_{\Delta} \times A_{\Delta} \to A_{\Delta}$ denotes the plugging function and we write $p \downarrow$ when p eventually terminates. Contextual equivalence for While is defined analogously. It is easy to show that the simple “embedding” compiler from While to While<sub>Δ</sub> is not fully abstract by examining terms $a \triangleq \mathbf{while} (\mathbf{var}[0])$ ($0 := 0$) and $b \triangleq \mathbf{while} (\mathbf{var}[0] * 2)$ ($0 := 0$), for which $a \cong b$ but $a_{\Delta} \not\cong_{\Delta} b_{\Delta}$. A context $c \triangleq (\mathbf{obs} 1 \_); \mathbf{while} (\mathbf{var}[1] - 1) \mathbf{skip}$ will log the result of the while condition in $a_{\Delta}$ and $b_{\Delta}$ in var[1] and then either diverge or terminate depending on the value of var[1]. An initial var[0] value of 1 will cause $c \llbracket a \rrbracket$ to terminate but $c \llbracket b \rrbracket$ to diverge.

**Securely extending While<sub>Δ</sub>** To deter malicious contexts from exploiting the extra information, we introduce sandboxing primitives to help hide it. We add an additional constructor in While<sub>Δ</sub>, $\lceil \langle progr \rangle \rceil$, and the following inference rules to form the secure version While<sub>Δ</sub> of While<sub>Δ</sub>.

$$ \frac{s, p \downarrow_v s'}{s, \lceil p \rceil \downarrow_0 s'} \qquad \frac{s, p \to_v s', p'}{s, \lceil p \rceil \to_0 s', \lceil p' \rceil} $$

We now consider the compiler from While to While<sub>Δ</sub> which, along with the obvious embedding, wraps the translated terms in sandboxes. This looks to be effective as programs a and b are now contextually equivalent and the extra information is adequately hidden. We will show that this compiler is indeed a map of distributive laws between While and While<sub>Δ</sub> but to do so we need a brief introduction on the underlying theory.

# 4 Secure compilers, categorically

## 4.1 Maps of distributive laws

Assume two GSOS laws $\rho_1 : \Sigma_1(\mathrm{Id} \times B_1) \Rightarrow B_1\Sigma_1^*$ and $\rho_2 : \Sigma_2(\mathrm{Id} \times B_2) \Rightarrow B_2\Sigma_2^*$, where $(\Sigma_1^*, \eta_1, \mu_1)$ and $(\Sigma_2^*, \eta_2, \mu_2)$ are the monads freely generated by $\Sigma_1$ and $\Sigma_2$ respectively. We shall regard pairs of natural transformations $(\sigma : \Sigma_1^* \Rightarrow \Sigma_2^*, b : B_1 \Rightarrow B_2)$ as compilers between the two semantics, where $\sigma$ acts as a syntactic translation and $b$ as a translation between behaviors.

**Remark 2.** If $A_1$ and $A_2$ are the sets of terms freely generated by $\Sigma_1$ and $\Sigma_2$, we can get the compiler $c : A_1 \to A_2$ from $\sigma$. On the other hand, $b$ generates a function $d : Z_1 \to Z_2$ between behaviors via finality.

**Remark 3.** We shall be writing $B^c$ for the cofree copointed endofunctor $\mathrm{Id} \times B$ over B and $b^c : B_1^c \Rightarrow B_2^c$ for $\mathrm{id} \times b$.
**Definition 5 (Adapted from [50]).** A map of GSOS laws from $\rho_1$ to $\rho_2$ consists of a natural transformation $\sigma : \Sigma_1^* \Rightarrow \Sigma_2^*$ subject to the monad laws $\sigma \circ \eta_1 = \eta_2$ and $\sigma \circ \mu_1 = \mu_2 \circ \Sigma_2^* \sigma \circ \sigma$ paired with a natural transformation $b : B_1 \Rightarrow B_2$ that satisfies the following coherence criterion:

$$ \begin{array}{ccc} \Sigma_1^* B_1^c & \underset{\rho_1^*}{\Rightarrow} & B_1^c \Sigma_1^* \\ \multicolumn{3}{c}{\sigma \circ \Sigma_1^* b^c} \\ \multicolumn{3}{c}{\Downarrow} \\ \Sigma_2^* B_2^c & \underset{\rho_2^*}{\Rightarrow} & B_2^c \Sigma_2^* \end{array} \quad \triangleright $$

*Remark 4.* A natural transformation $\sigma : \Sigma_1^* \Rightarrow \Sigma_2^*$ subject to the monad laws is equivalent to a natural transformation $t : \Sigma_1 \Rightarrow \Sigma_2^*$.

**Theorem 1.** If $\sigma$ and $b$ constitute a map of GSOS laws, then we get a compiler $c : A_1 \to A_2$ and behavior transformation $d : Z_1 \to Z_2$ satisfying $d \circ f_1 = f_2 \circ c : A_1 \to Z_2$. As bisimilarity is exactly equality in the final coalgebra (i.e. equality under $f_i : A_i \to Z_i$), $c$ preserves bisimilarity [50]. If $d$ is a monomorphism (which, under mild conditions, is the case in Set if every component of $b$ is a monomorphism), then $c$ also reflects bisimilarity.

What is very important though, is that the well-behavedness properties of the two GSOS laws bestow *contextual* meaning to bisimilarity. Recall that the gold standard for secure compilation is contextual equivalence (Definition 4), which is precisely what is observable through program contexts. Bisimilarity is generally not the same as contextual equivalence, but we can instead show that in the case of GSOS laws or other forms of distributive laws, bisimilarity defines the *upper bound* (most fine-grained distinction) of observability up to program contexts. We shall do so abstractly in the next subsections.

## 4.2 Abstract program contexts

The informal notion of a *context* in a programming language is that of a program with a hole [31]. Thus contexts are a syntactic construct that models external interactions with a program: a single context is an experiment whose outcome is the evaluation of the subject program *plugged* in the context.

Naïvely, one may hope to represent contexts by a functor $H$ sending a set of variables $X$ to the set $HX$ of terms in $\Sigma X$ that may have holes in them. A complication is that contexts may have holes at any depth (i.e. any number of operators may have been applied to a hole), whereas $\Sigma X$ is the set of terms that have exactly one operator in them, immediately applied to variables. One solution is to think of $Y$ in $HY$ as a set of variables that do not stand for terms, but for contexts. This approach is fine for multi-hole contexts, but if we also want to consider single-hole contexts and a given single-hole context $c$ is not the hole itself, then precisely one variable in $c$ should stand for a single-hole context, and all other variables should stand for terms. Thus, in order to support both single- and multi-hole contexts, we make $H$ a two-argument functor, where $H_X Y$ is the set of contexts with term variables from $X$ and context variables from $Y$.
The ‘pattern matching’ is justified by distributivity of $\mathbb{C}$. For hole $= i_1 : \top \to \top \uplus \Sigma X$, we can see that $\text{con} \circ (\text{id} \times \text{hole}) = i_1 \circ \pi_1$ as required by the definition of a context functor.

**Single-hole contexts** It was observed by McBride [29] that for inductive types, i.e. least fixpoints / initial algebras $\mu F$ of certain endofunctors $F$ called *containers* [4] or simply *polynomials*, their single-hole contexts are lists of $\partial F(\mu F)$ where $\partial F$ is the *derivative* of $F$ $^6$. Derivatives for containers, which were developed by Abbott et al. in [5], enable us to give a categorical interpretation of single-hole contexts as long as the syntax functor $\Sigma$ is a container.

It would be cumbersome to lay down the entire theory of containers and their
derivatives, so we shall instead focus on the more restricted set of *Simple Polynomial Functors* [22] (or SPF), used to model both syntax and behavior. Crucially,
SPF’s are differentiable and hence compatible with McBride’s construction.

**Definition 8 (Simple Polynomial Functors).** The collection of SPF is the least set of functors $\mathbb{C} \to \mathbb{C}$ satisfying the following rules:

$$
\begin{tikzcd}
id \arrow[r, "\text{const}", "K_J \in \text{SPF}"] \arrow[d, "\text{Id} \in \text{SPF}"] & \frac{J \in \text{Obj}(\mathbb{C})}{K_J \in \text{SPF}} \arrow[r, "\text{prod}", "F, G \in \text{SPF}"] \arrow[d, "F \uplus G \in \text{SPF}"] & \frac{F, G \in \text{SPF}}{F \times G \in \text{SPF}} \\
\text{coprod} \arrow[r, "F, G \in \text{SPF}", "\text{comp}"] & \text{prod} \arrow[r, "F, G \in \text{SPF}", "\text{comp}"] & \text{SPF} \arrow[d, "F \circ G \in \text{SPF}"]
\end{tikzcd}
$$

We can now define the differentiation action $\partial : \text{SPF} \to \text{SPF}$ by structural induction. Interestingly, it resembles simple derivatives for polynomial functions.

**Definition 9 (SPF derivation rules).**

$$
\begin{align*}
\partial \mathrm{Id} &= \top, & \partial K_J &= \bot, & \partial (G \uplus H) &= \partial G \uplus \partial H, \\
\partial (G \times H) &= (\partial G \times H) \uplus (G \times \partial H), & \partial (G \circ H) &= (\partial G \circ H) \times \partial H.
\end{align*}
$$

*Example 3.* The definition of con for single-hole contexts might look a bit cryptic at first sight so we shall use a small example from [29] to shed some light. In the case of binary trees, locating a hole in a context can be thought of as traversing through a series of nodes, choosing left or right according to the placement of the hole until it is found. At the same time a record of the trees at the non-chosen branches must be kept so that in the end the entire structure can be reproduced.

Now, considering that the set of binary trees is the least fixed point of functor
$\top \uplus (\text{Id} \times \text{Id})$, then the type of "abstract" choice at each intersection is the
functor $K_{\text{Bool}} \times \text{Id}$, where $K_{\text{Bool}}$ stands for a choice of left or right and the $\text{Id}$
part represents the passed structure. Lists of $(K_{\text{Bool}} \times \text{Id})$ BinTree are exactly
the sort of record we need to keep, i.e. they contain the same information as a
tree with a single hole. And indeed $K_{\text{Bool}} \times \text{Id}$ is (up to natural isomorphism)
the derivative of $\top \uplus (\text{Id} \times \text{Id})$!

<footnote n="6">⁶ The list operator itself arises from the derivative of the free monad operator.</footnote>
The contextual co-closure $A \stackrel{\bar{\tau}_1}{\rightleftarrows} \bar{R} \stackrel{\bar{\tau}_2}{\rightarrow} A$ of an arbitrary span $A \stackrel{r_1}{\rightleftarrows} R \stackrel{r_2}{\rightarrow} A$ is the final contextually closed span on $A$ with a span morphism $\bar{R} \rightarrow R$.

We call terms bisimilar if the operational semantics $f: A \rightarrow Z$ assigns them equal behaviors:

**Definition 11.** We define (strong) bisimilarity $\sim_{bis}$ as the pullback of the equality span $(\mathrm{id}_Z, \mathrm{id}_Z): Z \rightarrow Z \times Z$ along $f \times f: A \times A \rightarrow Z \times Z$ (if existent).

**Theorem 2.** Under the assumptions of 7, bisimilarity (if existent) is contextually closed.

*Proof.* We need to give a morphism of spans from $C_A \times (\sim_{bis})$ to $(\sim_{bis})$:

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

By definition of $(\sim_{bis})$, it suffices to give a morphism of spans to the equality span on $Z$, i.e. to prove that $f \circ [] \circ (\mathrm{id} \times r_1) = f \circ [] \circ (\mathrm{id} \times r_2)$. To this end, consider the following diagram (parameterized by $i \in \{1,2\}$), in which every polygon is easily seen to commute:

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

The bottom-right square stems from the underlying GSOS law: it is the algebra homomorphism part of the bialgebra morphism between the initial and the final bialgebras. Commutativity of the outer diagram reveals that $f \circ [] \circ (r_i \times \mathrm{id})$ is, regardless of $i$, the strong inductive extension of $[\mathrm{id}_Z, q_Z] \circ \mathrm{con}_Z \circ (w \times H_f \mathrm{id}_Z): (\sim_{bis}) \times H_A Z \rightarrow Z$. Thus, it is independent of $i$. $\square$
**Corollary 1.** In Set, bisimilarity is its own contextual coclosure: $a \sim_{bis} b \iff \forall c \in C_A. c[[a]] \sim_{bis} c[[b]]$

**Corollary 2.** In Set, bisimilarity implies contextual equivalence.<fnref n="7" />

*Proof.* Bisimilarity implies equitermination. This yields an implication between their coclosures. □

Comparing Corollary 1 to contextual equivalence in Definition 4 reveals their key difference. Contextual equivalence makes minimal assumptions on the underlying observables, which are simply divergence and termination. On the other hand, the contextual coclosure of bisimilarity assumes maximum observability (as dictated by the behavior functor) and in that sense it represents the upper bound of what can be observed through contexts. Consequently, this criterion is useful if the observables adequately capture the threat model, which is true for the examples that follow.

This theorem echoes similar results in the broader study of coalgebraic bisim- ulation [11, 41]. There are, however, two differences. The first is that our theorem allows for extra flexibility in the definition of contexts as the theorem is paramet- ric on the context functor. Second, by making the context construction explicit we can directly connect (the contextual coclosure of) bisimilarity to contextual equivalence (Corollary 2) and so have a more convincing argument for using maps of distributive laws as secure compilers.

# 5 An extra register (Part II)

The next step is to define the syntax and behavior natural transformations. The first compiler, $\sigma_{\Delta} : \Sigma \Rightarrow \Sigma_{\Delta}$, is a very simple mapping of constructors in While to their While$_{\Delta}$ counterparts. The second natural transformation, $\sigma_{\mathcal{K}} : \Sigma \Rightarrow \Sigma_{\mathcal{K}}^*$, is more complex as it involves an additional layer of syntax in While$_{\mathcal{K}}$.

**Definition 12 (Sandboxing natural transformation).** Consider the nat- ural transformation $e : \Sigma \Rightarrow \Sigma_{\mathcal{K}}$ which embeds $\Sigma$ in $\Sigma_{\mathcal{K}}$. Using PL notation, we define $\sigma_{\mathcal{K}} : \Sigma X \to \Sigma_{\mathcal{K}}^* X : p \mapsto \lceil e(p) \rceil$. This yields a monad morphism $\sigma_{\mathcal{K}}^* : \Sigma^* \to \Sigma_{\mathcal{K}}^*$ (Remark 4).

Defining the natural translation between behaviors is a matter of choosing a designated value for the added observable label. The only constraint is that the chosen value has to coincide with the label that the sandbox produces. $B_{\Delta}$ and $B_{\mathcal{K}}$ are identical so we need a single natural transformation $b : B \Rightarrow B_{\Delta/\mathcal{K}}$:

$$b : \forall X. (S \to S \times \text{Maybe } X) \to S \to \mathbb{N} \times S \times \text{Maybe } X$$

$$b f = \lambda(s : S) \to (0, f(s))$$

<footnote n="7">⁷ Note that we can not conclude that preservation of bisimilarity would imply preservation of contextual equivalence.</footnote>
**While** *to While*<sub>Δ</sub> We now have the natural translation pairs $(\sigma_{\Delta}, b)$ and $(\sigma_{\mathcal{K}}, b)$, which allows us to check the coherence criterion from Section 4.1. We shall be using a graphical notation that provides for a good intuition as to what failure or success of the criterion *means*. For example, Fig. 3 shows failure of the coherence criterion for the first pair.

The horizontal arrows in the diagram represent the two semantics, $\rho^*$ and $\rho^*_{\Delta}$, while the vertical arrows are the two horizontal compositions of the natural translation pair. The top-left node holds an element of $\Sigma^*(\mathrm{Id} \times B)$, which in this case is an assignment operation. The two rightmost nodes represent behaviors,

so the syntactic element is missing from the left side of the transition arrows.

In the upper path, the term is first applied to the GSOS law $\rho^*$ and the result is then passed to the translation pair, thus producing the designated label 0, typeset in blue for convenience. In the lower path, the term is first applied to the translation and then goes through the target semantics, $\rho^*_{\Delta}$, where the label $v$ is produced. It is easy to find such an $s$ so that $v \neq 0$.

<figure><img src="image_7.png" /><figcaption>Fig. 3. Failure of the criterion for $(\sigma_{\Delta}, b)$.</figcaption></figure>

**While** *to While*<sub>Δ</sub> The same example is investigated for the second translation pair $(\sigma_{\mathcal{K}}, b)$. Figure 4 shows what happens when we test the same case as before. Applying $\rho^*_{\mathcal{K}}$ to $\lceil l := e \rceil$ is similar to $\rho_{\mathcal{K}}$ acting twice. The innermost transition is the intermediate step and as it only appears in the bottom path it is typeset in

red. This time the diagram commutes as the label produced in the inner layer, $v$, is effectively erased by the sandboxing rules of *While*<sub>Δ</sub>.

<figure><img src="image_8.png" /><figcaption>Fig. 4. The coherence criterion for $(\sigma_{\mathcal{K}}, b)$.</figcaption></figure>

**An endo-compiler for While<sub>Δ</sub>** If $A_{\mathcal{K}}$ is the set of closed terms for While<sub>Δ</sub>, the compiler $u: A_{\mathcal{K}} \rightarrow A_{\mathcal{K}}$, which “escapes” While<sub>Δ</sub> terms from their sandboxes can be elegantly modeled using category theory. As before, it is not possible to express it using a simple natural transformation $\Sigma_{\mathcal{K}} \Rightarrow \Sigma_{\mathcal{K}}$. We can, however, use the free pointed endofunctor [28] over $\Sigma_{\mathcal{K}}$, $\mathrm{Id} \to \Sigma_{\mathcal{K}}$. What we want is to map non-sandboxed terms to themselves and lift the extra layer of syntax from sandboxed terms. Intuitively, for a set of variables $X$, $\Sigma_{\mathcal{K}}X$ is one layer of syntax “populated” with elements of $X$. If $X \supseteq \Sigma_{\mathcal{K}}X$ is the union of $\Sigma_{\mathcal{K}}X$ with the set of variables $X$, lifting the sandboxing layer is mapping the $X$ in $\lceil X \rceil$ to the left of $X \supseteq \Sigma_{\mathcal{K}}X$ and the rest to themselves at the right.
<figure><img src="image_9.png" /><figcaption>Fig. 5. Failure of the criterion for $\sigma_u$.</figcaption></figure>

This is obviously not a secure compiler as it allows discerning previously indistinguishable programs. As we can see in Figure 5, the coherence criterion fails in the expected manner.

# 6 State mismatch

Having established our categorical foundations, we shall henceforth focus on examples. The first one involves a compiler where the target machine is not necessarily more powerful than the source machine, but the target *value* primitives are not isomorphic to the ones used in the source. This is a well-documented problem [37], which has led to failure of full abstraction before [8, 18, 25].

For example, we can repeat the development of *While* except we substitute natural numbers with integers. We call this new version *While<sub>Z</sub>*.

$$ \langle expr \rangle ::= lit \mathbb{Z} \mid var \mathbb{N} \mid \langle expr \rangle \langle bin \rangle \langle expr \rangle \mid \langle un \rangle \langle expr \rangle $$

The behavior functor also differs in that the store type $S$ is substituted with $S_Z$, the set of lists of integers. We can define the behavioral natural transformation $b_Z : B \implies B_Z$ as the best “approximation” between the two behaviors. In Set:

$$ b_Z : \forall X. (S \to S \times (\top \uplus X)) \to S_Z \to S_Z \times (\top \uplus X) $$

$$ b_Z f = [\text{toZ}, \text{id}] \circ f \circ \text{toN} $$

Where toN replaces all negative numbers in the store with 0 and toZ typecasts $S$ to $S_Z$. It is easy to see that the identity compiler from *While* to $While_Z$ is not fully abstract. For example, the expressions 0 and $min(var[0], 0)$ are identical in *While* but can be distinguished in $While_Z$ (if

<figure><img src="image_10.png" /><figcaption>Fig. 6. Failure of the criterion for (id, $b_Z$).</figcaption></figure>

$var[0]$ is negative). This is reflected in the coherence criterion diagram for the identity compiler in Figure 6, when initiating the store with a negative integer.

The solution is to create a special environment where $While_Z$ forgets about negative integers, in essence copying what $b_Z$ does on the store. This is a special kind of sandbox, written $\langle \cdot \rangle$, for which we introduce the following rules:

$$ \frac{\text{toN}(s), p \downarrow s'}{s, \langle p \rangle \downarrow s'} \qquad \frac{\text{toN}(s), p \to s', p'}{s, \langle p \rangle \to s', \langle p' \rangle} $$
<figure><img src="image_11.png" /><figcaption>Fig. 7. The coherence criterion for $(\sigma_Z, b_Z)$.</figcaption></figure>

We may now repeat the construction from Definition 12 to define the compiler $\sigma_Z$. We can easily verify that the pair $(\sigma_Z, b_Z)$ constitutes a map of distributive laws. For instance, Figure 7 demonstrates how the previous failing case now works under $(\sigma_Z, b_Z)$.

# 7 Control Flow

Many low-level languages support unrestricted control flow in the form of jumping or branching to an address. On the other hand, control flow in high-level languages is usually restricted (think if-statements or function calls). A compiler from the high-level to the low-level might be insecure as it exposes source-level programs to illicit control flow. This is another important and well-documented example of failure of full abstraction [8, 37, 3, 33].

<figure><img src="image_12.png" /><figcaption>Fig. 8. Semantics of the Low language. Elements in square brackets are optional.</figcaption></figure>

We introduce low-level language *Low*, the programs of which are non-empty lists of instructions. *Low* differs significantly from *While* and its derivatives in both syntax and semantics. For the syntax, we define the set of instructions $\langle inst \rangle$ and set of programs $\langle asm \rangle$.

$$ \langle inst \rangle ::= \text{nop} | \text{stop} | \text{assign} \ N \langle expr \rangle | \text{br} \ \langle expr \rangle \ Z $$

$$ \langle asm \rangle ::= \langle inst \rangle | \langle inst \rangle ;; \langle asm \rangle $$
Instruction `nop` is the no-operation, `stop` halts execution and `assign` is analogous to the assignment operation in *While*. The `br` instruction is what really defines *Low*, as it stands for bidirectional relative branching.

**Semantics of Low** Figure 8 shows the operational semantics of *Low*. The execution state of a running program consists of a run-time store and the program counter register PC ∈ Z that points at the instruction being processed. If the program counter is zero, the leftmost instruction is executed. If the program counter is greater than zero, then the current instruction is further to the right. Otherwise, the program counter is out-of-bounds and execution stops. The categorical interpretation suggests a GSOS law ρ$_{L}$ of syntax functor Σ$_{L}$X = inst⊕(inst × X) over behavior functor B$_{L}$X = S × Z → S × Z × Maybe X.

**An insecure compiler** This time we start with the behavioral translation, which is less obvious as we have to go from $BX = S \to S \times \text{Maybe } X$ to $B_L X = S \times Z \to S \times Z \times \text{Maybe } X$. The increased arity in $B_L$ poses an interesting question as to what the program counter should mean in *While*. It makes sense to consider the program counter in *While* as zero since a program in *While* is treated uniformly as a single statement.

$$b_L : \forall X. (S \to S \times \text{Maybe } X) \to S \times Z \to S \times Z \times \text{Maybe } X$$

$$b_L f (s, 0) = \begin{cases} (s', 1, \text{nothing}) & \text{if } f s = (s', \text{nothing}) \\ (s', 0, \text{just } y) & \text{if } f s = (s', \text{just } y) \end{cases}$$

$$b_L f (s, n \neq 0) = (s, n, \text{nothing})$$

When it comes to translating terms, a typical compiler from *While* to *Low* would untangle the tree-like structure of *While* and convert it to a list of *Low* instructions. For `while` statements, the compiler would use branching to simulate looping in the low-level.

**Example 4.** Let us look at a simple case of a loop. The *While* program `while (var 0 < 2) (1 := var 1 + 1)` is compiled to `br ! (var 0 < 2) 3 ;; assign 1 (var 1 + 1) ;; br (lit 1) -2`

This compiler, called $c_L$, cannot be defined in terms of a natural transformation $\Sigma \implies \Sigma_L^*$ as per Remark 4, but it is inductive on the terms of the source language. In this case we can directly compare the two operational models $b_A \circ h : A \to B_L A$ (where $h : A \to BA$) and $h_L : A_L \to B_L A_L$ and notice that $c_L : A \to A_L$ is not a coalgebra homomorphism (Figure 9). The key is

<figure><img src="image_13.png" /><figcaption>Fig. 9. $c_L$ is not a coalgebra homomorphism.</figcaption></figure>
that the program counter in *Low* allows for finer observations on programs. Take for example the case for **while** (lit 0) (0 := lit 0), where the loop is always skipped. In *Low*, we can still access the loop body by simply pointing the program counter to it. This is a realistic attack scenario because *Low* allows manipulation of the program counter via the **br** instruction.

**Solution** By comparing the semantics between *While* in Figure 1 and *Low* in Figure 8 we find major differences. The first one is the reliance of *Low* to a program counter which keeps track of execution, whereas *While* executes statements from left to right. Second, the sequencing rule in *While* dictates that statements are removed from the program state<fnref n="8" /> upon completion. On the other hand, *Low* keeps the program state intact at all times. Finally, there is a stark contrast between the two languages in the way they handle **while** loops.

To address the above issues we introduce a new sequencing primitive `;;c` and a new looping primitive `loop` for *Low*, which prohibit illicit control flow and properly propagate the internal state. Furthermore, we change the semantics of the singleton **assign** instruction so that it mirrors the peculiarity of its *While* counterpart. The additions can be found in Figure 10.

<figure><img src="image_14.png" /><figcaption>**Fig. 10.** Secure primitives for the *Low* language.</figcaption></figure>

We may now define the simple “embedding” natural transformation $\sigma_E : \Sigma \Rightarrow \Sigma_L$, which maps **skip** to **stop**, assignments to **assign**, sequencing to `;;c` and **while** to **loop**.

Figure 11 shows success of the coherence criterion for the **while** case. Since the diagram commutes for all cases, $(\sigma_E, b_E)$ is a map of GSOS laws between *While* and the secure version of *Low*. This guarantees that, remarkably, despite the presence of branching, a low-level attacker cannot illicitly access code that is unreachable on

<figure><img src="image_15.png" /><figcaption>**Fig. 11.** The coherence criterion for $(\sigma_E, b_L)$.</figcaption></figure>

<footnote n="8">⁸ We are not referring to the store, but to the internal, algebraic state.</footnote>
the high-level. Regardless, the solution is a bit contrived in that the new *Low* primitives essentially copy what *While* does. This is partly because the above are complex issues involving radically different languages but also due to the current limitations of the underlying theory. We elaborate further on said limitations, as well as advantages and future improvements, at Section 9.

## 8 Local state encapsulation

High-level programming language abstractions often involve some sort of private state space that is protected from other objects. Basic examples include functions with local variables and objects with private members. Low-level languages do not offer such abstractions but when it comes to *secure architectures*, there is some type of *hardware sandboxing*<fnref n="9" /> to facilitate the need for *local state encapsulation*. Compilation schemes that respect confidentiality properties have been a central subject in secure compilation work [37, 8, 18, 46], dating all the way back to Abadi's seminal paper [1].

In this example we will explore how local state encapsulation fails due to lack of stack clearing [46, 44]. We begin by extending *While* to support blocks which have their own private state, thus introducing *While*<sub>B</sub>. More precisely, we add the **frame** and **return** commands that denote the beginning and end of a new block. We also have to modify the original behavior functor *B* to act on a stack of stores by simply specifying $B_B X = [S] \to [S] \times \text{Maybe } X$, where $[S]$ denotes a list of stores. For reasons that will become apparent later on, we shall henceforth consider stores of a certain length, say *L*.

<figure><img src="image_16.png" /><figcaption>**Fig. 12.** Semantics of the *While*<sub>B</sub> language.</figcaption></figure>

The semantics for *While*<sub>B</sub> can be found in Figure 12. Command **frame** allocates a new private store by appending one to the stack of stores while **return** pops the top frame from the stack. This built-in, automatic (de)allocation of frames guarantees that there are no traces of activity, in the form of stored values, of past blocks. The rest of the semantics are similar to *While*, only now **evaluating an expression** and **updating the state** acts on a stack of stores instead of a single, infinite store and **var expressions** act on the active, topmost frame.

<footnote n="9">⁹ Examples of this are enclaves in Intel SGX [15] and object capabilities in CHERI [51].</footnote>
<figure><img src="image_17.png" /><figcaption>Fig. 13. Semantics of the Stack language.</figcaption></figure>

**Low-level stack** In typical low-level instruction sets like the Intel x86 [21] or MIPS [30] there is a single, continuous *memory* which is partitioned in *frames* via processor registers. Figure 13 shows the semantics of *Stack*, a variant of *While*<sub>B</sub> with the same syntax that incorporates a simple *low-level stack*. The difference is that the stack frames are all sized *L*, the same size as each individual store in *While*<sub>B</sub>, so at each **frame** and **return** we need only increment and decrement the stack pointer. The presence of the stack pointer, which is essentially a natural number, means that the behavior of *Stack* is $B_S X = S \times \mathbb{N} \rightarrow S \times \mathbb{N} \times \text{Maybe } X$. The new evaluation function, **evalSP**, works similarly to **eval** in Definition 1, except for **var** *l* expressions that dereference values at offset *l* + *L* \* *sp*.

**An insecure compiler** *While*<sub>B</sub> and *Stack* share the same syntax so we only need a behavioral translation, which is all about relating the two different notions of stack. We thus define natural transformation $b_B : B_B \implies B_S$:

$$b_B : \forall X. ([S_L] \rightarrow [S_L] \times \text{Maybe } X) \rightarrow S \rightarrow \mathbb{N} \rightarrow S \times \mathbb{N} \times \text{Maybe } X$$

$$b_B f s sp = (\text{override } (\text{join } m) s, \text{len } m, y) \text{ where } (m, y) = f (\text{div } s sp)$$

$$\text{div } s sp = (\text{take } L s) :: (\text{div } (\text{drop } L s) (sp - 1))$$

$$\text{override } s' s = s' ++ \text{drop } (\text{len } s') s$$

We “divide” an infinite list by the number of stack frames, feed the result to the behavior function *f* and join (“flatten”) it back together while keeping the original part of the infinite list which extends beyond the *active stack* intact. Note that in the case of the **frame** command *f* adds a new frame to the list of stores. The problem is that in *While*<sub>B</sub> the new frame is initialized to 0 in contrast to *Stack* where **frame** does not initialize new frames. This leads to a failure of the coherence criterion for (*id*, *b*<sub>B</sub>) as we can see in Figure 14.

Failure of the criterion is meaningful in that it underlines key problems of this compiler which can be exploited by a low-level attacker. First, the low-level calling convention indirectly allows terms to access expired stack frames. Second, violating the assumption in *While*<sub>B</sub> that new frames are properly initialized breaks behavioral equivalence. For example, programs *a* $\triangleq$ **frame**; 0 := *var*[0]+1 and *b* $\triangleq$ **frame**; 0 := 1 behave identically in *While*<sub>B</sub> but not in *Stack*.
<figure><img src="image_18.png" /><figcaption>Fig. 14. Failure of the criterion for $(id, b_B)$.</figcaption></figure>

**Solution** It is clear that the lack of stack frame initialization in *Stack* is the lead cause of failure so we introduce the following fix in the **frame** rule.

$$ \frac{m' = (\text{take } (L * sp) m) \ \ddagger \ s_0 \ \ddagger (\text{drop } ((L+1)' * sp) m)}{(m, sp), \text{frame} \ \downarrow (m', sp+1)} $$

The idea behind the new **frame** rule is that the L-sized block in position *sp*, which is going to be the new stack frame, has all its values replaced by zeroes. As we can see in Figure 15, the coherence criterion is now satisfied and the example described earlier no longer works.

<figure><img src="image_19.png" /><figcaption>Fig. 15. The coherence criterion for $(id, b_B)$ under the new **frame** rule.</figcaption></figure>

# 9 Discussion and future work

**On Mathematical Operational Semantics** The cases we covered in this paper are presented using Plotkin's Structural Operational Semantics [38], yet their foundations are deeply categorical [48]. Consequently, for one to use the methods presented in this paper, the semantics involved must fall within the framework of distributive laws, the generality of which has been explored in the past [47, 50], albeit not exhaustively. To the best of our knowledge, Section 7 and Section 8 show the first instances of distributive laws as low-level machines.

Bialgebraic semantics are well-behaved in that *bisimilarity* is a *congruence* [19]. We used that to show that two bisimilar programs will remain bisimilar irrespective of the context they are plugged into, which is not the same as contextual equivalence. However, full abstraction is but one of a set of proposed characterizations of secure compilation [36, 2] and the key intuition is that our framework
is suitable as long as bisimilarity adequately captures the threat model. While
this is the case in the examples, we can imagine situations where the threat
model is *weaker* than the one implied by bisimilarity.

For example, language *While*<sub>⊤</sub> in Section 3 includes labels in its transition
structure and the underlying model is accurate in that *While*<sub>⊤</sub> terms can ma-
nipulate said labels. However, if we were to remove *obs* statements from the
syntax, the threat model becomes weaker than the one implied by bisimilarity.
Similarly in Section 7 and *Low*, we could remove the implicit assumption that
the program counter can be manipulated by a low-level attacker.

This issue can be classified as part of the broader effort towards coalgebraic
weak bisimilarity, a hard problem which has been an object of intense, ongoing
scientific research [42, 39, 20, 13, 43, 42, 12]. Of particular interest is the work
by Abou-Saleh and Pattinson [7, 6] about bialgebraic semantics, where they use
techniques introduced in [20] to obtain a more appropriate semantic domain for
effectful languages as a final coalgebra in the Kleisli category of a suitable monad.
This method is thus a promising avenue towards exploring weaker equivalences
in bialgebraic semantics, as long as these can be described by a monad.

**On Maps of Distributive Laws** Maps of distributive laws were first men-
tioned by Power and Watanabe [40], then elaborated as *Well-behaved transla-
tions* by Watanabe [50] and more recently by Klin and Nachyla [27]. Despite the
few examples presented in [50, 27], this paper is the first major attempt towards
applying the theory behind maps of distributive laws in a concrete problem, let
alone in secure compilation.

From a theoretical standpoint, maps of distributive laws have remained largely
the same since their introduction. This comes despite the interesting develop-
ments discussed in Section 9 regarding distributive laws, which of course are
the subjects of *maps* of distributive laws. We speculate the existence of *Kleisli*
maps of distributive laws that guarantee preservation of equivalences weaker
than bisimilarity. We plan to develop this notion and explore its applicability in
future work.

**Conclusion** It is evident that the systematic approach presented in this work may markedly streamline proofs for compiler security as it involves a single, simple coherence criterion. Explicit reasoning about program contexts is no longer necessary, but that does not mean that contexts are irrelevant. On the contrary, the guarantees are implicitly *contextual* due to the well-behavedness of the semantics. Finally, while the overall usability and eventual success of our method remains a question mark as it depends on the expressiveness of the threat model, the body of work in coalgebraic weak bisimilarity and distributive laws in Kleisli categories suggests that there are many promising avenues for further progress.

**Acknowledgements.** This work was partially supported by the Research Fund KU Leuven. Andreas Nuyts holds a PhD fellowship from the Research Foundation - Flanders (FWO).
References

[1] Martín Abadi. "Protection in Programming-Language Translations". In: *Secure Internet Programming, Security Issues for Mobile and Distributed Objects*. 1999, pp. 19–34. DOI: 10.1007/3-540-48749-2\_2. URL: https://doi.org/10.1007/3-540-48749-2\_2.

[2] Carmine Abate et al. *Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation*. 2018. arXiv: 1807.04603 [cs.PL].

[3] Carmine Abate et al. "When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise". In: *Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018*. Ed. by David Lie et al. ACM, 2018, pp. 1351–1368. ISBN: 978-1-4503-5693-0. DOI: 10.1145/3243734.3243745. URL: https://doi.org/10.1145/3243734.3243745.

[4] Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. "Containers: Constructing strictly positive types". In: *Theor. Comput. Sci.* 342.1 (2005), pp. 3–27. DOI: 10.1016/j.tcs.2005.06.002. URL: https://doi.org/10.1016/j.tcs.2005.06.002.

[5] Michael Gordon Abbott et al. "for Data: Differentiating Data Structures". In: *Fundam. Inform.* 65.1-2 (2005), pp. 1–28. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi65-1-2-02.

[6] Faris Abou-Saleh. "A coalgebraic semantics for imperative programming languages". PhD thesis. Imperial College London, UK, 2014. URL: http://hdl.handle.net/10044/1/13693.

[7] Faris Abou-Saleh and Dirk Pattinson. "Towards Effects in Mathematical Operational Semantics". In: *Electr. Notes Theor. Comput. Sci.* 276 (2011), pp. 81–104. DOI: 10.1016/j.entcs.2011.09.016. URL: https://doi.org/10.1016/j.entcs.2011.09.016.

[8] Pieter Agten et al. "Secure Compilation to Modern Processors". In: *25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012*. Ed. by Stephen Chong. IEEE Computer Society, 2012, pp. 171–185. ISBN: 978-1-4673-1918-8. DOI: 10.1109/CSF.2012.12. URL: https://doi.org/10.1109/CSF.2012.12.

[9] Amal Ahmed and Matthias Blume. "An equivalence-preserving CPS translation via multi-language semantics". In: *Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011*. Ed. by Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy. ACM, 2011, pp. 431–444. ISBN: 978-1-4503-0865-6. DOI: 10.1145/2034773.2034830. URL: https://doi.org/10.1145/2034773.2034830.

[10] Amal Ahmed et al. "Secure Compilation (Dagstuhl Seminar 18201)". In: *Dagstuhl Reports* 8.5 (2018). Ed. by Amal Ahmed et al., pp. 1–30. ISSN: 2192-5283. DOI: 10.4230/DagRep.8.5.1. URL: http://drops.dagstuhl.de/opus/volltexte/2018/9891.
[11] Falk Bartels. *On Generalised Coinduction and Probabilistic Specification Formats: Distributive Laws in Coalgebraic Modelling*. 2004.

[12] Filippo Bonchi et al. "Lax Bialgebras and Up-To Techniques for Weak Bisimulations". In: *26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015*. Ed. by Luca Aceto and David de Frutos-Escrig. Vol. 42. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015, pp. 240-253. ISBN: 978-3-939897-91-0. DOI: 10.4230/LIPIcs.CONCUR.2015.240. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.240.

[13] Tomasz Brengos. "Weak bisimulation for coalgebras over order enriched monads". In: *Logical Methods in Computer Science* 11.2 (2015). DOI: 10.2168/LMCS-11(2:14)2015. URL: https://doi.org/10.2168/LMCS-11(2:14)2015.

[14] J. Robin B. Cockett. "Introduction to Distributive Categories". In: *Mathematical Structures in Computer Science* 3.3 (1993), pp. 277-307. DOI: 10.1017/S0960129500000232. URL: https://doi.org/10.1017/S0960129500000232.

[15] Victor Costan and Srinivas Devadas. "Intel SGX Explained". In: *IACR Cryptology ePrint Archive* 2016 (2016), p. 86. URL: http://eprint.iacr.org/2016/086.

[16] Dominique Devriese, Marco Patrignani, and Frank Piessens. "Fully-abstract compilation by approximate back-translation". In: *Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016*. 2016, pp. 164-177. DOI: 10.1145/2837614.2837618. URL: https://doi.org/10.1145/2837614.2837618.

[17] Derek Dreyer, Amal Ahmed, and Lars Birkedal. "Logical Step-Indexed Logical Relations". In: *Logical Methods in Computer Science* 7.2 (2011). DOI: 10.2168/LMCS-7(2:16)2011. URL: https://doi.org/10.2168/LMCS-7(2:16)2011.

[18] Cédric Fournet et al. "Fully abstract compilation to JavaScript". In: *The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013*. 2013, pp. 371-384. DOI: 10.1145/2429069.2429114. URL: https://doi.org/10.1145/2429069.2429114.

[19] Jan Friso Groote and Frits W. Vaandrager. "Structured Operational Semantics and Bisimulation as a Congruence". In: *Inf. Comput.* 100.2 (1992), pp. 202-260. DOI: 10.1016/0890-5401(92)90013-6. URL: https://doi.org/10.1016/0890-5401(92)90013-6.

[20] Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. "Generic Trace Semantics via Coinduction". In: *Logical Methods in Computer Science* 3.4 (2007). DOI: 10.2168/LMCS-3(4:11)2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.

[21] *Intel 64 and IA-32 Architectures Software Developer's Manual*. Intel Corporation. 2016. URL: https://www.intel.com/content/dam/www/public/
us/en/documents/manuals/64-ia-32-architectures-software-developer-instruction-set-reference-manual-325383.pdf.

[22] Bart Jacobs. *Introduction to Coalgebra: Towards Mathematics of States and Observation*. Vol. 59. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. ISBN: 9781316823187. DOI: 10.1017/CBO9781316823187. URL: https://doi.org/10.1017/CBO9781316823187.

[23] Bart Jacobs. "Parameters and Parametrization in Specification, Using Distributive Categories". In: *Fundam. Inform.* 24.3 (1995), pp. 209–250. DOI: 10.3233/FI-1995-2431. URL: https://doi.org/10.3233/FI-1995-2431.

[24] Radha Jagadeesan et al. "Local Memory via Layout Randomization". In: *Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27-29 June, 2011*. IEEE Computer Society, 2011, pp. 161–174. ISBN: 978-1-61284-644-6. DOI: 10.1109/CSF.2011.18. URL: https://doi.org/10.1109/CSF.2011.18.

[25] Andrew Kennedy. "Securing the .NET programming model". In: *Theor. Comput. Sci.* 364.3 (2006), pp. 311–317. DOI: 10.1016/j.tcs.2006.08.014. URL: https://doi.org/10.1016/j.tcs.2006.08.014.

[26] Bartek Klin. "Bialgebras for structural operational semantics: An introduction". In: *Theor. Comput. Sci.* 412.38 (2011), pp. 5043–5069. DOI: 10.1016/j.tcs.2011.03.023. URL: https://doi.org/10.1016/j.tcs.2011.03.023.

[27] Bartek Klin and Beata Nachyla. "Presenting Morphisms of Distributive Laws". In: *6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands*. 2015, pp. 190–204. DOI: 10.4230/LIPIcs.CALCO.2015.190. URL: https://doi.org/10.4230/LIPIcs.CALCO.2015.190.

[28] Marina Lenisa, John Power, and Hiroshi Watanabe. "Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads". In: *Electr. Notes Theor. Comput. Sci.* 33 (2000), pp. 230–260. DOI: 10.1016/S1571-0661(05)80350-0. URL: https://doi.org/10.1016/S1571-0661(05)80350-0.

[29] Conor Mcbride. *The Derivative of a Regular Type is its Type of One-Hole Contexts (Extended Abstract)*. 2001.

[30] *MIPS Architecture for Programmers Volume II-A: The MIPS32 Instruction Set Manual*. MIPS Technologies. 2016. URL: https://s3-eu-west-1.amazonaws.com/downloads-mips/documents/MD00086-2B-MIPS32BIS-AFP-6.06.pdf.

[31] James H. Morris. "Lambda-Calculus Models of Programming Languages". PhD thesis. Massachusetts Institute of Technology, 1968.

[32] Max S. New, William J. Bowman, and Amal Ahmed. "Fully abstract compilation via universal embedding". In: *Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016*. Ed. by Jacques Garrigue, Gabriele Keller, and Eijiro Sumii. ACM, 2016, pp. 103–116. ISBN: 978-1-4503-4219-3. DOI: 10.1145/2951913.2951941. URL: https://doi.org/10.1145/2951913.2951941.
[33] Marco Patrignani, Amal Ahmed, and Dave Clarke. "Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work". In: *ACM Comput. Surv.* 51.6 (Feb. 2019), 125:1–125:36. ISSN: 0360-0300. DOI: 10.1145/3280984.

[34] Marco Patrignani, Dave Clarke, and Frank Piessens. "Secure Compilation of Object-Oriented Components to Protected Module Architectures". In: *Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings*. Ed. by Chung-chieh Shan. Vol. 8301. Lecture Notes in Computer Science. Springer, 2013, pp. 176–191. ISBN: 978-3-319-03541-3. DOI: 10.1007/978-3-319-03542-0\_13. URL: https://doi.org/10.1007/978-3-319-03542-0\_13.

[35] Marco Patrignani, Dominique Devriese, and Frank Piessens. "On Modular and Fully-Abstract Compilation". In: *IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016*. IEEE Computer Society, 2016, pp. 17–30. ISBN: 978-1-5090-2607-4. DOI: 10.1109/CSF.2016.9. URL: https://doi.org/10.1109/CSF.2016.9.

[36] Marco Patrignani and Deepak Garg. "Robustly Safe Compilation". In: *Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings*. 2019, pp. 469–498. DOI: 10.1007/978-3-030-17184-1\_17. URL: https://doi.org/10.1007/978-3-030-17184-1\_17.

[37] Marco Patrignani et al. "Secure Compilation to Protected Module Architectures". In: *ACM Trans. Program. Lang. Syst.* 37.2 (2015), 6:1–6:50. DOI: 10.1145/2699503. URL: https://doi.org/10.1145/2699503.

[38] Gordon D. Plotkin. "A structural approach to operational semantics". In: *J. Log. Algebr. Program.* 60-61 (2004), pp. 17–139.

[39] Andrei Popescu. "Weak Bisimilarity Coalgebraically". In: *Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings*. 2009, pp. 157–172. DOI: 10.1007/978-3-642-03741-2\_12. URL: https://doi.org/10.1007/978-3-642-03741-2\_12.

[40] John Power and Hiroshi Watanabe. "Distributivity for a monad and a comonad". In: *Electr. Notes Theor. Comput. Sci.* 19 (1999), p. 102. DOI: 10.1016/S1571-0661(05)80271-3. URL: https://doi.org/10.1016/S1571-0661(05)80271-3.

[41] Jurriaan Rot et al. "Enhanced coalgebraic bisimulation". In: *Mathematical Structures in Computer Science* 27.7 (2017), pp. 1236–1264. DOI: 10.1017/S0960129515000523. URL: https://doi.org/10.1017/S0960129515000523.

[42] Jan Rothe and Dragan Masulovic. "Towards Weak Bisimulation For Coalgebras". In: *Electr. Notes Theor. Comput. Sci.* 68.1 (2002), pp. 32–46. DOI: 10.1016/S1571-0661(04)80499-7. URL: https://doi.org/10.1016/S1571-0661(04)80499-7.
[43] Jan J. M. M. Rutten. "A note on coinduction and weak bisimilarity for while programs". In: *ITA* 33.4/5 (1999), pp. 393–400. DOI: 10.1051/ita:1999125. URL: https://doi.org/10.1051/ita:1999125.

[44] Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. "Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management". In: *Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings*. Ed. by Amal Ahmed. Vol. 10801. Lecture Notes in Computer Science. Springer, 2018, pp. 475–501. ISBN: 978-3-319-89883-4. DOI: 10.1007/978-3-319-89884-1\_17. URL: https://doi.org/10.1007/978-3-319-89884-1\_17.

[45] Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. "StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities". In: *Proc. ACM Program. Lang*. 3.POLP (Jan. 2019), 19:1–19:28. ISSN: 2475-1421. DOI: 10.1145/3290332.

[46] Stelios Tsampas, Dominique Devriese, and Frank Piessens. "Temporal Safety for Stack Allocated Memory on Capability Machines". In: *32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019*. IEEE, 2019, pp. 243–255. ISBN: 978-1-7281-1407-1. DOI: 10.1109/CSF.2019.00024. URL: https://doi.org/10.1109/CSF.2019.00024.

[47] Daniele Turi. "Categorical Modelling of Structural Operational Rules: Case Studies". In: *Category Theory and Computer Science, 7th International Conference, CTCS '97, Santa Margherita Ligure, Italy, September 4-6, 1997, Proceedings*. 1997, pp. 127–146. DOI: 10.1007/BFb0026985. URL: https://doi.org/10.1007/BFb0026985.

[48] Daniele Turi and Gordon D. Plotkin. "Towards a Mathematical Operational Semantics". In: *Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997*. 1997, pp. 280–291. DOI: 10.1109/LICS.1997.614955. URL: https://doi.org/10.1109/LICS.1997.614955.

[49] Thomas Van Strydonck, Frank Piessens, and Dominique Devriese. "Linear Capabilities for Fully Abstract Compilation of Separation-Logic-Verified Code". In: *Proc. ACM Program. Lang*. ICFP (2019). accepted.

[50] Hiroshi Watanabe. "Well-behaved Translations between Structural Operational Semantics". In: *Electr. Notes Theor. Comput. Sci.* 65.1 (2002), pp. 337–357. DOI: 10.1016/S1571-0661(04)80372-4. URL: https://doi.org/10.1016/S1571-0661(04)80372-4.

[51] Robert N. M. Watson et al. "CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization". In: *2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015*. IEEE Computer Society, 2015, pp. 20–37. ISBN: 978-1-4673-6949-7. DOI: 10.1109/SP.2015.9. URL: https://doi.org/10.1109/SP.2015.9.