Keywords

FormalPara Remark

To ease reading, we highlight the elements of source languages in , the target elements in and the common ones in black [33].

1 Introduction

Due to the complexity of modern computing systems, engineers make substantial use of layered design. Higher layers hide details of the lower ones and come with abstractions that ease reasoning about the system itself [39]. A layered design of programming languages allows to benefit from modules, interfaces or dependent types of a source, high-level language to write well-structured programs, and execute them efficiently in a target, low-level language, after compilation. Unfortunately, an attacker may exploit the lack of abstractions at the low-level to mount a so-called layer-below attack [39], which is otherwise impossible at the high-level [17, 18].

Secure compilation [35] devises both principles and proof techniques to preserve the (security-relevant) abstractions of the source and prevent layer-below attacks. Abadi [1] hinted that secure compilers must respect equivalences, as some security properties can be expressed in terms of indistinguishability w.r.t. arbitrary attackers, or contextual equivalence. Fully abstract compilers preserve and reflect (to avoid trivial translations) contextual equivalence.

Two decades of successes [1, 8, 9, 13, 14, 19, 34, 36, 43, 45] made full abstraction the gold-standard for secure compilation. However, some ad-hoc examples from recent literature [4, 37] showed that fully abstract compilers may still introduce bugs that were not present in source programs, e.g.,

Example 1

(See also Appendix E.5 of [4]). Consider source programs to be functions (from booleans to natural numbers) and target ones to be functions . Define contextual equivalence to be equality of outputs on equal inputs. Next, identify with , and compile a program to that coincides with and returns a default value – denoting a bug – otherwise,

is fully abstract, yet a source program that “never outputs 42”, will no longer enjoy this property.    \(\blacksquare \)

This simple example underlines the fact that if a security property like “never output 42” is not captured by contextual equivalence, there is no guarantee it will be preserved by a fully abstract compiler. Abadi [1] tellingly wrote

[...] we still have only a limited understanding of how to specify and prove that a translation preserves particular security properties. [...]

Abate et al. [4] proposed to specify security in terms of hyperproperties, sets of sets of traces of observable events [15]. In this setting, they consider a compiler secure only if it robustly preserves a class of hyperproperties, i.e., if it preserves their satisfaction against arbitrary attackers. For Example 1, “never output 42” can be specified as a safety hyperproperty, where function inputs and outputs are the observable events. The above compiler is not secure according to Abate et al. [4], as it does not robustly preserve the class of safety hyperproperties. More generally, each particular class of hyperproperties, e.g.,  the one for data integrity or the one for data confidentiality [15], determines a precise formal secure compilation criterion.

Despite the introduction of the robust criteria, full abstraction is still widely adopted [14, 19, 43, 45], for at least two reasons. First, contextual equivalence can model security properties such as noninterference [13], isolation [14], well-bracketed control flow or local state encapsulation [43] for programs that don’t expose events externally. Second, even though fully abstract compilers do not in general preserve data integrity or confidentiality, they often do so in practice.

Fully abstract and robust compilation both embody valuable notions of secure compilation and neither is stronger than the other nor are they orthogonal, which makes us believe their relation deserves further investigation. Our goal is to have criteria with well understood security guarantees for compiled programs, so that both users and developers of compilers may decide which criterion better fits their needs. For that, we assume an abstract trace semantics, collecting observables events and internal steps, is given for both source and target languages, and start our quest not by asking if a given fully abstract compiler preserves all hyperproperties, but which ones do and which ones do not preserve.

Contributions. First, we make explicit the guarantees given by full abstraction w.r.t. arbitrary source hyperproperties. We achieve this by showing that for every fully abstract compiler , there exists a translation or interpretation of source hyperproperties into target ones, \(\tilde{\tau }\), such that if robustly satisfies a source hyperproperty , robustly satisfies (Theorem 1). However, we observe that a fully abstract compiler may fail to preserve the robust satisfaction of some hyperproperty, as \(\tilde{\tau }\) may map interesting hyperproperties to trivial ones (Example 2). We then provide a sufficient and necessary condition to preserve the robust satisfaction of hyperproperties (Corollary 1), but argue that it is unfeasible to be proven true for an arbitrary fully abstract compiler. To overcome the above issues, we introduce a novel criterion, that we formulate in the abstract framework of Mathematical Operational Semantics (MOS). We show that our novel criterion implies full abstraction and the preservation of robust satisfaction of arbitrary hyperproperties (Sect. 5). We illustrate effectiveness and realizability of our criterion in Example 3.

