Published In

IEEE Symposium on Security and Privacy 2015

Document Type


Publication Date



Cache memory, Computer security


Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level “symbolic machine,” and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety; in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy’s rules embodies a high-level specification characterizing a useful security property. Last, we show how the symbolic machine itself can be implemented in terms of a hardware rule cache and a software controller.


This paper was presented at IEEE Symposium on Security and Privacy 2015, May 17-21, 2015, San Jose, CA. This is the postprint version. The final version is on the publisher's website:



Persistent Identifier