In this short talk I will try to encourage our emerging community not to make secure compilation merely a synonym for full abstraction and variants, since there are important practical settings in which full abstraction and its variants do not seem to provide a reasonable attacker model. I will particularly discuss about side-channel attacks, for which full abstraction seems too strong and hopeless to realistically achieve in practice, but for which two intuitively weaker properties seem much better suited: For cryptographic code that is written in a constant-time discipline one can show that a compiler preserves its side-channel resistance. For non-cryptographic code, one will very likely have to give up confidentially guarantees in the presence of side-channels, but one can still focus on the preservation of robust safety, which still goes beyond compiler correctness and is strong enough to imply the preservation of certain forms of integrity such as data invariants even in an adversarial low-level context. As such I believe that it is in the best interest of our community to take a broad and inclusive view of secure compilation not just when it comes to enforcement mechanisms and proof techniques, but also with respect to the guarantees one aims for in the first place.

Catalin is a tenured Research Scientist at Inria Paris where he develops rigorous formal techniques for solving security problems. He is particularly interested in formal methods for security (memory safety, compartmentalization, dynamic monitoring, integrity, security protocols, information flow), programming languages (type systems, verification, proof assistants, property-based testing, semantics, formal metatheory, certified tools), and the design and verification of security-critical systems (reference monitors, secure compilers, microkernels, secure hardware). He is actively involved in the design of the F* verification system and was recently awarded an ERC Starting Grant on secure compilation. Catalin was a PhD student at Saarland University and a Research Associate at University of Pennsylvania before joining Inria Paris in 2013.