2 Fully Abstract and Robust Compilation

Let us briefly recall the intuition of fully abstract and robust compilation, and provide their rigorous definitions. We refer the interested reader to [3, 4, 35] for more details.

2.1 Fully Abstract Compilation

Abadi [1] proposed fully abstract compilation to preserve security properties such as confidentiality and integrity when these are expressed in terms of indistinguishability w.r.t. the observations of arbitrary attackers, the latter modeled as execution contexts. For a concrete example, if no source context can distinguish a program that uses some confidential data k from a program that does not, we can deduce that k is kept confidential by . Thus, a compiler from a source language to a target one, that aims to preserve confidentiality, must ensure that also and are equivalent w.r.t. the observations of any target context . To avoid trivial translations, one typically asks for the reflection of the equivalence as well.

Definition 1

(Fully abstract compilation [1]). A compiler is fully abstract iff for any and ,

where , denote source and target contexts resp., , denote the two contextual equivalences, i.e.,  equivalence relations on programs.

Notice that the security notions one can preserve and reflect with a fully abstract compiler are those captured by the contextual equivalence relation \(\approx \), that determines both the meaningfulness and the effectiveness of full abstraction. Indeed, if is too coarse-grained, some interesting security properties may be ignored. Dually, if is too fine-grained, equivalent source programs may not have counterparts that are equivalent in the target. In Sect. 3, we pick \(\approx \) to be equality of execution traces which, under mild assumptions [20, 28], coincides with other common choices of \(\approx \) (see also Sect. 6).

2.2 Robust Compilation

Abate et al. [4] suggest a family of secure compilation criteria that depend on the security notion one is interested in preserving. The key idea in their criteria is the preservation of robust satisfaction, i.e., satisfaction of (classes of) security properties against arbitrary attackers, modeled as contexts. More concretely, Abate et al. [3, 4] assume that every execution of a program exposes a trace of observable events \(t \in Trace \) for a fixed set \( Trace \) and model interesting security notions like data integrity, confidentiality or observational determinism as sets of sets of traces, i.e.,  hyperproperties denoted by  [15].

Definition 2

(Robust satisfaction [3, 4]). A program P robustly satisfies a hyperproperty H iff \( \forall C.~C\left[ P\right] \models H \), where \(C\left[ P\right] \models H \triangleq beh (C\left[ P\right] ) \in H\) and \( beh (C\left[ P\right] )\) is the set of all traces that can be observed when executing \(C\left[ P\right] \).

Secure compilation criteria can then be defined as the preservation of robust satisfaction of classes of hyperproperties such as safety or liveness [4], in this paper we consider the class of all hyperproperties and robust hyperproperty preservation from [3]). For that, consider a function \(\tau \) that takes a source-level hyperproperty and returns its interpretation (or translation) at the target level. Intuitively, a compiler is if, for any source hyperproperty robustly satisfied by , its interpretation is robustly satisfied by , formally:

Definition 3

(Robust hyperproperty preservation). A compiler preserves the robust satisfaction of hyperproperties according to a translation iff the following holds

when \(\tau \) is clear from the context we simply say that is robust.

can be formulated without quantification on hyperproperties [3, 4].

Lemma 1

(Property-free ). For a compiler , is equivalent toFootnote 1

Notice that, while Definition 3 describes—through \(\tau \)—the target guarantees for against arbitrary target contexts, Lemma 1 enables proofs by back-translation. In fact, similarly to fully abstract compilation [35], one can prove that a compiler is by exhibiting a so-called back-translation map producing a source context whose interaction with exposes “the same” observables as does with :

Remark 1

( by back-translation). holds if there exists a back-translation function \( bk \) such that for any and any , is such that .

3 Comparing and

