Formally Secure Compilation
-----------------------------------
          
ABSTRACT
-----------------------------------
Severe low-level vulnerabilities abound in today's 
computer systems, allowing cyber-attackers to remotely 
gain full control. This happens in big part because our 
programming languages, compilers, and architectures 
were designed in an era of scarce hardware resources 
and too often trade off security for efficiency. The 
semantics of mainstream low-level languages like C is 
inherently insecure, and even for safer languages, 
establishing security with respect to a high-level 
semantics does not guarantee the absence of low-level 
attacks.

SECOMP (http://secure-compilation.github.io/) is a new 
ERC-funded project aimed at leveraging emerging 
hardware capabilities for fine-grained protection to 
build the first, efficient secure compilers for 
realistic low-level programming languages (the C 
language, and Low* a safe subset of C embedded in F* 
for verification).  These compilers will provide a more 
secure semantics for source programs and will ensure 
that high-level abstractions cannot be violated even 
when interacting with untrusted low-level code.  To 
achieve this level of security without sacrificing 
efficiency, our secure compilers target a tagged 
architecture, which associates a metadata tag to each 
word and efficiently propagates and checks tags 
according to software-defined rules.  We are using 
property-based testing and formal verification to 
provide high confidence that our compilers are indeed 
secure.

Formally, we are constructing machine-checked proofs in 
Coq of fully abstract compilation and of novel secure 
compilation criteria that ensure the preservation of 
large classes of hyperproperties even against an 
adversarial context.  These strong properties 
complement compiler correctness and ensure that no 
machine-code attacker can do more harm to securely 
compiled components than a component already could with 
respect to a secure source-level semantics.