Towards effective preservation of robust safety properties

Secure compilation investigates when compilation chains preserve security properties. Over the years, different formal criteria and proof techniques have been put forward for proving a compiler secure. However, these proposals require a lot of manual effort by compiler designers. This paper introduces a formal approach to mechanically support these efforts. We focus on the specific class of robust safety properties and we propose a translation validation approach that leverages program analysis techniques to check that a compilation run preserves security.