• type systems
• control-flow flattening
• constant-time policy
• translation validation
• full abstraction
• secure compilation
• language-based security

Software is pervasive in our daily lives and we rely on it for many critical tasks. Despite the abundance of (formal) techniques that can be used to prevent bugs, software is often incorrect and insecure. One of the sources of this insecurity is that a gap persists between what the programmer writes and what actually gets executed.

Such a gap is mainly due to the fact that it is often hard to translate (e.g., via compilation) a source language (typically at high-level) into a target language (typically at lower-level), without losing any abstraction.

Indeed, a well-known advantage of using a high-level language is that it usually provides a multiplicity of abstractions and mechanisms (e.g., types, modules, automatic memory management) that enforce good programming practices and ease programmers in writing correct and secure code. However, those high-level abstractions do not always have counterparts at the low-level. This discrepancy can be dangerous when the source level abstractions are used to enforce security properties: if the target language does not provide any mechanism to preserve such properties, the resulting code is vulnerable to attacks.

One tentative solution could be to adapt the source to the target language (or vice versa) to make them equally powerful, but that is undesirable because we possibly lose the advantages that come from having different levels of abstraction in the source and in the target. A better solution is to work on the compiler itself, by guaranteeing that it preserves the source-level security properties. The emerging field of secure compilation has exactly this goal. More precisely, secure compilation is concerned with ensuring that the security properties at the source level are preserved as they are at the target level or, equivalently, that all the (interesting) attacks that can be carried out at the target level have corresponding attacks at the source level. In this way, the reasoning carried out at the source level to rule out attacks suffices to rule out attacks at the target.

This thesis approaches the problem of secure compilation from three different points of view. We argue that secure compilation --- being relevant at many levels of the computational stack --- needs to be tackled at different levels of abstraction, depending on the security goals that one has in mind.

At the highest level of abstraction we work on verifying that security properties are preserved under program transformations whose target language is the same as the source (e.g., program optimizations or obfuscations). We first follow a classical approach and we manually prove that the widely-used control-flow flattening program obfuscation preserves the constant-time policy, i.e., a security policy that requires that the execution time of programs does not depend on their secret inputs. Then, we move to an automatic and efficient approach. For that, we assume a (security) type system that statically checks whether the property of interest holds or not, and we provide a framework to make its usage incremental, so as to make it possible to perform the analysis after each optimization step without excessively slowing down the compiler.

Moving down from the highest level of abstraction, we weaken the requirement about the source and the target languages being equal and consider transformations that involve a translation step. This line of research is more general and follows an approach similar to that of translation validation to automatically certify that a compiled program has a given security property knowing that its original version enjoys it.

Finally, at the very bottom of the computational stack we deal with low-level attackers, e.g., those that can carry out micro-architectural attacks. More precisely, we provide an instantiation of the well-known principle of full abstraction to prove that an extension to an enclaved-execution architecture is secure with respect to the class of interrupt-based micro-architectural attacks.