Secure compilation to modern processors: extended version

We present a secure (fully abstract) compilation scheme to compile a high-level language to low-level machine code. Full abstraction is achieved by relying on the virtualization support provided by modern processors: a small hypervisor efficiently implements fine-grained memory access control, and this gives the low-level language sufficient protection features to serve as a target for the fully abstract compilation of a simple Java-like language. We formalize high-level and low-level languages and prove full abstraction for our compilation algorithm. We also show by means of an implementation that our low-level language with fine-grained memory access-control can be realized efficiently on modern commodity platforms. This report is an extended version of the paper published at Computer Security Foundations Symposium 2012. It extends the conference version with technical details about the formalization and the proofs.nrpages: 41status: publishe