Fully Abstract Trace Semantics for Low-level Isolation Mechanisms – Extended version

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) com-pilation 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. Low-level machine code offers virtually no protection mechanism from an attacker that has code injection privileges, who is free to read sensible data and disrupt the execution flow with malicious code. A way to defend against these kind of attacks is by employing a fine-grained program counter-based memory access control mechanisms (FPMAC). The idea behind recent FPMACs implementations [3, 5, 8, 9], is to run sensitive code in isolation, so that malicious low-level code cannot tamper with it. Although details of these works differ, the FPMAC protection mechanism can be summarized as follows. The memory is logically divided into a protected and an unprotected section. Protected memory is further divided into a code and a data section. The code section contains a number of entry points: addresses which unprotected memory instructions can jump to and execute. The data section is accessible only from the protected section. The following table provides a representation of the access control model enforced by the protection mechanism