An Equivalence-Preserving CPS Translation Via Multi-Language Semantics
Language-based security relies on the assumption that all potential attacks follow the rules of the language in question. When programs are compiled into a different language, this is true only if the translation process preserves observational equivalence. To prove that a translation preserves equivalence, one must show that if two program fragments cannot be distinguished by any source context, then their translations cannot be distinguished by any target context. Informally, target contexts must be no more powerful than source contexts, i.e., for every target context there exists a source context that "Behaves the same." This seems to amount to being able to "Back-translate" arbitrary target terms.