Secure Compilation

Compilers convert source language to target language. Sometimes they take one pass, and sometimes they take multiple passes. We need to make sure the compiled language in each pass retains all the security properties of the source language : The goal of secure compilation techniques is to ensure this particular thing. Secure compilation is generally represented with an equivalence relation. Source language e_s is equivalent to target language e_t is written as e_s~e_t. if there is an intermediate compiler step then e_s ~ e_i and e_i ~ e_t should hold and from transitivity we get e_s ~ e_i ~ e_t .

To prove the equivalence we need to be prove (i) e_s~e_t and (ii) e_t~e_s. To prove the first one, closure conversion is done for all lambda functions. To prove the both (i) and (ii) logical relations and translation types are used. If some target term is of translation type then only it can be back-translated to source term. Amal’s paper on “Noninterference for Free” gives a good insight where they convert DCC to System F. Her OPLSS lectures are worth listening to.