In the previous section we defined fully abstract compilation as the preservation and reflection of contextual equivalence, i.e.,  what the contexts can observe about programs. Instead, was defined as the preservation of (robust satisfaction of) hyperproperties of externally observable traces of events. To enable any comparison, we first provide an intuition on how to accommodate the mismatch in observations between full abstraction and (see the online appendix [5] for all the details). We assume the operational semantics of our languages exhaustively specify the execution of programs in contexts, including both internal steps and steps that expose externally observable events like inputs and outputs. Also, we say that a trace is abstract if it collects both internal steps and externally observable events. In a slight abuse of notation, we still denote with \( beh (C\left[ P\right] )\) the set of all the possible abstract traces allowed by the semantics when executing P in C. Moreover, since hyperproperties just express predicates over events , we now write \( beh (C\left[ P\right] ) \in H\) to mean that the traces of events for \(C\left[ P\right] \) satisfy the hyperproperty H. Finally, we elect to express contextual equivalence as the equality of the (sets of) abstract traces in an arbitrary context.

Definition 4

(Equality of \( beh (\cdot )\)). For programs \(P_1, P_2\) and a context  C,

$$ C\left[ P_1\right] \approx C\left[ P_2\right] \iff beh (C\left[ P_1\right] ) = beh (C\left[ P_2\right] ) $$

In Sect. 6 we discuss other common choices for \(\approx \) such as equi-termination, and the hypotheses under which they are equivalent to ours. We now instantiate Definition 1 on the contextual equivalence from Definition 4 and make explicit the notion of fully abstract compilation we are going to use from now on. Note how we are only interested in the preservation of contextual equivalence, as reflection is often subsumed by compiler correctness (e.g., in absence of internal non-determinism) [1, 35].

Definition 5

( ). For a compiler , is the following predicate

Abate et al. [4], Patrignani and Garg [37] have previously investigated the relation between as in Definition 5 and . In particular, Abate et al. [4] showed that does not imply any of the robust criteria, with an example similar to the one we sketched in Sect. 1. In this section, we provide further evidence of this fact: a fully abstract compiler that does not preserve the robust satisfaction of a security-relevant hyperproperty, namely noninterference. More details on the example can be found in the online appendix [5].

Example 2

Let and to be two WHILE-like languages [31] with a mutable state. A state \(s \in S \triangleq ( Var \rightarrow \mathbb {N})\) assigns every variable \(\texttt {v} \in Var \) a natural number. We assume \( Var \) to be partitioned into a “high” (private) and a “low” (public) part. We write \(\texttt {v} \in Var_H \) (\(\texttt {v} \in Var_L \), resp.) to denote that the variable \(\texttt {v}\) is private (public, resp.). Partial programs are defined in the same way in both and , whereas whole programs, or terms, are obtained by filling the hole(s) of a context with a partial program (Fig. 1). The only context in is , called the identity context and such that for any , . Instead, contexts in additionally include that is able to observe the internal event \(\mathcal {H}\) (intuitively, a form of information leakage that is not observed by source contexts) and report it by emitting !.

Fig. 1.
figure 1

\(\langle P \rangle \) defines the syntax of both and partial programs, where \(\langle expr \rangle \) denotes the usual arithmetic expressions over \(\mathbb {N}\). and define instead the contexts of and , respectively.

Full size image
Fig. 2.
figure 2

Selected rules of and .

Full size image

The semantics of and are partially given in Fig. 2. Rule  is for assignments that do not involve high variables. is for assignments of high variables, and – upon a change in their value – the internal trace \(\mathcal {H}\) is emitted. The counterparts, and , work similarly. Finally, the most interesting rule is , where we see how context reports a \(\mathbf ! \) upon encountering an \(\mathcal {H}\).

For example, consider a high variable \(\texttt {v} \in Var_H \) and the program . When is plugged in the identity context , the resulting behavior is Intuitively, the traces in express that the execution starts in a state s, then a high variable is updated (\(\mathcal {H}\)) leading to state \(s^\prime \) and then the program terminates \((\checkmark )\). For the same \(\texttt {v} \in Var_H \), target program in , we have that Notice the additional \(\mathbf ! \) w.r.t. the source, due to the fact that the context observed a change in a high variable. Informally, we say that a program satisfies noninterference if, executing it in two low-equivalent initial states, it transitions to two low-equivalent states. More rigorously, noninterference can be defined for both and as the following hyperproperty ,

