Fully abstract trace semantics for protected module architectures

摘要

Protected module architectures (PMAs) are isolation mechanisms of emerging processors that provide security building blocks for modern software systems. Reasoning about these building blocks means reasoning about elaborate assembly code, which can be very complex due to the loose structure of the code. One way to overcome this complexity is providing the code with a well-structured semantics. This paper presents one such semantics, namely a fully abstract trace semantics, for an assembly languag