Katholieke Universiteit Leuven
The authors present a secure (fully abstract) compilation scheme to compile an object-based high-level language to low-level machine code. Full abstraction is achieved by relying on a fine-grained program counter-based memory access protection scheme, which is part of their low-level target language. They discuss why standard compilers fail to provide full abstraction and introduce enhancements needed to achieve this goal. They prove that their enhanced compilation scheme provides full abstraction from their high-level source language to their low-level target language.