Published In

IEEE Symposium on Security and Privacy 2015

Document Type

Post-Print

Publication Date

5-2015

Subjects

Cache memory, Computer security

Abstract

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.

Description

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: http://dx.doi.org/10.1109/SP.2015.55

DOI

10.1109/SP.2015.55

Persistent Identifier

http://archives.pdx.edu/ds/psu/16805

Download

Share

COinS