Many secure compilation chains aim at ensuring that if there is no attack a source context can mount against a source program then there is no attack an adversarial target context can mount against the compiled program. One may, for instance, try to prevent attacks against trace properties (e.g., safety), hyperproperties (e.g., noninterference), or relational hyperproperties (e.g., observational equivalence).

Proving that these compilation chains are secure is, however, challenging. For any target attack one has to exhibit a source context mounting the same attack against the source program. Such back-translations can be highly complex, especially for hyperproperties and relational hyperproperties.

We describe a novel back-translation technique that results in simpler proofs, which can be more easily mechanized in a proof assistant like Coq. Given any number of finite trace prefixes, our back-translation builds a single source context producing these prefixes. We see the finite set of trace prefixes as a tree of events, and use state in the back-translated context to record the current position in this tree. The back-translation is done in many small steps, each adding to the tree new information describing how the location should change depending on how the context regains control. To prove such a back-translation correct we give semantics to every intermediate tree language and prove many small forward simulations, basically seeing the back-translation as a verified nanopass compiler.

This technique allows us to prove in Coq a strong secure compilation criterion for an existing simple compilation chain that was previously only proved to satisfy a weaker criterion.