Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components
This work addresses secure compilation for systems with distrustful components, representing an incremental advance by extending full abstraction to this context.
The authors tackled the problem of secure compilation for mutually distrustful components by proposing a new attacker model and implementing a compiler chain with a novel security monitor using micro-policies, achieving protection of language abstractions like class isolation and type safety against arbitrary low-level attacks.
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.