Secure compilation of oject-oriented components to untyped machine code
Marco Patrignani, Dave Clarke, Frank Piessens · Lirias · 2013
A fully abstract compilation scheme prevents high-level code security features from being bypassed by an attacker operating at a lower level. This paper presents a fully abstract compilation scheme from a realistic object-oriented language with dynamic memory allocation to untyped machine code. Full abstraction of the compilation scheme relies on enhancing the low-level machine model with a fine-grained, program counter-based memory access control mechanism. This paper contains the outline of a formal proof of full abstraction of the compilation scheme, guaranteeing that low- and high-level attackers have the same power.