where \(t_i^0\) stands for the first observable of the trace \(t_i\) and \(=_L\) denotes the fact that two states are low-equivalent (i.e.,  they coincide on all \(x \in Var_L \)). Also, we lift the notation to traces and write \(t_1 =_L t_2\) to denote that \(t_1\) and \(t_2\) are pointwise low-equivalent. More precisely, \(=_L\) ignores all occurrences of \(\mathcal {H}\) (as it is internal) and compares traces observable-by-observable, relating \(\checkmark \) and \(\mathbf ! \) to themselves and comparing states with the above notion of low-equivalence.

The identity compiler preserves trace equality (see the online appendix [5] for the proof), but does not preserve the robust satisfaction of noninterference as the context can detect changes in high variables and report a !.    \(\blacksquare \)

On the one hand, provides an explicit description of the target hyperproperty that is guaranteed to be robustly satisfied after compilation under the hypothesis that is robustly satisfied in the source. However, does not imply the preservation of contextual equivalence (or trace equality) because hyperproperties cannot specify which traces are allowed for every single context. On the other hand, it is possible that does not preserve (the robust satisfaction of) hyperproperties, because contextual equivalence may not capture some hyperproperty such as noninterference, as shown in Example 2. So, what kind of hyperproperties a compiler is guaranteed to preserve? If robustly satisfies (possibly not captured by ), what is the hyperproperty that is robustly satisfied by for being ?

We answer this question by defining a map so that implies . The map \(\tilde{\tau }\) enjoys an optimality condition making it the best possible description of the target guarantee for programs compiled by a compiler.

Theorem 1

If is , then there exists a map \(\tilde{\tau }\) such that is . Moreover, \(\tilde{\tau }\) is the smallest (pointwise) with this property.

To avoid any misunderstanding, we stress the fact that, akin to [32, Theorem 1], neither the existence, nor the optimality of \(\tilde{\tau }\) can be used to argue that a compiler is reasonably robust. The robustness of depends on the image of \(\tilde{\tau }\) on the hyperproperties of interest: it should not be trivial, e.g.,   like in Example 2 nor distort the intuitive meaning of the hyperproperty itself,  e.g.,  ”. In a setting in which observables are coarse enough to be common to source and target traces, i.e.,   = , it is possible to establish whether \(\tilde{\tau }(H)\) has “the same meaning” as H:

Corollary 1

If is , then for every hyperproperty H, preserves the robust satisfaction of H iff \(\tilde{\tau }(H) \subseteq H\), where \(\tilde{\tau }\) is the map from Theorem 1.

The rigorous definition of \(\tilde{\tau }\) and the proof of Theorem 1 and Corollary 1 can be found in the online appendix [5]. Here, we only mention that the definition of \(\tilde{\tau }\) requires information on the compiler itself, thus it can be unfeasible to compute and assess the meaningfulness of \(\tilde{\tau }(H)\). Corollary 1 partially mitigates this problem by allowing to approximate \(\tilde{\tau }(H)\) rather than computing it, e.g.,  by showing an intermediate K such that \(\tilde{\tau }(H) \subseteq K \subseteq H\). We leave as future work any approximation techniques for \(\tilde{\tau }\) that would make substantial use of Corollary 1.

To overcome the issues highlighted above, we extend the categorical approach to secure compilation of Tsampas et al. [48] and propose an abstract criterion that implies both and for a \(\tau \) defined via co-induction and therefore independent of the compiler. In Sect. 4 we shall summarize the underlying theory before introducing our criterion in Sect. 5.

4 Secure Compilation, Categorically

The basis of our approach and that of Tsampas et al. [48] is the framework of Mathematical Operational Semantics (MOS) [50]. Here, we briefly explain how MOS gives a mathematical description of programming languages as well as (secure) compilers and show how our earlier Example 2 fits such a framework. We refer the interested reader to the seminal paper of Turi and Plotkin [50] and the excellent introductory material of Klin [24] for more details. Further examples and applications can be found in the literature [48, 49, 51].

4.1 Distributive Laws and Operational Semantics

The main idea of MOS is that the semantics of programming languages, or systems in general, can be formally described through distributive laws (i.e., natural transformations of varying complexity) of a syntax functor \(\varSigma \) over a behavior functor B in a suitable category (in our case the category \(\mathbf {Set}\) of sets and total functions [24]). The functor \(\varSigma : \mathbf {Set}\rightarrow \mathbf {Set}\) represents the algebraic signature of the language and thus acts as an abstract description of its syntax. Instead, the functor \(B: \mathbf {Set}\rightarrow \mathbf {Set}\) describes the behavior of the language in terms of its observable events (e.g.,  the behavior of a non-deterministic labeled transition system can be modeled by the functor \(BX = \wp {(X)}^{\varDelta }\), where \(\varDelta \) is a set of trace labels [52]);

