Fully abstract trace semantics of low-level protection mechanisms
Marco Patrignani, Dave Clarke · Lirias · 2012
Fine-grained program counter-based memory access control mechanisms can be used to enhance low-level machine models to become the target of secure (fully abstract) compilation schemes. A secure compilation scheme reduces the power of a low-level attacker with code injection privileges to that of a high-level attacker which generally does not have such privileges. The existing trace semantics for a fine-grained program counter-based memory access control mechanism is not fully abstract, thus the protection mechanism it models cannot be used as the target of a provably secure compilation scheme. This paper shows why is such a fully abstract trace semantics needed, and proposes a correction to the existing trace semantics that makes it fully abstract and thus capable of supporting a secure compilation scheme.