Secure compilation prevents all low-level attacks on compiled code and allows for sound reasoning about security in the source language. In this work we propose a new attacker model for secure compilation that extends the well-known notion of full abstraction to ensure protection for mutually distrustful components. We devise a compiler chain (compiler, linker, and loader) and a novel security monitor that together defend against this strong attacker model. The monitor is implemented using a recently proposed, generic tag-based protection framework called micro-policies, which comes with hardware support for efficient caching and with a formal verification methodology. Our monitor protects the abstractions of a simple object-oriented language---class isolation, the method call discipline, and type safety---against arbitrary low-level attackers.
@article{arxiv.1510.00697,
title = {Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components},
author = {Yannis Juglaret and Catalin Hritcu and Arthur Azevedo de Amorim and Benjamin C. Pierce and Antal Spector-Zabusky and Andrew Tolmach},
journal= {arXiv preprint arXiv:1510.00697},
year = {2015}
}