Recall now the languages and of Example 2. The syntax functor for for a set of terms X builds terms according to (the sum of all) the constructors of the language:

where E is the set of arithmetic expressions. The behavior functor for is a map that for an arbitrary set X, updates a store \(s \in S\), and either terminates (\(\checkmark \)) or returns another term in X, possibly recording that some high-variable has been modified (\(\mathcal {H}\)):

In , the syntax functor is , where the extra occurrence of X corresponds to the target context , and . We explicitly notice that syntactic “holes” are represented by the identity functor \(\mathrm {Id}\;X = X\) and, to make this connection clearer, the syntax functor for can be equivalently written as .

Next, we can define the operational semantics, a distributive law of \(\varSigma \) over B, in the format of a GSOS law ([24, Section 6.3]). A GSOS law of \(\varSigma \) over B is a natural transformation \(\rho : \varSigma (\mathrm {Id}\times B) \Longrightarrow B\varSigma ^{*}\), where \(\varSigma ^{*}\) is the free monad over \(\varSigma \). For instance, the rules of sequential composition in (see and in the online appendix [5, Fig. 4]) correspond to the following component of the GSOS law :

Here, with X a generic set of terms, i.e.,   and can be programs, contexts or programs within a context, and . The image of is an element of , depending on whether transitions to a term (thus involving ), or terminates with \(\checkmark \) ( ).

Lastly, we informally recall that when the formal semantics of a language is given through a GSOS law \(\rho : \varSigma (\mathrm {Id}\times B) \Longrightarrow B\varSigma ^{*}\), for \(\varSigma , B : \mathbf {Set}\rightarrow \mathbf {Set}\), the set of programs is (isomorphic to) the initial algebra \(A = \varSigma ^{*}\emptyset \), while the final coalgebra \(Z = B^{\infty }\top \)Footnote 2 describes the set of all possible behaviors.

Remark 2

A distributive law \(\rho \) induces a map \(f : A \rightarrow Z\) that assigns to every closed term or program its behaviors as specified by the law \(\rho \) itself.

For and from Example 2 and are just another, equivalent representation of and , e.g.,  for v private variable,

In other words, map \(f: A \rightarrow Z\) is the abstract counterpart of map \( beh (\cdot )\) that assigns to every program the set of all its possible execution traces.

4.2 Maps of Distributive Laws as Fully Abstract Compilers

Watanabe [51] first introduced maps of distributive laws (MoDL) as well-behaved translations between two GSOS languages. Tsampas et al. [48] showed how MoDL can also be used as a formal, abstract criterion for secure compilation. Let us recall the definition of MoDL for two GSOS laws in the same category.

Definition 6

(MoDL). A map of distributive law between and is a pair of natural transformations and such that the following diagram commutes,

figure cn

where extends to a morphism of free monads, i.e., to terms of arbitrary depth via structural induction.

The diagram in Definition 6 expresses a form of compatibility of the source and the target semantics. Considering any source term, executing it w.r.t. the source semantics and then translating the behavior (together with the resulting source term) is equivalent to first compiling the source term (and translating the behavior of its subterms) and then executing it w.r.t. the target semantics .

We recall that the set of source (resp. target) programs is ( resp.), and that is the compiler induced by s. On the behaviors side, the natural transformation induces a translation of behaviors where \(Z \triangleq B^{\infty }\top \). The compiler preserves (and also reflects when all the components of b are injective) bisimilarity (see [48], Section 4.3). Whenever bisimilarity coincides with trace equality (see Definition 4), for example under the assumption of determinacyFootnote 3, the following holds ([48]).

Corollary 2

In absence of internal non-determinism, MoDL implies .

Similarly to , the definition of MoDL does not ensure that is robust. Indeed, the obvious embedding compiler from Example 2 is a MoDL (let \(s = i_{1}\) and ). Intuitively, MoDL adequately captures the fact that compilation preserves the behavior of terms, but fails to capture the observations target contexts can make on compiled terms.

5 Reconciling Fully Abstract and Robust Compilation

