Universal Composability is Secure Compilation
- Marco Patrignani, Riad S. Wahby, Robert Künnemann
In compiler verification, we look to prove a compiler correct by proving that it has a certain property. For example, the (currently) "standard" property is Semantics Preservation which states that compiled program's behaviour must be one of the source program's behaviours (must be the same) i.e. the compiler should not introduce new behaviours. Behaviour is dependent on a language's semantics -- For example, a language might have non-determinism (multiple behaviours) or might not permit infinite loops (e.g. non-turing complete languages). Intuitively, the semantics of the source and target languages must be similar/close enough to be given a notion of "behaves the same".
Semantics preservation typically only works for compilers that process whole programs e.g. semantics perservation does not apply to cases where you link with a pre-compiled library, or libraries written in another language. This is precisely because programmers are interested in linking/combining code from vastly different source languages where it is difficult to give their semantics a notion of "behaves the same".
Consider compiled Java (a memory safe langauge) code that is linked against a C (a memory unsafe language) library.
Secure compilation is the current area of research that studies
- the properties of interest (to verify) in a separate compilation setting i.e. what does it mean for our compiler to maintain "memory safety" of the compiled Java code?
- what kind of guarantees about source level security (or really, any) abstractions we can provide in target code in a separate compilation setting. i.e. How can we prove our compiler "maintains the memory safety of the compile Java code"? (Whatever that means).
In our little tour of SC, we looked at a property called (Contextual) Equivalence preservation, which is a candidate for a "standard" notion of secure compilation. Back translations are one technique to prove this property and were mentioned in the UCisSC paper as something that could contribute to UC side.
Formal Approaches to Secure Compilation
- Marco Patrignani, Amal Ahmed, Dave Clarke