To account for the shortcoming of MoDL, we introduce a new, complementary definition that allows reasoning explicitly on the semantic power of contexts in some target language relative to contexts in a source language. This definition acts (in conjunction with MoDL) as an abstract criterion of robust compilers.

For the new definition, we elect to qualify some constructors in \(\varSigma \) as contexts constructors so that \(\varSigma \triangleq \mathfrak {C}\uplus \mathfrak {P}\) where \(\mathfrak {C}\) defines the constructors for contexts and \(\mathfrak {P}\) for all the rest. We also assume that the GSOS law \(\rho : \varSigma (\mathrm {Id}\times B) \Longrightarrow \varSigma ^{*}B\) respects this “logical partition” of \(\varSigma \) in that \(\rho = [ B\;i_1 \circ \rho _1, ~\rho _2 ]\) where \(\rho _1: \mathfrak {C}(\mathrm {Id}\times B) \Longrightarrow B \mathfrak {C}^{*}\) and \(\rho _2: \mathfrak {P}(\mathrm {Id}\times B) \Longrightarrow B \varSigma ^{*}\).

Definition 7

(MMoDL). A many layers map of distributive laws (MMoDL) between and is given by natural transformations and making the following commute:

figure cr

The top-left object, , represents a target context which is filled with some source term, whose subterms exhibit some source behavior. In both paths, the plugged source terms are initially evaluated w.r.t. the source semantics. On the upper path, we first back-translate [16] the target context using t, then we run the resulting program w.r.t. the source semantics (), and finally we translate the resulting behavior back to the target via b. Instead, in the lower path we first translate the resulting behavior through , then we let the target context observe (), and finally we back-translate the behavior via .

To relate MMoDL with , we formulate the latter in the framework of MOS. Recall (see Remark 1) that holds if there exists a back-translation map \( bk \) that for every target context and program , produces a source context such that .

Remark 3

((Abstract) ). For , a compiler is iff there exists \( bk \) such that

where \(f : A \rightarrow Z\) associates to every program its behaviors as specified by \(\rho \) (see Remark 2) and \( plug \) is the operation of plugging a term into a context.

We are now ready to state our second contribution, namely that the pairing of a MoDL (s, b) and a MMoDL (t, b) gives an (abstract) compiler.

Theorem 2

(MMoDL imply ). Let , and such that (s, b) and (t, b) are (respectively) a MoDL and a MMoDL from to . The compiler is (abstract) for \(\tau = b^{\infty }_{\top }\) coinductively induced by b.

Proof (Sketch). The back-translation \( bk := t^{*}_{\emptyset } \times id \) satisfies the equation in Remark 3 (details in the online appendix [5]).    \(\square \)

Before fixing the compiler from Example 2 to make it satisfy both MoDL (Definition 6) and MMoDL (Definition 7), let us see why the back-translation mapping both target contexts to the identity source context is not a MMoDL. Let \(\texttt {v} \in Var_H \) be a private variable, on the upper path of Definition 7 we have

figure cz

Note how the identity context fails to report !. On the lower path, we have instead

figure da

Here, it is evident that the context “picks up” \(\mathcal {H}\) and reports !, unlike  .

Example 3

(Example 2, revisited). We now show how to fix the compiler from Example 2 by making it for a suitable \(\tau \). For that, we first need to slightly modify the language . The idea is that variable assignments in should now be sandboxed, so that the interactions with the context do not expose sensitive information. Formally, we extend the algebraic signature of with a constructor for sandboxing assignments, i.e.,  , so that terms are generated by grammar

where the semantics of is described in Fig. 3. We can now define the new (i.e.,  fixed) compiler and the appropriate map \(\tau \), so that is . Both and \(\tau \) are determined by the natural transformations s, t, and b, such that (s, b) is a MoDL and (t, b) is a MMoDL. The natural transformation , and therefore the inductively defined compiler , wraps assignments in the sandbox , i.e.,   and acts as the identity on other terms. The natural transformation maps every context to the identity context . Finally, the translation of behaviors erases the occurrences of \(\mathcal {H}\), implying that the compiled terms are not expected to report changes in high variables.

Fig. 3.
figure 3

Rules extending the semantics of .

Full size image

Recall that the diagram from Definition 7 failed to commute for Example 2, because (s, b) being a MoDL imposed b to not erase any occurrences of \(\mathcal {H}\). The same diagram for the new language and natural transformations s, b, and t now commutes. More specifically, in the upper path we have

figure dm

while in the lower path we get

figure dn

We point the reader interested to the online appendix [5] for more details in showing that the above (s, b) is a MoDL and that (t, b) is a MMoDL.

Hereafter, we discuss one of the benefits of the abstract definitions presented so far, namely that we can easily compute \(\tau \), and immediately establish if programs that robustly satisfy (noninterference in ) are compiled to programs that robustly satisfy . In order to do so, we need to connect and to traces and hyperproperties of and . Elements of Z are functions that assign to every \(s \in S\) a new state \(s'\) and maybe an extra symbol like \(\mathbf ! \) or \(\mathcal {H}\), and a continuation, i.e.,  another function of the same type. Traces are instead sequences of stores possibly exhibiting the extra symbols \(\mathcal {H}\) and \(\mathbf ! \). It is easy to show (see the online appendix [5]) that every trace corresponds to an element of Z – the function that returns the head of the trace and continues as the tail of the same trace – and that every function in Z corresponds to a set of traces – one trace for every fixed \(s \in S\). Thus, we can prove that \(\tau \) maps (the set of functions in corresponding to) to a subset of (the set of functions corresponding to) , i.e.,   the compiler preserves robust satisfaction.    \(\blacksquare \)

6 Related Work

In this section, we discuss related work regarding origins and applications of full abstraction, trace based criteria, MoDL and relevant proof techniques.

Full abstraction was introduced to relate the operational and the denotational semantics of programming languages [40]. A denotational semantics of a language is said to be fully abstract w.r.t. an operational one for the same language iff the same denotation is given to contextually equivalent terms, i.e.,  those terms that result the same when evaluated according to the operational semantics. Common choices to establish when the result of the evaluation is the same, and hence to define contextual equivalence, are equi-convergence and equi-divergence (e.g.,  in [13, 14, 23, 28, 38]). Notice that there is no loss of generality with these choices, if (and only if!) contexts are powerful enough [28], e.g., when all inputs can be thought as part of the context, and the context itself may select one final value as the result of the execution or diverge.

Fully abstract translations as in Definition 1 have been adopted for comparing expressiveness of languages (see, e.g.,  the works by Mitchell [28] and Patrignani et al. [38]), but Gorla and Nestmann [21] showed that they may lead to false positive results. The interested reader can find out more in the online appendix [5], where we also sketch how to use for expressiveness comparisons.

Full Abstraction and Secure Compilation. Abadi [1] originally proposed to use full abstraction to preserve security properties in translations from a source language \(L_1\) to a target one \(L_2\). A fully abstract translation or compiler preserves and reflects equivalences, and can therefore be a way to preserve security properties when these are expressed as equivalences. Remarkable examples from the literature are given by Bowman and Ahmed [13], Busi et al. [14] and Skorstengaard et al. [43]. In the first two works the authors model contexts so that contextual equivalence captures (forms of) noninterference and preserve it through a fully abstract translation. Skorstengaard et al. [43] consider a source language with well-bracketed control flow (WBCF) and local state encapsulation (LSE), then model target contexts so that these two properties are captured by contextual equivalence and, they exhibit a fully abstract translation so that both WBCF and LSE are guaranteed also in the target. We stress the fact that, all security properties that are not captured by contextual equivalence are not necessarily preserved by a fully abstract compiler, thus allowing for counterexamples similar to Example 1. Finally, it is worth noting that fully abstract compilation does not prevent source programs to be insecure, nor suggests how to fix them, quoting Abadi [1]:

An expression of the source language \(L_1\) may be written in a silly, incompetent, or even malicious way. For example, the expression may be a program that broadcasts some sensitive information—so this expression is insecure on its own, even before any translation to \(L_2\). Thus, full abstraction is clearly not sufficient for security [...]

Beyond Full Abstraction. Several definitions of “well-behaved translations” exist, depending both on the scenario and on the properties one aims to preserve during the translation. For example, if the goal is to preserve functional correctness, then it is natural to require the compiled program to simulate the source one [29]. This can be expressed both as a relation between the operational semantics of the source and the target (see for example [27, 42, 51]), or extrinsically as a relation between the execution traces of programs before and after compilation [3, 12, 46]. Trace based criteria for compiler correctness The CompCert [12, 26] and CakeML [46] projects are milestones in the formal verification of compilers. Preservation of functional correctness can be expressed in both cases in terms of execution traces [3]. For the CompCert compiler, executing w.r.t. the target semantics yields the same observable events as executing w.r.t. the source semantics, as long as does not encounter an undefined behavior. Similarly, CakeML ensures that executing w.r.t. the target semantics yields the same observable events as executing w.r.t. the source semantics, as long as there is enough space in target memory. In both cases, correctness is proven by exhibiting a simulation between and .

Trace Based Criteria for Secure Compilation. Similarly to what happens for functional correctness, relations between the execution traces of a program and of its compiled version, can be used to express preservation of noninterference through compilation [10, 11, 30]. The simulation-based techniques introduced in CompCert sometimes suffice also to show the preservation of noninterference, e.g.,  when the source and the target semantics are equipped with a notion of leakage [10, Sections 5.2–5.4]. However, in more general cases a stronger, cube-shaped simulation is needed (see [10, Section 5.5], and [11, 30]). Stewart et al. [44] propose a variant of CompCert that also gives some guarantees w.r.t. source contexts, and their compilation in the target. Still, this does not guarantee security against arbitrary target contexts, that can be strictly stronger than source ones. Abate et al. [3, 4] propose a family of criteria with the goal of preserving satisfaction of (classes of) security properties against arbitrary contexts. Also, they show that their criteria can be formulated in at least two equivalent ways. The first one explicitly describes the target guarantees ensured for compiled programs, for example which safety properties are guaranteed for programs written in unsafe languages and compiled according to the criterion proposed by Abate et al. [2] (see their Appendix A). The second way is instead more amenable to proofs, e.g.,  by enabling proofs by back-translation Abate et al. [2, Fig. 4].

Maps of Distributive Laws (MoDL). Mathematical Operational Semantics (MOS) and distributive laws ensure well-behavedness of the operational semantics of a language while also providing a formal description for it. Such semantics have been given for languages with algebraic effects [6] and for stochastic calculi [25]. In their biggest generality distributive laws are defined between monads and comonads [24], but it is often convenient to consider the slightly less general GSOS laws that correspond bijectively to GSOS rules [7, 24, 41].

Proof Techniques for fully abstract compilation include both cross-language logical relations between source and compiled programs [13, 35, 43] and back-translation of target contexts into source ones [14, 16, 35]. The latter technique sometimes exploits information from execution traces [16], and can be adapted also to some of the robust criteria of Abate et al. [4]. Ongoing work is aiming to formalize the back-translation technique needed to prove some of the robust preservation of safety (hyper)properties in the Coq proof assistant [2, 47]. The best results in mechanization of secure compilation criteria have been achieved for the criteria that can be proven via simulations, especially when extending the CompCert proof scripts, e.g.,  [10]. The complexity of many proofs is relatively contained as they show a forward simulation—the source program simulates the one in the target—and “flip” it into a backward one—the compiled program simulates the source one—with a general argument. We are not aware of mechanized proofs for MoDL, but we believe it would be convenient to first express maps between GSOS laws as relations between GSOS rules (see also Sect. 7).

7 Conclusions and Future Work

The scope of this work has been to clarify the guarantees provided by criteria for secure compilation, make them explicit and immediately accessible to users and developers of (provably) secure compilers. We investigated the relation between fully abstract and robust compilation, provided an explicit description of the hyperproperties robustly preserved by a fully abstract compiler, and noticed that these are not always meaningful, nor of practical utility. We have therefore introduced a novel criterion that ensures both fully abstract and robust compilation, and such that the meaningfulness of the hyperproperty guaranteed to hold after compilation can be easily established. The proposed example shows that our criterion is achievable.

Future work will focus on proof techniques for MoDL and MMoDL that are amenable to formalization in a proof assistant. For that we can either build on existing formalizations of polynomial functors as containers, or exploit the correspondence between GSOS laws and GSOS rules, and characterize MoDL and MMoDL as relations between source and target rules. Another interesting line of work consists in devising over (under) approximation for the map \(\tilde{\tau }\) from Theorem 1, and use our Corollary 1 to establish whether existing fully abstract compilers preserve (violate) a given hyperproperty.